From ddb90d3038f77b4058b29c65f1269d951bc21a07 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Sep 2013 17:58:46 -0700 Subject: [PATCH] feat(kernel): add unification_constraint and trace objects to the kernel Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work. The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables. Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication. Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 1 - src/kernel/CMakeLists.txt | 3 +- src/kernel/metavar.h | 94 ++++++++++++++- src/kernel/trace.cpp | 15 +++ src/kernel/trace.h | 62 ++++++++++ src/kernel/unification_constraint.cpp | 80 +++++++++++++ src/kernel/unification_constraint.h | 160 ++++++++++++++++++++++++++ src/library/ho_unifier.cpp | 24 ++-- src/tests/library/ho_unifier.cpp | 18 +-- 9 files changed, 432 insertions(+), 25 deletions(-) create mode 100644 src/kernel/trace.cpp create mode 100644 src/kernel/trace.h create mode 100644 src/kernel/unification_constraint.cpp create mode 100644 src/kernel/unification_constraint.h diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 445fd8811..93f1830f4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include #include #include diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 41b3f4d8c..45bd0e26b 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,5 +1,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp normalizer.cpp context.cpp level.cpp object.cpp environment.cpp - type_checker.cpp builtin.cpp occurs.cpp metavar.cpp) + type_checker.cpp builtin.cpp occurs.cpp metavar.cpp trace.cpp + unification_constraint.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index ed32b464f..2d6477462 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -85,9 +85,99 @@ public: */ template void for_each(F f) const { m_subst.for_each(f); } +}; - // TODO(Leo) metavar - expr mk_metavar(context const & = context()) { return expr(); } +/** + \brief Metavar environment. It is an auxiliary datastructure used for: + + 1- Creating metavariables. + 2- Storing their types and the contexts where they were created. + 3- Storing substitutions. + 4- Collecting constraints +*/ +class metavar_env { + typedef splay_map name2expr; + typedef splay_map name2context; + + name_generator m_name_generator; + substitution m_substitution; + name2expr m_metavar_types; + name2context m_metavar_contexts; + unsigned m_timestamp; + + void inc_timestamp(); +public: + metavar_env(); + + /** + \brief The timestamp is increased whenever this environment is + updated. + */ + unsigned get_timestamp() const { return m_timestamp; } + + /** + \brief Create a new metavariable in the given context and with the given type. + */ + expr mk_metavar(context const & ctx = context(), expr const & type = expr()); + + /** + \brief Return the context where the given metavariable was created. + \pre is_metavar(m) + */ + context get_context(expr const & m); + context get_context(name const & m); + + /** + \brief Return the type of the given metavariable. + \pre is_metavar(m) + */ + expr get_type(expr const & m); + expr get_type(name const & m); + + /** + \brief Return true iff the metavariable named \c m is assigned in this substitution. + */ + bool is_assigned(name const & m) const; + + /** + \brief Return true if the given metavariable is assigned in this + substitution. + + \pre is_metavar(m) + */ + bool is_assigned(expr const & m) const; + + /** + \brief Assign metavariable named \c m. + + \pre !is_assigned(m) + */ + void assign(name const & m, expr const & t); + + /** + \brief Assign metavariable \c m to \c t. + + \pre is_metavar(m) + \pre !has_meta_context(m) + \pre !is_assigned(m) + */ + void assign(expr const & m, expr const & t); + + /** + \brief Return the set of substitutions. + */ + substitution const & get_substitutions() const; + + /** + \brief Return the substitution associated with the given metavariable + in this substitution. + + If the metavariable is not assigned in this substitution, then it returns the null + expression. + + \pre is_metavar(m) + */ + expr get_subst(expr const & m) const; }; /** diff --git a/src/kernel/trace.cpp b/src/kernel/trace.cpp new file mode 100644 index 000000000..35c2dda0d --- /dev/null +++ b/src/kernel/trace.cpp @@ -0,0 +1,15 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/trace.h" + +namespace lean { +bool trace::has_children() const { + buffer r; + get_children(r); + return !r.empty(); +} +} diff --git a/src/kernel/trace.h b/src/kernel/trace.h new file mode 100644 index 000000000..d4e072c93 --- /dev/null +++ b/src/kernel/trace.h @@ -0,0 +1,62 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "util/debug.h" +#include "util/rc.h" +#include "util/buffer.h" +#include "util/sexpr/format.h" + +namespace lean { +class trace; +/** + \brief Base class used to represent trace objects. + These objects are used to trace the execution of different engines in Lean. + The traces may help users understanding why something did not work. + The traces are particularly important for the elaborator. +*/ +class trace_cell { + MK_LEAN_RC(); + void dealloc() { delete this; } +public: + virtual ~trace_cell() {} + virtual format pp() const = 0; + virtual void get_children(buffer & r) const = 0; +}; + +/** + \brief Smart pointer for trace_cell's +*/ +class trace { + trace_cell * m_ptr; + explicit trace(trace_cell * ptr):m_ptr(ptr) {} +public: + trace():m_ptr(nullptr) {} + trace(trace const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + trace(trace && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~trace() { if (m_ptr) m_ptr->dec_ref(); } + + operator bool() const { return m_ptr != nullptr; } + + trace_cell * raw() const { return m_ptr; } + + friend void swap(trace & a, trace & b) { std::swap(a.m_ptr, b.m_ptr); } + + trace & operator=(trace const & s) { LEAN_COPY_REF(trace, s); } + trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); } + format pp() const { lean_assert(m_ptr); return m_ptr->pp(); } + void get_children(buffer & r) const { if (m_ptr) m_ptr->get_children(r); } + bool has_children() const; +}; + +inline unsigned get_rc(trace const & t) { return t.raw()->get_rc(); } +inline bool is_shared(trace const & t) { return get_rc(t) > 1; } +inline format pp(trace const & t) { return t.pp(); } +inline void get_children(trace const & t, buffer & r) { + return t.get_children(r); +} +} diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp new file mode 100644 index 000000000..56c44361d --- /dev/null +++ b/src/kernel/unification_constraint.cpp @@ -0,0 +1,80 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/unification_constraint.h" + +namespace lean { +unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t): + m_kind(k), m_ctx(c), m_trace(t), m_rc(1) { +} +void unification_constraint_cell::dealloc() { + switch (m_kind) { + case unification_constraint_kind::Eq: + delete static_cast(this); + break; + case unification_constraint_kind::Convertible: + delete static_cast(this); + break; + case unification_constraint_kind::Max: + delete static_cast(this); + break; + case unification_constraint_kind::Choice: + static_cast(this)->~unification_constraint_choice(); + delete[] reinterpret_cast(this); + break; + } +} + +unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t): + unification_constraint_cell(unification_constraint_kind::Eq, c, t), + m_lhs(lhs), + m_rhs(rhs) { +} + +unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t): + unification_constraint_cell(unification_constraint_kind::Convertible, c, t), + m_from(from), + m_to(to) { +} + +unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t): + unification_constraint_cell(unification_constraint_kind::Max, c, t), + m_lhs1(lhs1), + m_lhs2(lhs2), + m_rhs(rhs) { +} + +unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t): + unification_constraint_cell(unification_constraint_kind::Choice, c, t), + m_mvar(mvar), + m_num_choices(num) { +} + +unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t) { + return unification_constraint(new unification_constraint_eq(c, lhs, rhs, t)); +} + +unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t) { + return unification_constraint(new unification_constraint_convertible(c, from, to, t)); +} + +unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t) { + return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, t)); +} + +unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t) { + char * mem = new char[sizeof(unification_constraint_choice) + num*sizeof(expr)]; + unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, t)); + expr * m_choices = to_choice(r)->m_choices; + for (unsigned i = 0; i < num; i++) + new (m_choices+i) expr(choices[i]); + return r; +} + +unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list const & choices, trace const & t) { + return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), t); +} +} diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h new file mode 100644 index 000000000..1ca0642e8 --- /dev/null +++ b/src/kernel/unification_constraint.h @@ -0,0 +1,160 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "kernel/expr.h" +#include "kernel/context.h" +#include "kernel/trace.h" + +namespace lean { +/** + \brief There are four kinds of unification constraints in Lean + + 1- ctx |- t == s t is (definitionally) equal to s + 2- ctx |- t << s t is convertible to s (this is weaker than equality) + 3- ctx |- max(t1, t2) == s The maximum of t1 and t2 is equal to s + 4- ctx |- ?m == t_1 Or ... Or ?m == t_k The metavariable ?m is equal to t_1, ..., or t_k + + \remark The constraint ctx |- t == s implies that ctx |- t << s, but + the converse is not true. Example: ctx |- Type 1 << Type 2, but + we don't have ctx |- Type 1 == Type 2. + + \remark In the max constraint, \c t1 and \c t2 must be eventually unifiable with a Type term. + For example, assume the constraint ctx |- max(?m1, Type 1) == ?m2. Now, suppose + ?m2 is assigned to Type 1. Then, ?m1 can be assigned to Type 0 + or Type 1. +*/ +enum class unification_constraint_kind { Eq, Convertible, Max, Choice }; + +/** + \brief Base class for all Lean unification constraints. +*/ +class unification_constraint_cell { + unification_constraint_kind m_kind; + context m_ctx; + trace m_trace; //!< justification for this constraint + MK_LEAN_RC(); + void dealloc(); +public: + unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t); + unification_constraint_kind kind() const { return m_kind; } + trace const & get_trace() const { return m_trace; } + context const & get_context() const { return m_ctx; } +}; + +class unification_constraint { +private: + unification_constraint_cell * m_ptr; + explicit unification_constraint(unification_constraint_cell * ptr):m_ptr(ptr) {} +public: + unification_constraint():m_ptr(nullptr) {} + unification_constraint(unification_constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + unification_constraint(unification_constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~unification_constraint() { if (m_ptr) m_ptr->dec_ref(); } + + friend void swap(unification_constraint & a, unification_constraint & b) { std::swap(a.m_ptr, b.m_ptr); } + + unification_constraint & operator=(unification_constraint const & s) { LEAN_COPY_REF(unification_constraint, s); } + unification_constraint & operator=(unification_constraint && s) { LEAN_MOVE_REF(unification_constraint, s); } + + unification_constraint_kind kind() const { return m_ptr->kind(); } + unification_constraint_cell * raw() const { return m_ptr; } + + operator bool() const { return m_ptr != nullptr; } + + friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t); + friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t); + friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t); + friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t); +}; + +/** + \brief Unification constraint of the form ctx |- lhs == rhs +*/ +class unification_constraint_eq : public unification_constraint_cell { + expr m_lhs; + expr m_rhs; +public: + unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t); + expr const & get_lhs() const { return m_lhs; } + expr const & get_rhs() const { return m_rhs; } +}; + +/** + \brief Unification constraint of the form ctx |- from << to. + The meaning is \c from is convertible to \c to. Example: ctx |- Type 1 << Type 2. + It is weaker than ctx |- from == rhs. +*/ +class unification_constraint_convertible : public unification_constraint_cell { + expr m_from; + expr m_to; +public: + unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t); + expr const & get_from() const { return m_from; } + expr const & get_to() const { return m_to; } +}; + +/** + \brief Unification constraint of the form ctx |- max(lhs1, lhs2) == rhs. +*/ +class unification_constraint_max : public unification_constraint_cell { + expr m_lhs1; + expr m_lhs2; + expr m_rhs; +public: + unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t); + expr const & get_lhs1() const { return m_lhs1; } + expr const & get_lhs2() const { return m_lhs2; } + expr const & get_rhs() const { return m_rhs; } +}; + +/** + \brief Unification constraint of the form ctx |- mvar == choices[0] OR ... OR mvar == choices[size-1]. +*/ +class unification_constraint_choice : public unification_constraint_cell { + expr m_mvar; + unsigned m_num_choices; + expr m_choices[0]; + friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t); +public: + unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t); + expr const & get_mvar() const { return m_mvar; } + unsigned get_num_choices() const { return m_num_choices; } + expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; } + expr const * begin_choices() const { return m_choices; } + expr const * end_choices() const { return m_choices + m_num_choices; } +}; + +unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t); +unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t); +unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t); +unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t); +unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list const & choices, trace const & t); + +inline bool is_eq(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Eq; } +inline bool is_convertible(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Convertible; } +inline bool is_max(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Max; } +inline bool is_choice(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Choice; } + +inline unification_constraint_eq * to_eq(unification_constraint const & c) { lean_assert(is_eq(c)); return static_cast(c.raw()); } +inline unification_constraint_convertible * to_convertible(unification_constraint const & c) { lean_assert(is_convertible(c)); return static_cast(c.raw()); } +inline unification_constraint_max * to_max(unification_constraint const & c) { lean_assert(is_max(c)); return static_cast(c.raw()); } +inline unification_constraint_choice * to_choice(unification_constraint const & c) { lean_assert(is_choice(c)); return static_cast(c.raw()); } + +context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); } +trace const & get_trace(unification_constraint const & c) { return c.raw()->get_trace(); } +expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); } +expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); } +expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); } +expr const & convertible_to(unification_constraint const & c) { return to_convertible(c)->get_to(); } +expr const & max_lhs1(unification_constraint const & c) { return to_max(c)->get_lhs1(); } +expr const & max_lhs2(unification_constraint const & c) { return to_max(c)->get_lhs2(); } +expr const & max_rhs(unification_constraint const & c) { return to_max(c)->get_rhs(); } +expr const & choice_mvar(unification_constraint const & c) { return to_choice(c)->get_mvar(); } +unsigned choice_size(unification_constraint const & c) { return to_choice(c)->get_num_choices(); } +expr const & choice_ith(unification_constraint const & c, unsigned i) { return to_choice(c)->get_choice(i); } +} diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp index 21735a298..52d68c284 100644 --- a/src/library/ho_unifier.cpp +++ b/src/library/ho_unifier.cpp @@ -142,7 +142,7 @@ class ho_unifier::imp { \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s */ - bool contains_solution(list const & r, substitution const & s, residue const & rs, substitution const & ini_s) { + bool contains_solution(list const & r, substitution const & /* s */, residue const & rs, substitution const & /* ini_s */ ) { return empty(rs) && std::any_of(r.begin(), r.end(), [&](result const & prev) { @@ -162,7 +162,7 @@ class ho_unifier::imp { \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s */ - substitution cleanup_subst(substitution const & s, substitution const & ini_s) { + substitution cleanup_subst(substitution const & s, substitution const & /* ini_s */) { #if 0 // TODO(Leo) metavar metavar_env new_s; for (unsigned i = 0; i < ini_s.size(); i++) { @@ -426,7 +426,7 @@ class ho_unifier::imp { buffer imitation_args; // arguments for the imitation imitation_args.push_back(f_b); for (unsigned i = 1; i < num_b; i++) { - expr h_i = new_s.mk_metavar(ctx); + expr h_i; // = new_s.mk_metavar(ctx); imitation_args.push_back(mk_app_vars(h_i, num_a - 1)); new_q.push_front(constraint(ctx, update_app(a, 0, h_i), arg(b, i))); } @@ -437,8 +437,8 @@ class ho_unifier::imp { // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), (h_1 x_1 ... x_{num_a-1}) = (h_2 x_1 ... x_{num_a-1}) // New constraints (h_1 a_1 ... a_{num_a-1}) == eq_lhs(b) // (h_2 a_1 ... a_{num_a-1}) == eq_rhs(b) - expr h_1 = new_s.mk_metavar(ctx); - expr h_2 = new_s.mk_metavar(ctx); + expr h_1; // = new_s.mk_metavar(ctx); + expr h_2; // = new_s.mk_metavar(ctx); expr imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1))); new_s.assign(mname, imitation); new_q.push_front(constraint(ctx, update_app(a, 0, h_1), eq_lhs(b))); @@ -449,8 +449,8 @@ class ho_unifier::imp { // fun (x_b : (?h_1 x_1 ... x_{num_a-1})), (?h_2 x_1 ... x_{num_a-1} x_b) // New constraints (h_1 a_1 ... a_{num_a-1}) == abst_domain(b) // (h_2 a_1 ... a_{num_a-1} x_b) == abst_body(b) - expr h_1 = new_s.mk_metavar(ctx); - expr h_2 = new_s.mk_metavar(ctx); + expr h_1; // = new_s.mk_metavar(ctx); + expr h_2; // = new_s.mk_metavar(ctx); expr imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a))); new_s.assign(mname, imitation); new_q.push_front(constraint(ctx, update_app(a, 0, h_1), abst_domain(b))); @@ -510,20 +510,20 @@ class ho_unifier::imp { buffer imitation; imitation.push_back(f_b); for (unsigned i = 1; i < num_b; i++) - imitation.push_back(new_s.mk_metavar(ctx)); + imitation.push_back(expr()); // new_s.mk_metavar(ctx)); new_s.assign(mname, mk_app(imitation.size(), imitation.data())); } else if (is_eq(b)) { // Imitation for equality b == Eq(s1, s2) // mname <- Eq(?h_1, ?h_2) - expr h_1 = new_s.mk_metavar(ctx); - expr h_2 = new_s.mk_metavar(ctx); + expr h_1; // = new_s.mk_metavar(ctx); + expr h_2; // = new_s.mk_metavar(ctx); new_s.assign(mname, mk_eq(h_1, h_2)); } else if (is_abstraction(b)) { // Lambdas and Pis // Imitation for Lambdas and Pis, b == Fun(x:T) B // mname <- Fun (x:?h_1) ?h_2 x) - expr h_1 = new_s.mk_metavar(ctx); - expr h_2 = new_s.mk_metavar(ctx); + expr h_1; // = new_s.mk_metavar(ctx); + expr h_2; // = new_s.mk_metavar(ctx); new_s.assign(mname, update_abstraction(b, h_1, mk_app(h_2, Var(0)))); } else { new_q.push_front(constraint(ctx, pop_meta_context(a), lift_free_vars(b, i, 1))); diff --git a/src/tests/library/ho_unifier.cpp b/src/tests/library/ho_unifier.cpp index 2e9589fd4..76c344b3a 100644 --- a/src/tests/library/ho_unifier.cpp +++ b/src/tests/library/ho_unifier.cpp @@ -29,7 +29,7 @@ void tst1() { expr x = Const("x"); expr a = Const("a"); expr b = Const("b"); - expr m1 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); expr l = m1(b, a); expr r = f(b, f(a, b)); for (auto sol : unify(context(), l, r, subst)) { @@ -55,7 +55,7 @@ void tst2() { expr x = Const("x"); expr a = Const("a"); expr b = Const("b"); - expr m1 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); expr l = m1(b, a); expr r = Fun({x, N}, f(x, Eq(a, b))); for (auto sol : unify(context(), l, r, subst)) { @@ -77,9 +77,9 @@ void tst3() { env.add_var("f", N >> (Int >> N)); env.add_var("a", N); env.add_var("b", N); - expr m1 = subst.mk_metavar(); - expr m2 = subst.mk_metavar(); - expr m3 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); + expr m2; // = subst.mk_metavar(); + expr m3; // = subst.mk_metavar(); expr t1 = metavar_type(m1); expr t2 = metavar_type(m2); expr f = Const("f"); @@ -107,8 +107,8 @@ void tst4() { expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); - expr m1 = subst.mk_metavar(); - expr m2 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); + expr m2; // = subst.mk_metavar(); expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1))); expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x))); auto sols = unify(context(), l, r, subst); @@ -130,7 +130,7 @@ void tst5() { env.add_var("N", Type()); env.add_var("f", N >> (N >> N)); expr f = Const("f"); - expr m1 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); expr l = f(f(m1)); expr r = f(m1); auto sols = unify(context(), l, r, subst); @@ -147,7 +147,7 @@ void tst6() { expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); - expr m1 = subst.mk_metavar(); + expr m1; // = subst.mk_metavar(); expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x)); expr r = Fun({x, N}, f(x, x)); auto sols = unify(context(), l, r, subst);