diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 29393fc3c..59bfad578 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -67,6 +67,20 @@ function(add_theory FILE DEPS) endif() endfunction() +# The following command invokes the lean binary to update .cpp/.h interface files +# associated with a .lean file. +function(update_interface FILE DEST ARG) + get_filename_component(BASENAME ${FILE} NAME_WE) + set(CPPFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.cpp") + set(HFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.h") + add_custom_command(OUTPUT ${CPPFILE} ${HFILE} + COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2cpp.lean > ${CPPFILE} + COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2h.lean > ${HFILE} + DEPENDS ${FILE}) + add_custom_target("${BASENAME}_decls" DEPENDS ${CPPFILE}) + add_dependencies(builtin ${BASENAME}_decls) +endfunction() + add_kernel_theory("kernel.lean" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua") add_kernel_theory("Nat.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") @@ -75,3 +89,8 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") + +update_interface("kernel.lean" "kernel" "-n") +update_interface("Nat.lean" "library/arith" "-n") +update_interface("Int.lean" "library/arith" "") +update_interface("Real.lean" "library/arith" "") \ No newline at end of file diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 35b8db6c8..1b3e0c177 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -61,7 +61,7 @@ axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x) -- Alias for subst where we can provide P explicitly, but keep A,a,b implicit -definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b +theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b := subst H1 H2 theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f @@ -267,12 +267,6 @@ theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false := boolext (λ H, absurd (and_eliml H) (and_elimr H)) (λ H, false_elim (a ∧ ¬ a) H) -theorem not_true : (¬ true) == false -:= trivial - -theorem not_false : (¬ false) == true -:= trivial - theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) := case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b)) (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b) diff --git a/src/builtin/lean2cpp.lean b/src/builtin/lean2cpp.lean new file mode 100644 index 000000000..0da5c219b --- /dev/null +++ b/src/builtin/lean2cpp.lean @@ -0,0 +1,32 @@ +(* + -- Auxiliary script for generating .cpp files that define + -- constants defined in Lean + local env = get_environment() + local num_imports = 0 + print('/*') + print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.') + print('Released under Apache 2.0 license as described in the file LICENSE.') + print('*/') + print("// Automatically generated file, DO NOT EDIT") + print('#include "kernel/environment.h"') + print('#include "kernel/decl_macros.h"') + print('namespace lean {') + for obj in env:objects() do + if obj:is_begin_import() or obj:is_begin_builtin_import() then + num_imports = num_imports + 1 + elseif obj:is_end_import() then + num_imports = num_imports - 1 + elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then + local is_fn = env:normalize(obj:get_type()):is_pi() + io.write('MK_CONSTANT(') + name_to_cpp_decl(obj:get_name()) + if is_fn then + io.write('_fn') + end + io.write(', ') + name_to_cpp_expr(obj:get_name()) + print(');') + end + end + print('}') +*) diff --git a/src/builtin/lean2h.lean b/src/builtin/lean2h.lean new file mode 100644 index 000000000..d9a226294 --- /dev/null +++ b/src/builtin/lean2h.lean @@ -0,0 +1,71 @@ +(* + -- Auxiliary script for generating .h file that declare mk_* and is_* functions for + -- constants defined in Lean + local env = get_environment() + local num_imports = 0 + print('/*') + print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.') + print('Released under Apache 2.0 license as described in the file LICENSE.') + print('*/') + print("// Automatically generated file, DO NOT EDIT") + print('#include "kernel/expr.h"') + print('namespace lean {') + for obj in env:objects() do + if obj:is_begin_import() or obj:is_begin_builtin_import() then + num_imports = num_imports + 1 + elseif obj:is_end_import() then + num_imports = num_imports - 1 + elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then + local ty = env:normalize(obj:get_type()) + local is_fn = ty:is_pi() + local arity = 0 + while ty:is_pi() do + n, d, ty = ty:fields() + arity = arity + 1 + end + local is_th = obj:is_theorem() or obj:is_axiom() + io.write("expr mk_") + name_to_cpp_decl(obj:get_name()) + if is_fn then + io.write("_fn"); + end + print("();") + io.write("bool is_") + name_to_cpp_decl(obj:get_name()) + if is_fn then + io.write("_fn"); + end + print("(expr const & e);") + if is_fn and not is_th then + io.write("inline bool is_") + name_to_cpp_decl(obj:get_name()) + io.write("(expr const & e) { return is_app(e) && is_"); + name_to_cpp_decl(obj:get_name()) + print("_fn(arg(e, 0)); }") + end + if is_fn then + io.write("inline expr mk_") + name_to_cpp_decl(obj:get_name()) + if is_th then + io.write("_th"); + end + io.write("("); + for i = 1, arity do + if i > 1 then + io.write(", ") + end + io.write("expr const & e" .. tostring(i)) + end + io.write(") { return mk_app({mk_"); + name_to_cpp_decl(obj:get_name()) + io.write("_fn()") + for i = 1, arity do + io.write(", e" .. tostring(i)) + end + print ("}); }") + end + end + end + print('}') + +*) diff --git a/src/builtin/name_conv.lua b/src/builtin/name_conv.lua new file mode 100644 index 000000000..d287e7035 --- /dev/null +++ b/src/builtin/name_conv.lua @@ -0,0 +1,38 @@ +-- Output a C++ statement that creates the given name +function name_to_cpp_expr(n) + function rec(n) + if not n:is_atomic() then + rec(n:get_prefix()) + io.write(", ") + end + if n:is_string() then + io.write("\"" .. n:get_string() .. "\"") + else + error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n)) + end + end + + io.write("name(") + if n:is_atomic() then + rec(n) + else + io.write("{") + rec(n) + io.write("}") + end + io.write(")") +end + +-- Output a C++ constant name based on the given hierarchical name +-- It uses '_' to glue the hierarchical name parts +function name_to_cpp_decl(n) + if not n:is_atomic(n) then + name_to_cpp_decl(n:get_prefix()) + io.write("_") + end + if n:is_string() then + io.write(n:get_string()) + else + error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n)) + end +end diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index e28979830..c6bc65842 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 2d5d7f2a5..65c52721c 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,34 +44,20 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } -static name g_eq_imp_trans("eq_imp_trans"); -static name g_imp_eq_trans("imp_eq_trans"); -static name g_imp_trans("imp_trans"); -static name g_eq_ne_trans("eq_ne_trans"); -static name g_ne_eq_trans("ne_eq_trans"); -static name g_neq("neq"); - calc_proof_parser::calc_proof_parser() { expr imp = mk_implies_fn(); - expr eq = mk_homo_eq_fn(); - expr iff = mk_iff_fn(); - expr neq = mk_constant(g_neq); + expr eq = mk_eq_fn(); + expr neq = mk_neq_fn(); add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(eq, 3)); - add_supported_operator(op_data(iff, 2)); add_supported_operator(op_data(neq, 3)); add_trans_step(eq, eq, trans_data(mk_trans_fn(), 6, eq)); - add_trans_step(eq, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); - add_trans_step(imp, eq, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); - add_trans_step(imp, imp, trans_data(mk_constant(g_imp_trans), 5, imp)); - add_trans_step(iff, iff, trans_data(mk_trans_fn(), 6, iff)); - add_trans_step(iff, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); - add_trans_step(imp, iff, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); - add_trans_step(eq, iff, trans_data(mk_trans_fn(), 6, iff)); - add_trans_step(iff, eq, trans_data(mk_trans_fn(), 6, iff)); - add_trans_step(eq, neq, trans_data(mk_constant(g_eq_ne_trans), 6, neq)); - add_trans_step(neq, eq, trans_data(mk_constant(g_ne_eq_trans), 6, neq)); + add_trans_step(eq, imp, trans_data(mk_eq_imp_trans_fn(), 5, imp)); + add_trans_step(imp, eq, trans_data(mk_imp_eq_trans_fn(), 5, imp)); + add_trans_step(imp, imp, trans_data(mk_imp_trans_fn(), 5, imp)); + add_trans_step(eq, neq, trans_data(mk_eq_ne_trans_fn(), 6, neq)); + add_trans_step(neq, eq, trans_data(mk_ne_eq_trans_fn(), 6, neq)); } optional calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const { @@ -108,12 +94,12 @@ static expr parse_step_pr(parser_imp & imp, expr const & lhs) { expr eq_pr = imp.parse_expr(); imp.check_rcurly_next("invalid calculational proof, '}' expected"); // Using axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b. - return imp.save(Subst(imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), // let elaborator compute the first four arguments - imp.save(Refl(imp.save(mk_placeholder(), p), lhs), p), - eq_pr), p); + return imp.save(mk_subst_th(imp.save(mk_placeholder(), p), + imp.save(mk_placeholder(), p), + imp.save(mk_placeholder(), p), + imp.save(mk_placeholder(), p), // let elaborator compute the first four arguments + imp.save(mk_refl_th(imp.save(mk_placeholder(), p), lhs), p), + eq_pr), p); } else { return imp.parse_expr(); } diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index 2e4d9de77..3ac59cb01 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -561,11 +561,11 @@ expr parser_imp::parse_led_id(expr const & left) { } /** \brief Parse expr '=' expr. */ -expr parser_imp::parse_eq(expr const & left) { +expr parser_imp::parse_heq(expr const & left) { auto p = pos(); next(); expr right = parse_expr(g_eq_precedence); - return save(mk_eq(left, right), p); + return save(mk_heq(left, right), p); } /** \brief Parse expr '->' expr. */ @@ -947,7 +947,7 @@ expr parser_imp::mk_app_left(expr const & left, expr const & arg) { expr parser_imp::parse_led(expr const & left) { switch (curr()) { case scanner::token::Id: return parse_led_id(left); - case scanner::token::Eq: return parse_eq(left); + case scanner::token::Eq: return parse_heq(left); case scanner::token::Arrow: return parse_arrow(left); case scanner::token::LeftParen: return mk_app_left(left, parse_lparen()); case scanner::token::IntVal: return mk_app_left(left, parse_nat_int()); diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index dce04e7e0..815ee39b6 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -291,7 +291,7 @@ private: pos_info const & p); expr parse_expr_macro(name const & id, pos_info const & p); expr parse_led_id(expr const & left); - expr parse_eq(expr const & left); + expr parse_heq(expr const & left); expr parse_arrow(expr const & left); expr parse_lparen(); void parse_names(buffer> & result); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b210c55d1..d20737faa 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -234,7 +234,7 @@ class pp_fn { return is_atomic(arg(e, 1)); else return false; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::HEq: case expr_kind::Let: return false; } return false; @@ -441,7 +441,7 @@ class pp_fn { operator_info op = get_operator(e); if (op) { return op.get_precedence(); - } else if (is_eq(e)) { + } else if (is_heq(e)) { return g_eq_precedence; } else if (is_arrow(e)) { return g_arrow_precedence; @@ -459,7 +459,7 @@ class pp_fn { operator_info op = get_operator(e); if (op) { return op.get_fixity() == fx; - } else if (is_eq(e)) { + } else if (is_heq(e)) { return fixity::Infix == fx; } else if (is_arrow(e)) { return fixity::Infixr == fx; @@ -1022,7 +1022,7 @@ class pp_fn { } /** \brief Pretty print the child of an equality. */ - result pp_eq_child(expr const & e, unsigned depth) { + result pp_heq_child(expr const & e, unsigned depth) { if (is_atomic(e)) { return pp(e, depth + 1); } else { @@ -1034,11 +1034,11 @@ class pp_fn { } /** \brief Pretty print an equality */ - result pp_eq(expr const & e, unsigned depth) { + result pp_heq(expr const & e, unsigned depth) { result p_arg1, p_arg2; format r_format; - p_arg1 = pp_eq_child(eq_lhs(e), depth); - p_arg2 = pp_eq_child(eq_rhs(e), depth); + p_arg1 = pp_heq_child(heq_lhs(e), depth); + p_arg2 = pp_heq_child(heq_rhs(e), depth); r_format = group(format{p_arg1.first, space(), g_eq_fmt, line(), p_arg2.first}); return mk_result(r_format, p_arg1.second + p_arg2.second + 1); } @@ -1121,7 +1121,7 @@ class pp_fn { case expr_kind::Lambda: case expr_kind::Pi: r = pp_abstraction(e, depth); break; case expr_kind::Type: r = pp_type(e); break; - case expr_kind::Eq: r = pp_eq(e, depth); break; + case expr_kind::HEq: r = pp_heq(e, depth); break; case expr_kind::Let: r = pp_let(e, depth); break; case expr_kind::MetaVar: r = pp_metavar(e, depth); break; } diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 494edf5a4..ffb33a973 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/io_state.h" #include "kernel/decl_macros.h" +#include "kernel/kernel_decls.cpp" namespace lean { // ======================================= @@ -19,7 +20,6 @@ expr const TypeU = Type(u_lvl); // ======================================= // Boolean Type -MK_CONSTANT(Bool, "Bool"); expr const Bool = mk_Bool(); expr mk_bool_type() { return mk_Bool(); } bool is_bool(expr const & t) { return is_Bool(t); } @@ -116,57 +116,6 @@ static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); }); static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); }); // ======================================= -MK_CONSTANT(implies_fn, name("implies")); -MK_CONSTANT(iff_fn, name("iff")); -MK_CONSTANT(and_fn, name("and")); -MK_CONSTANT(or_fn, name("or")); -MK_CONSTANT(not_fn, name("not")); -MK_CONSTANT(forall_fn, name("forall")); -MK_CONSTANT(exists_fn, name("exists")); -MK_CONSTANT(homo_eq_fn, name("eq")); -// Axioms -MK_CONSTANT(mp_fn, name("mp")); -MK_CONSTANT(discharge_fn, name("discharge")); -MK_CONSTANT(case_fn, name("case")); -MK_CONSTANT(refl_fn, name("refl")); -MK_CONSTANT(subst_fn, name("subst")); -MK_CONSTANT(abst_fn, name("funext")); -MK_CONSTANT(htrans_fn, name("htrans")); -MK_CONSTANT(hsymm_fn, name("hsymm")); -// Theorems -MK_CONSTANT(eta_fn, name("eta")); -MK_CONSTANT(imp_antisym_fn, name("iffintro")); -MK_CONSTANT(trivial, name("trivial")); -MK_CONSTANT(false_elim_fn, name("false_elim")); -MK_CONSTANT(absurd_fn, name("absurd")); -MK_CONSTANT(em_fn, name("em")); -MK_CONSTANT(double_neg_fn, name("doubleneg")); -MK_CONSTANT(double_neg_elim_fn, name("doubleneg_elim")); -MK_CONSTANT(mt_fn, name("mt")); -MK_CONSTANT(contrapos_fn, name("contrapos")); -MK_CONSTANT(absurd_elim_fn, name("absurd_elim")); -MK_CONSTANT(eq_mp_fn, name("eqmp")); -MK_CONSTANT(not_imp1_fn, name("not_imp_eliml")); -MK_CONSTANT(not_imp2_fn, name("not_imp_elimr")); -MK_CONSTANT(conj_fn, name("and_intro")); -MK_CONSTANT(conjunct1_fn, name("and_eliml")); -MK_CONSTANT(conjunct2_fn, name("and_elimr")); -MK_CONSTANT(disj1_fn, name("or_introl")); -MK_CONSTANT(disj2_fn, name("or_intror")); -MK_CONSTANT(disj_cases_fn, name("or_elim")); -MK_CONSTANT(refute_fn, name("refute")); -MK_CONSTANT(symm_fn, name("symm")); -MK_CONSTANT(trans_fn, name("trans")); -MK_CONSTANT(congr1_fn, name("congr1")); -MK_CONSTANT(congr2_fn, name("congr2")); -MK_CONSTANT(congr_fn, name("congr")); -MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); -MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); -MK_CONSTANT(forall_elim_fn, name("forall_elim")); -MK_CONSTANT(forall_intro_fn, name("forall_intro")); -MK_CONSTANT(exists_elim_fn, name("exists_elim")); -MK_CONSTANT(exists_intro_fn, name("exists_intro")); - void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index e5a7e925b..c7113bec0 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/expr.h" +#include "kernel/io_state.h" +#include "kernel/kernel_decls.h" namespace lean { // See src/builtin/kernel.lean for signatures. @@ -32,191 +33,12 @@ bool is_true(expr const & e); /** \brief Return true iff \c e is the Lean false value. */ bool is_false(expr const & e); -expr mk_if_fn(); -bool is_if_fn(expr const & e); -inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); } -inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); } -inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); } -inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(mk_bool_type(), c, t, e); } -inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool_if(c, t, e); } - -expr mk_implies_fn(); -bool is_implies_fn(expr const & e); -inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); } -inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); } inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } - -expr mk_iff_fn(); -bool is_iff_fn(expr const & e); -inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); } -inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); } -inline expr Iff(expr const & e1, expr const & e2) { return mk_iff(e1, e2); } - -expr mk_and_fn(); -bool is_and_fn(expr const & e); -inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); } -inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); } inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); } - -expr mk_or_fn(); -bool is_or_fn(expr const & e); -inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); } -inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); } inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); } - -expr mk_not_fn(); -bool is_not_fn(expr const & e); -inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); } -inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); } inline expr Not(expr const & e) { return mk_not(e); } - -expr mk_forall_fn(); -bool is_forall_fn(expr const & e); -inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e, 0)); } -inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); } -inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); } - -expr mk_exists_fn(); -bool is_exists_fn(expr const & e); -inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); } -inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); } inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); } +// inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_eq(A, l, r); } -expr mk_homo_eq_fn(); -bool is_homo_eq_fn(expr const & e); -inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); } -inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); } -inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); } - -expr mk_mp_fn(); -inline expr MP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mp_fn(), a, b, H1, H2); } - -expr mk_discharge_fn(); -inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); } - -expr mk_case_fn(); -inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); } - -expr mk_refl_fn(); -inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); } - -expr mk_subst_fn(); -inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); } - -expr mk_eta_fn(); -inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); } - -expr mk_imp_antisym_fn(); -inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); } - -expr mk_abst_fn(); -inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); } - -expr mk_hsymm_fn(); -inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) { return mk_app({mk_hsymm_fn(), A, B, a, b, H1}); } - -expr mk_htrans_fn(); -inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { - return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2}); -} - -expr mk_trivial(); -#define Trivial mk_trivial() - -expr mk_true_ne_false(); -#define TrueNeFalse mk_true_ne_false(); - -expr mk_em_fn(); -inline expr EM(expr const & a) { return mk_app(mk_em_fn(), a); } - -expr mk_false_elim_fn(); -inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); } - -expr mk_absurd_fn(); -inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); } - -expr mk_double_neg_fn(); -inline expr DoubleNeg(expr const & a) { return mk_app(mk_double_neg_fn(), a); } - -expr mk_double_neg_elim_fn(); -inline expr DoubleNegElim(expr const & P, expr const & H) { return mk_app(mk_double_neg_elim_fn(), P, H); } - -expr mk_mt_fn(); -inline expr MT(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mt_fn(), a, b, H1, H2); } - -expr mk_contrapos_fn(); -inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); } - -expr mk_false_imp_any_fn(); -inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); } - -expr mk_absurd_elim_fn(); -inline expr AbsurdElim(expr const & a, expr const & c, expr const & H1, expr const & H2) { - return mk_app(mk_absurd_elim_fn(), a, c, H1, H2); -} - -expr mk_eq_mp_fn(); -inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); } - -expr mk_not_imp1_fn(); -inline expr NotImp1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp1_fn(), a, b, H); } - -expr mk_not_imp2_fn(); -inline expr NotImp2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp2_fn(), a, b, H); } - -expr mk_conj_fn(); -inline expr Conj(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_conj_fn(), a, b, H1, H2); } - -expr mk_conjunct1_fn(); -inline expr Conjunct1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct1_fn(), a, b, H); } - -expr mk_conjunct2_fn(); -inline expr Conjunct2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct2_fn(), a, b, H); } - -expr mk_disj1_fn(); -inline expr Disj1(expr const & a, expr const & H, expr const & b) { return mk_app(mk_disj1_fn(), a, H, b); } - -expr mk_disj2_fn(); -inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); } - -expr mk_disj_cases_fn(); -inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); } - -expr mk_refute_fn(); -inline expr Refute(expr const & a, expr const & H) { return mk_app({mk_refute_fn(), a, H}); } - -expr mk_symm_fn(); -inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); } - -expr mk_trans_fn(); -inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); } - -expr mk_eqt_elim_fn(); -inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); } - -expr mk_eqt_intro_fn(); -inline expr EqTIntro(expr const & a, expr const & H) { return mk_app(mk_eqt_intro_fn(), a, H); } - -expr mk_congr1_fn(); -inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); } - -expr mk_congr2_fn(); -inline expr Congr2(expr const & A, expr const & B, expr const & a, expr const & b, expr const & f, expr const & H) { return mk_app({mk_congr2_fn(), A, B, a, b, f, H}); } - -expr mk_congr_fn(); -inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); } - -expr mk_forall_elim_fn(); -inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); } - -expr mk_forall_intro_fn(); -inline expr ForallIntro(expr const & A, expr const & P, expr const & H) { return mk_app(mk_forall_intro_fn(), A, P, H); } - -expr mk_exists_elim_fn(); -inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr const & H1, expr const & H2) { return mk_app({mk_exists_elim_fn(), A, P, B, H1, H2}); } - -expr mk_exists_intro_fn(); -inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); } -class io_state; void import_kernel(environment const & env, io_state const & ios); } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index b6cb3c80c..ec74121b5 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -142,13 +142,13 @@ expr mk_app(unsigned n, expr const * as) { to_app(r)->m_hash = hash_args(new_n, m_args); return r; } -expr_eq::expr_eq(expr const & lhs, expr const & rhs): - expr_cell(expr_kind::Eq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()), +expr_heq::expr_heq(expr const & lhs, expr const & rhs): + expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()), m_lhs(lhs), m_rhs(rhs) { } -expr_eq::~expr_eq() {} -void expr_eq::dealloc(buffer & todelete) { +expr_heq::~expr_heq() {} +void expr_heq::dealloc(buffer & todelete) { dec_ref(m_rhs, todelete); dec_ref(m_lhs, todelete); delete(this); @@ -246,7 +246,7 @@ void expr_cell::dealloc() { case expr_kind::MetaVar: delete static_cast(it); break; case expr_kind::Type: delete static_cast(it); break; case expr_kind::Constant: static_cast(it)->dealloc(todo); break; - case expr_kind::Eq: static_cast(it)->dealloc(todo); break; + case expr_kind::HEq: static_cast(it)->dealloc(todo); break; case expr_kind::App: static_cast(it)->dealloc(todo); break; case expr_kind::Lambda: static_cast(it)->dealloc(todo); break; case expr_kind::Pi: static_cast(it)->dealloc(todo); break; @@ -279,10 +279,10 @@ bool is_arrow(expr const & t) { } } -bool is_eq(expr const & e, expr & lhs, expr & rhs) { - if (is_eq(e)) { - lhs = eq_lhs(e); - rhs = eq_rhs(e); +bool is_heq(expr const & e, expr & lhs, expr & rhs) { + if (is_heq(e)) { + lhs = heq_lhs(e); + rhs = heq_rhs(e); return true; } else { return false; @@ -296,7 +296,7 @@ expr copy(expr const & a) { case expr_kind::Type: return mk_type(ty_level(a)); case expr_kind::Value: return mk_value(static_cast(a.raw())->m_val); case expr_kind::App: return mk_app(num_args(a), begin_args(a)); - case expr_kind::Eq: return mk_eq(eq_lhs(a), eq_rhs(a)); + case expr_kind::HEq: return mk_heq(heq_lhs(a), heq_rhs(a)); case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); @@ -341,7 +341,7 @@ constexpr char g_first_app_size_kind = 32; constexpr char g_small_app_num_args = 32; constexpr bool is_small(expr_kind k) { return 0 <= static_cast(k) && static_cast(k) < g_first_app_size_kind; } static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_small(expr_kind::Value) && is_small(expr_kind::App) && - is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::Eq) && + is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::HEq) && is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big"); class expr_serializer : public object_serializer { @@ -384,7 +384,7 @@ class expr_serializer : public object_serializer const & t); friend expr mk_value(value & v); friend expr mk_app(unsigned num_args, expr const * args); - friend expr mk_eq(expr const & l, expr const & r); + friend expr mk_heq(expr const & l, expr const & r); friend expr mk_lambda(name const & n, expr const & t, expr const & e); friend expr mk_pi(name const & n, expr const & t, expr const & e); friend expr mk_type(level const & l); @@ -215,14 +215,14 @@ public: expr const * end_args() const { return m_args + m_num_args; } }; /** \brief Heterogeneous equality */ -class expr_eq : public expr_cell { +class expr_heq : public expr_cell { expr m_lhs; expr m_rhs; friend class expr_cell; void dealloc(buffer & todelete); public: - expr_eq(expr const & lhs, expr const & rhs); - ~expr_eq(); + expr_heq(expr const & lhs, expr const & rhs); + ~expr_heq(); expr const & get_lhs() const { return m_lhs; } expr const & get_rhs() const { return m_rhs; } }; @@ -392,7 +392,7 @@ inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; } inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; } inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; } -inline bool is_eq(expr_cell * e) { return e->kind() == expr_kind::Eq; } +inline bool is_heq(expr_cell * e) { return e->kind() == expr_kind::HEq; } inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; } inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; } inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; } @@ -404,7 +404,7 @@ inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; } inline bool is_value(expr const & e) { return e.kind() == expr_kind::Value; } inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; } -inline bool is_eq(expr const & e) { return e.kind() == expr_kind::Eq; } +inline bool is_heq(expr const & e) { return e.kind() == expr_kind::HEq; } inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; } inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } bool is_arrow(expr const & e); @@ -431,8 +431,8 @@ inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2}); inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); } inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); } inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); } -inline expr mk_eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r)); } -inline expr Eq(expr const & l, expr const & r) { return mk_eq(l, r); } +inline expr mk_heq(expr const & l, expr const & r) { return expr(new expr_heq(l, r)); } +inline expr HEq(expr const & l, expr const & r) { return mk_heq(l, r); } inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); } inline bool is_default_arrow_var_name(name const & n) { return n == "a"; } @@ -464,7 +464,7 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast(e); } inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast(e); } inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast(e); } -inline expr_eq * to_eq(expr_cell * e) { lean_assert(is_eq(e)); return static_cast(e); } +inline expr_heq * to_heq(expr_cell * e) { lean_assert(is_heq(e)); return static_cast(e); } inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast(e); } inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast(e); } inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast(e); } @@ -475,7 +475,7 @@ inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar inline expr_var * to_var(expr const & e) { return to_var(e.raw()); } inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); } inline expr_app * to_app(expr const & e) { return to_app(e.raw()); } -inline expr_eq * to_eq(expr const & e) { return to_eq(e.raw()); } +inline expr_heq * to_heq(expr const & e) { return to_heq(e.raw()); } inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); } inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.raw()); } inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); } @@ -497,8 +497,8 @@ inline optional const & const_type(expr_cell * e) { return to_constant(e) inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast(e)->get_value(); } inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); } inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); } -inline expr const & eq_lhs(expr_cell * e) { return to_eq(e)->get_lhs(); } -inline expr const & eq_rhs(expr_cell * e) { return to_eq(e)->get_rhs(); } +inline expr const & heq_lhs(expr_cell * e) { return to_heq(e)->get_lhs(); } +inline expr const & heq_rhs(expr_cell * e) { return to_heq(e)->get_rhs(); } inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); } inline expr const & abst_domain(expr_cell * e) { return to_abstraction(e)->get_domain(); } inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); } @@ -530,8 +530,8 @@ inline unsigned num_args(expr const & e) { return to_app(e)->ge inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); } inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); } inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); } -inline expr const & eq_lhs(expr const & e) { return to_eq(e)->get_lhs(); } -inline expr const & eq_rhs(expr const & e) { return to_eq(e)->get_rhs(); } +inline expr const & heq_lhs(expr const & e) { return to_heq(e)->get_lhs(); } +inline expr const & heq_rhs(expr const & e) { return to_heq(e)->get_rhs(); } inline name const & abst_name(expr const & e) { return to_abstraction(e)->get_name(); } inline expr const & abst_domain(expr const & e) { return to_abstraction(e)->get_domain(); } inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); } @@ -545,7 +545,7 @@ inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e) inline bool has_metavar(expr const & e) { return e.has_metavar(); } -bool is_eq(expr const & e, expr & lhs, expr & rhs); +bool is_heq(expr const & e, expr & lhs, expr & rhs); // ======================================= // ======================================= @@ -653,15 +653,15 @@ template expr update_let(expr const & e, F f) { else return e; } -template expr update_eq(expr const & e, F f) { +template expr update_heq(expr const & e, F f) { static_assert(std::is_same::type, std::pair>::value, - "update_eq: return type of f is not pair"); - expr const & old_l = eq_lhs(e); - expr const & old_r = eq_rhs(e); + "update_heq: return type of f is not pair"); + expr const & old_l = heq_lhs(e); + expr const & old_r = heq_rhs(e); std::pair p = f(old_l, old_r); if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r)) - return mk_eq(p.first, p.second); + return mk_heq(p.first, p.second); else return e; } diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 32a3870b1..87259e256 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -64,7 +64,7 @@ class expr_eq_fn { if (!apply(arg(a, i), arg(b, i))) return false; return true; - case expr_kind::Eq: return apply(eq_lhs(a), eq_lhs(b)) && apply(eq_rhs(a), eq_rhs(b)); + case expr_kind::HEq: return apply(heq_lhs(a), heq_lhs(b)) && apply(heq_rhs(a), heq_rhs(b)); case expr_kind::Lambda: // Remark: we ignore get_abs_name because we want alpha-equivalence case expr_kind::Pi: return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b)); case expr_kind::Type: return ty_level(a) == ty_level(b); diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h index d584a9456..37ebad1ac 100644 --- a/src/kernel/for_each_fn.h +++ b/src/kernel/for_each_fn.h @@ -85,9 +85,9 @@ class for_each_fn { } goto begin_loop; } - case expr_kind::Eq: - todo.emplace_back(eq_rhs(e), offset); - todo.emplace_back(eq_lhs(e), offset); + case expr_kind::HEq: + todo.emplace_back(heq_rhs(e), offset); + todo.emplace_back(heq_lhs(e), offset); goto begin_loop; case expr_kind::Lambda: case expr_kind::Pi: diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 8e8fb5dda..67ba0a0e0 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -38,7 +38,7 @@ protected: return true; case expr_kind::Var: return var_idx(e) >= offset; - case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: + case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -76,8 +76,8 @@ protected: case expr_kind::App: result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); break; - case expr_kind::Eq: - result = apply(eq_lhs(e), offset) || apply(eq_rhs(e), offset); + case expr_kind::HEq: + result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); break; case expr_kind::Lambda: case expr_kind::Pi: @@ -166,7 +166,7 @@ class free_var_range_fn { return 0; case expr_kind::Var: return var_idx(e) + 1; - case expr_kind::MetaVar: case expr_kind::App: case expr_kind::Eq: + case expr_kind::MetaVar: case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -199,8 +199,8 @@ class free_var_range_fn { for (auto const & c : args(e)) result = std::max(result, apply(c)); break; - case expr_kind::Eq: - result = std::max(apply(eq_lhs(e)), apply(eq_rhs(e))); + case expr_kind::HEq: + result = std::max(apply(heq_lhs(e)), apply(heq_rhs(e))); break; case expr_kind::Lambda: case expr_kind::Pi: @@ -258,7 +258,7 @@ protected: return true; // assume that any free variable can occur in the metavariable case expr_kind::Var: return var_idx(e) >= offset + m_low && var_idx(e) < offset + m_high; - case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: + case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -297,8 +297,8 @@ protected: case expr_kind::App: result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); break; - case expr_kind::Eq: - result = apply(eq_lhs(e), offset) || apply(eq_rhs(e), offset); + case expr_kind::HEq: + result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); break; case expr_kind::Lambda: case expr_kind::Pi: diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp new file mode 100644 index 000000000..27be7341f --- /dev/null +++ b/src/kernel/kernel_decls.cpp @@ -0,0 +1,96 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/environment.h" +#include "kernel/decl_macros.h" +namespace lean { +MK_CONSTANT(Bool, name("Bool")); +MK_CONSTANT(TypeU, name("TypeU")); +MK_CONSTANT(not_fn, name("not")); +MK_CONSTANT(or_fn, name("or")); +MK_CONSTANT(and_fn, name("and")); +MK_CONSTANT(implies_fn, name("implies")); +MK_CONSTANT(exists_fn, name("exists")); +MK_CONSTANT(eq_fn, name("eq")); +MK_CONSTANT(neq_fn, name("neq")); +MK_CONSTANT(em_fn, name("em")); +MK_CONSTANT(case_fn, name("case")); +MK_CONSTANT(refl_fn, name("refl")); +MK_CONSTANT(subst_fn, name("subst")); +MK_CONSTANT(funext_fn, name("funext")); +MK_CONSTANT(allext_fn, name("allext")); +MK_CONSTANT(substp_fn, name("substp")); +MK_CONSTANT(eta_fn, name("eta")); +MK_CONSTANT(trivial, name("trivial")); +MK_CONSTANT(absurd_fn, name("absurd")); +MK_CONSTANT(eqmp_fn, name("eqmp")); +MK_CONSTANT(boolcomplete_fn, name("boolcomplete")); +MK_CONSTANT(false_elim_fn, name("false_elim")); +MK_CONSTANT(imp_trans_fn, name("imp_trans")); +MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans")); +MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans")); +MK_CONSTANT(not_not_eq_fn, name("not_not_eq")); +MK_CONSTANT(not_not_elim_fn, name("not_not_elim")); +MK_CONSTANT(mt_fn, name("mt")); +MK_CONSTANT(contrapos_fn, name("contrapos")); +MK_CONSTANT(absurd_elim_fn, name("absurd_elim")); +MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml")); +MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr")); +MK_CONSTANT(resolve1_fn, name("resolve1")); +MK_CONSTANT(and_intro_fn, name("and_intro")); +MK_CONSTANT(and_eliml_fn, name("and_eliml")); +MK_CONSTANT(and_elimr_fn, name("and_elimr")); +MK_CONSTANT(or_introl_fn, name("or_introl")); +MK_CONSTANT(or_intror_fn, name("or_intror")); +MK_CONSTANT(or_elim_fn, name("or_elim")); +MK_CONSTANT(refute_fn, name("refute")); +MK_CONSTANT(symm_fn, name("symm")); +MK_CONSTANT(trans_fn, name("trans")); +MK_CONSTANT(ne_symm_fn, name("ne_symm")); +MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans")); +MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans")); +MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); +MK_CONSTANT(congr1_fn, name("congr1")); +MK_CONSTANT(congr2_fn, name("congr2")); +MK_CONSTANT(congr_fn, name("congr")); +MK_CONSTANT(exists_elim_fn, name("exists_elim")); +MK_CONSTANT(exists_intro_fn, name("exists_intro")); +MK_CONSTANT(boolext_fn, name("boolext")); +MK_CONSTANT(iff_intro_fn, name("iff_intro")); +MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); +MK_CONSTANT(or_comm_fn, name("or_comm")); +MK_CONSTANT(or_assoc_fn, name("or_assoc")); +MK_CONSTANT(or_id_fn, name("or_id")); +MK_CONSTANT(or_falsel_fn, name("or_falsel")); +MK_CONSTANT(or_falser_fn, name("or_falser")); +MK_CONSTANT(or_truel_fn, name("or_truel")); +MK_CONSTANT(or_truer_fn, name("or_truer")); +MK_CONSTANT(or_tauto_fn, name("or_tauto")); +MK_CONSTANT(and_comm_fn, name("and_comm")); +MK_CONSTANT(and_id_fn, name("and_id")); +MK_CONSTANT(and_assoc_fn, name("and_assoc")); +MK_CONSTANT(and_truer_fn, name("and_truer")); +MK_CONSTANT(and_truel_fn, name("and_truel")); +MK_CONSTANT(and_falsel_fn, name("and_falsel")); +MK_CONSTANT(and_falser_fn, name("and_falser")); +MK_CONSTANT(and_absurd_fn, name("and_absurd")); +MK_CONSTANT(not_and_fn, name("not_and")); +MK_CONSTANT(not_and_elim_fn, name("not_and_elim")); +MK_CONSTANT(not_or_fn, name("not_or")); +MK_CONSTANT(not_or_elim_fn, name("not_or_elim")); +MK_CONSTANT(not_iff_fn, name("not_iff")); +MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim")); +MK_CONSTANT(not_implies_fn, name("not_implies")); +MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim")); +MK_CONSTANT(not_congr_fn, name("not_congr")); +MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro")); +MK_CONSTANT(not_forall_fn, name("not_forall")); +MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim")); +MK_CONSTANT(not_exists_fn, name("not_exists")); +MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim")); +MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1")); +MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2")); +MK_CONSTANT(exists_unfold_fn, name("exists_unfold")); +} diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h new file mode 100644 index 000000000..aea60526a --- /dev/null +++ b/src/kernel/kernel_decls.h @@ -0,0 +1,273 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/expr.h" +namespace lean { +expr mk_Bool(); +bool is_Bool(expr const & e); +expr mk_TypeU(); +bool is_TypeU(expr const & e); +expr mk_not_fn(); +bool is_not_fn(expr const & e); +inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); } +inline expr mk_not(expr const & e1) { return mk_app({mk_not_fn(), e1}); } +expr mk_or_fn(); +bool is_or_fn(expr const & e); +inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); } +inline expr mk_or(expr const & e1, expr const & e2) { return mk_app({mk_or_fn(), e1, e2}); } +expr mk_and_fn(); +bool is_and_fn(expr const & e); +inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); } +inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); } +expr mk_implies_fn(); +bool is_implies_fn(expr const & e); +inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); } +inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); } +expr mk_exists_fn(); +bool is_exists_fn(expr const & e); +inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); } +inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); } +expr mk_eq_fn(); +bool is_eq_fn(expr const & e); +inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); } +inline expr mk_eq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_fn(), e1, e2, e3}); } +expr mk_neq_fn(); +bool is_neq_fn(expr const & e); +inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); } +inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); } +expr mk_em_fn(); +bool is_em_fn(expr const & e); +inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); } +expr mk_case_fn(); +bool is_case_fn(expr const & e); +inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); } +expr mk_refl_fn(); +bool is_refl_fn(expr const & e); +inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); } +expr mk_subst_fn(); +bool is_subst_fn(expr const & e); +inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_funext_fn(); +bool is_funext_fn(expr const & e); +inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); } +expr mk_allext_fn(); +bool is_allext_fn(expr const & e); +inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); } +expr mk_substp_fn(); +bool is_substp_fn(expr const & e); +inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eta_fn(); +bool is_eta_fn(expr const & e); +inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); } +expr mk_trivial(); +bool is_trivial(expr const & e); +expr mk_absurd_fn(); +bool is_absurd_fn(expr const & e); +inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); } +expr mk_eqmp_fn(); +bool is_eqmp_fn(expr const & e); +inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); } +expr mk_boolcomplete_fn(); +bool is_boolcomplete_fn(expr const & e); +inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); } +expr mk_false_elim_fn(); +bool is_false_elim_fn(expr const & e); +inline expr mk_false_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_false_elim_fn(), e1, e2}); } +expr mk_imp_trans_fn(); +bool is_imp_trans_fn(expr const & e); +inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_imp_eq_trans_fn(); +bool is_imp_eq_trans_fn(expr const & e); +inline expr mk_imp_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eq_imp_trans_fn(); +bool is_eq_imp_trans_fn(expr const & e); +inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_not_not_eq_fn(); +bool is_not_not_eq_fn(expr const & e); +inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); } +expr mk_not_not_elim_fn(); +bool is_not_not_elim_fn(expr const & e); +inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); } +expr mk_mt_fn(); +bool is_mt_fn(expr const & e); +inline expr mk_mt_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_mt_fn(), e1, e2, e3, e4}); } +expr mk_contrapos_fn(); +bool is_contrapos_fn(expr const & e); +inline expr mk_contrapos_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_contrapos_fn(), e1, e2, e3, e4}); } +expr mk_absurd_elim_fn(); +bool is_absurd_elim_fn(expr const & e); +inline expr mk_absurd_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_absurd_elim_fn(), e1, e2, e3, e4}); } +expr mk_not_imp_eliml_fn(); +bool is_not_imp_eliml_fn(expr const & e); +inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); } +expr mk_not_imp_elimr_fn(); +bool is_not_imp_elimr_fn(expr const & e); +inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); } +expr mk_resolve1_fn(); +bool is_resolve1_fn(expr const & e); +inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); } +expr mk_and_intro_fn(); +bool is_and_intro_fn(expr const & e); +inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); } +expr mk_and_eliml_fn(); +bool is_and_eliml_fn(expr const & e); +inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); } +expr mk_and_elimr_fn(); +bool is_and_elimr_fn(expr const & e); +inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); } +expr mk_or_introl_fn(); +bool is_or_introl_fn(expr const & e); +inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_introl_fn(), e1, e2, e3}); } +expr mk_or_intror_fn(); +bool is_or_intror_fn(expr const & e); +inline expr mk_or_intror_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_intror_fn(), e1, e2, e3}); } +expr mk_or_elim_fn(); +bool is_or_elim_fn(expr const & e); +inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_refute_fn(); +bool is_refute_fn(expr const & e); +inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); } +expr mk_symm_fn(); +bool is_symm_fn(expr const & e); +inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_symm_fn(), e1, e2, e3, e4}); } +expr mk_trans_fn(); +bool is_trans_fn(expr const & e); +inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_ne_symm_fn(); +bool is_ne_symm_fn(expr const & e); +inline expr mk_ne_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ne_symm_fn(), e1, e2, e3, e4}); } +expr mk_eq_ne_trans_fn(); +bool is_eq_ne_trans_fn(expr const & e); +inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_ne_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_ne_eq_trans_fn(); +bool is_ne_eq_trans_fn(expr const & e); +inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eqt_elim_fn(); +bool is_eqt_elim_fn(expr const & e); +inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); } +expr mk_congr1_fn(); +bool is_congr1_fn(expr const & e); +inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_congr2_fn(); +bool is_congr2_fn(expr const & e); +inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_congr_fn(); +bool is_congr_fn(expr const & e); +inline expr mk_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_exists_elim_fn(); +bool is_exists_elim_fn(expr const & e); +inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); } +expr mk_exists_intro_fn(); +bool is_exists_intro_fn(expr const & e); +inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); } +expr mk_boolext_fn(); +bool is_boolext_fn(expr const & e); +inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); } +expr mk_iff_intro_fn(); +bool is_iff_intro_fn(expr const & e); +inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); } +expr mk_eqt_intro_fn(); +bool is_eqt_intro_fn(expr const & e); +inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); } +expr mk_or_comm_fn(); +bool is_or_comm_fn(expr const & e); +inline expr mk_or_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_or_comm_fn(), e1, e2}); } +expr mk_or_assoc_fn(); +bool is_or_assoc_fn(expr const & e); +inline expr mk_or_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_assoc_fn(), e1, e2, e3}); } +expr mk_or_id_fn(); +bool is_or_id_fn(expr const & e); +inline expr mk_or_id_th(expr const & e1) { return mk_app({mk_or_id_fn(), e1}); } +expr mk_or_falsel_fn(); +bool is_or_falsel_fn(expr const & e); +inline expr mk_or_falsel_th(expr const & e1) { return mk_app({mk_or_falsel_fn(), e1}); } +expr mk_or_falser_fn(); +bool is_or_falser_fn(expr const & e); +inline expr mk_or_falser_th(expr const & e1) { return mk_app({mk_or_falser_fn(), e1}); } +expr mk_or_truel_fn(); +bool is_or_truel_fn(expr const & e); +inline expr mk_or_truel_th(expr const & e1) { return mk_app({mk_or_truel_fn(), e1}); } +expr mk_or_truer_fn(); +bool is_or_truer_fn(expr const & e); +inline expr mk_or_truer_th(expr const & e1) { return mk_app({mk_or_truer_fn(), e1}); } +expr mk_or_tauto_fn(); +bool is_or_tauto_fn(expr const & e); +inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e1}); } +expr mk_and_comm_fn(); +bool is_and_comm_fn(expr const & e); +inline expr mk_and_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_and_comm_fn(), e1, e2}); } +expr mk_and_id_fn(); +bool is_and_id_fn(expr const & e); +inline expr mk_and_id_th(expr const & e1) { return mk_app({mk_and_id_fn(), e1}); } +expr mk_and_assoc_fn(); +bool is_and_assoc_fn(expr const & e); +inline expr mk_and_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_assoc_fn(), e1, e2, e3}); } +expr mk_and_truer_fn(); +bool is_and_truer_fn(expr const & e); +inline expr mk_and_truer_th(expr const & e1) { return mk_app({mk_and_truer_fn(), e1}); } +expr mk_and_truel_fn(); +bool is_and_truel_fn(expr const & e); +inline expr mk_and_truel_th(expr const & e1) { return mk_app({mk_and_truel_fn(), e1}); } +expr mk_and_falsel_fn(); +bool is_and_falsel_fn(expr const & e); +inline expr mk_and_falsel_th(expr const & e1) { return mk_app({mk_and_falsel_fn(), e1}); } +expr mk_and_falser_fn(); +bool is_and_falser_fn(expr const & e); +inline expr mk_and_falser_th(expr const & e1) { return mk_app({mk_and_falser_fn(), e1}); } +expr mk_and_absurd_fn(); +bool is_and_absurd_fn(expr const & e); +inline expr mk_and_absurd_th(expr const & e1) { return mk_app({mk_and_absurd_fn(), e1}); } +expr mk_not_and_fn(); +bool is_not_and_fn(expr const & e); +inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); } +expr mk_not_and_elim_fn(); +bool is_not_and_elim_fn(expr const & e); +inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); } +expr mk_not_or_fn(); +bool is_not_or_fn(expr const & e); +inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); } +expr mk_not_or_elim_fn(); +bool is_not_or_elim_fn(expr const & e); +inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); } +expr mk_not_iff_fn(); +bool is_not_iff_fn(expr const & e); +inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); } +expr mk_not_iff_elim_fn(); +bool is_not_iff_elim_fn(expr const & e); +inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); } +expr mk_not_implies_fn(); +bool is_not_implies_fn(expr const & e); +inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); } +expr mk_not_implies_elim_fn(); +bool is_not_implies_elim_fn(expr const & e); +inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); } +expr mk_not_congr_fn(); +bool is_not_congr_fn(expr const & e); +inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); } +expr mk_eq_exists_intro_fn(); +bool is_eq_exists_intro_fn(expr const & e); +inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); } +expr mk_not_forall_fn(); +bool is_not_forall_fn(expr const & e); +inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); } +expr mk_not_forall_elim_fn(); +bool is_not_forall_elim_fn(expr const & e); +inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); } +expr mk_not_exists_fn(); +bool is_not_exists_fn(expr const & e); +inline expr mk_not_exists_th(expr const & e1, expr const & e2) { return mk_app({mk_not_exists_fn(), e1, e2}); } +expr mk_not_exists_elim_fn(); +bool is_not_exists_elim_fn(expr const & e); +inline expr mk_not_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_exists_elim_fn(), e1, e2, e3, e4}); } +expr mk_exists_unfold1_fn(); +bool is_exists_unfold1_fn(expr const & e); +inline expr mk_exists_unfold1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_unfold1_fn(), e1, e2, e3, e4}); } +expr mk_exists_unfold2_fn(); +bool is_exists_unfold2_fn(expr const & e); +inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_unfold2_fn(), e1, e2, e3, e4}); } +expr mk_exists_unfold_fn(); +bool is_exists_unfold_fn(expr const & e); +inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); } +} diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index 0e7f3e74a..cbe3de1f2 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -56,8 +56,8 @@ struct max_sharing_fn::imp { cache(r); return r; } - case expr_kind::Eq : { - expr r = update_eq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); }); + case expr_kind::HEq : { + expr r = update_heq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); }); cache(r); return r; } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 56924293c..f4c80ca98 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -309,13 +309,13 @@ class normalizer::imp { } break; } - case expr_kind::Eq: { - expr new_lhs = normalize(eq_lhs(a), s, k); - expr new_rhs = normalize(eq_rhs(a), s, k); + case expr_kind::HEq: { + expr new_lhs = normalize(heq_lhs(a), s, k); + expr new_rhs = normalize(heq_rhs(a), s, k); if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs) && typeid(to_value(new_lhs)) == typeid(to_value(new_rhs))) { r = mk_bool_value(new_lhs == new_rhs); } else { - r = mk_eq(new_lhs, new_rhs); + r = mk_heq(new_lhs, new_rhs); } break; } diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index e9cff162c..c78f84ce8 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -156,12 +156,12 @@ public: pop_rs(num); break; } - case expr_kind::Eq: - if (check_index(f, 0) && !visit(eq_lhs(e), offset)) + case expr_kind::HEq: + if (check_index(f, 0) && !visit(heq_lhs(e), offset)) goto begin_loop; - if (check_index(f, 1) && !visit(eq_rhs(e), offset)) + if (check_index(f, 1) && !visit(heq_rhs(e), offset)) goto begin_loop; - r = update_eq(e, rs(-2), rs(-1)); + r = update_heq(e, rs(-2), rs(-1)); pop_rs(2); break; case expr_kind::Pi: case expr_kind::Lambda: diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 32343f03c..d177ab780 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -22,9 +22,9 @@ expr replace_visitor::visit_app(expr const & e, context const & ctx) { lean_assert(is_app(e)); return update_app(e, [&](expr const & c) { return visit(c, ctx); }); } -expr replace_visitor::visit_eq(expr const & e, context const & ctx) { - lean_assert(is_eq(e)); - return update_eq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); }); +expr replace_visitor::visit_heq(expr const & e, context const & ctx) { + lean_assert(is_heq(e)); + return update_heq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); }); } expr replace_visitor::visit_abst(expr const & e, context const & ctx) { lean_assert(is_abstraction(e)); @@ -80,7 +80,7 @@ expr replace_visitor::visit(expr const & e, context const & ctx) { case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared); case expr_kind::MetaVar: return save_result(e, visit_metavar(e, ctx), shared); case expr_kind::App: return save_result(e, visit_app(e, ctx), shared); - case expr_kind::Eq: return save_result(e, visit_eq(e, ctx), shared); + case expr_kind::HEq: return save_result(e, visit_heq(e, ctx), shared); case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared); case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared); case expr_kind::Let: return save_result(e, visit_let(e, ctx), shared); diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index f3f139040..ac74a9afb 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -31,7 +31,7 @@ protected: virtual expr visit_var(expr const &, context const &); virtual expr visit_metavar(expr const &, context const &); virtual expr visit_app(expr const &, context const &); - virtual expr visit_eq(expr const &, context const &); + virtual expr visit_heq(expr const &, context const &); virtual expr visit_abst(expr const &, context const &); virtual expr visit_lambda(expr const &, context const &); virtual expr visit_pi(expr const &, context const &); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 743d69830..46da9c1c0 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -176,7 +176,7 @@ class type_checker::imp { } case expr_kind::Type: return mk_type(ty_level(e) + 1); - case expr_kind::Eq: + case expr_kind::HEq: // cheap when we are just inferring types if (m_infer_only) return mk_bool_type(); @@ -241,10 +241,10 @@ class type_checker::imp { f_t = check_pi(f_t, e, ctx); } } - case expr_kind::Eq: + case expr_kind::HEq: lean_assert(!m_infer_only); - infer_type_core(eq_lhs(e), ctx); - infer_type_core(eq_rhs(e), ctx); + infer_type_core(heq_lhs(e), ctx); + infer_type_core(heq_rhs(e), ctx); return save_result(e, mk_bool_type(), shared); case expr_kind::Lambda: if (!m_infer_only) { @@ -422,7 +422,7 @@ public: // Catch easy cases switch (e.kind()) { case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false; - case expr_kind::Eq: return true; + case expr_kind::HEq: return true; default: break; } expr t = infer_type(e, ctx, menv, nullptr); diff --git a/src/kernel/update_expr.cpp b/src/kernel/update_expr.cpp index c3de8d9d8..1bbacf582 100644 --- a/src/kernel/update_expr.cpp +++ b/src/kernel/update_expr.cpp @@ -67,10 +67,10 @@ expr update_let(expr const & let, optional const & t, expr const & v, expr return mk_let(let_name(let), t, v, b); } -expr update_eq(expr const & eq, expr const & l, expr const & r) { - if (is_eqp(eq_lhs(eq), l) && is_eqp(eq_rhs(eq), r)) +expr update_heq(expr const & eq, expr const & l, expr const & r) { + if (is_eqp(heq_lhs(eq), l) && is_eqp(heq_rhs(eq), r)) return eq; else - return mk_eq(l, r); + return mk_heq(l, r); } } diff --git a/src/kernel/update_expr.h b/src/kernel/update_expr.h index 5836c6f08..b693f45b7 100644 --- a/src/kernel/update_expr.h +++ b/src/kernel/update_expr.h @@ -43,5 +43,5 @@ expr update_let(expr const & let, optional const & t, expr const & v, expr \remark Return \c eq if the given lhs and rhs are (pointer) equal to the ones in \c eq. */ -expr update_eq(expr const & eq, expr const & l, expr const & r); +expr update_heq(expr const & eq, expr const & l, expr const & r); } diff --git a/src/library/arith/Int_decls.cpp b/src/library/arith/Int_decls.cpp new file mode 100644 index 000000000..53b120c91 --- /dev/null +++ b/src/library/arith/Int_decls.cpp @@ -0,0 +1,20 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/environment.h" +#include "kernel/decl_macros.h" +namespace lean { +MK_CONSTANT(Int, name("Int")); +MK_CONSTANT(Int_ge_fn, name({"Int", "ge"})); +MK_CONSTANT(Int_lt_fn, name({"Int", "lt"})); +MK_CONSTANT(Int_gt_fn, name({"Int", "gt"})); +MK_CONSTANT(Int_sub_fn, name({"Int", "sub"})); +MK_CONSTANT(Int_neg_fn, name({"Int", "neg"})); +MK_CONSTANT(Int_mod_fn, name({"Int", "mod"})); +MK_CONSTANT(Int_divides_fn, name({"Int", "divides"})); +MK_CONSTANT(Int_abs_fn, name({"Int", "abs"})); +MK_CONSTANT(Nat_sub_fn, name({"Nat", "sub"})); +MK_CONSTANT(Nat_neg_fn, name({"Nat", "neg"})); +} diff --git a/src/library/arith/Int_decls.h b/src/library/arith/Int_decls.h new file mode 100644 index 000000000..77b1583e6 --- /dev/null +++ b/src/library/arith/Int_decls.h @@ -0,0 +1,50 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/expr.h" +namespace lean { +expr mk_Int(); +bool is_Int(expr const & e); +expr mk_Int_ge_fn(); +bool is_Int_ge_fn(expr const & e); +inline bool is_Int_ge(expr const & e) { return is_app(e) && is_Int_ge_fn(arg(e, 0)); } +inline expr mk_Int_ge(expr const & e1, expr const & e2) { return mk_app({mk_Int_ge_fn(), e1, e2}); } +expr mk_Int_lt_fn(); +bool is_Int_lt_fn(expr const & e); +inline bool is_Int_lt(expr const & e) { return is_app(e) && is_Int_lt_fn(arg(e, 0)); } +inline expr mk_Int_lt(expr const & e1, expr const & e2) { return mk_app({mk_Int_lt_fn(), e1, e2}); } +expr mk_Int_gt_fn(); +bool is_Int_gt_fn(expr const & e); +inline bool is_Int_gt(expr const & e) { return is_app(e) && is_Int_gt_fn(arg(e, 0)); } +inline expr mk_Int_gt(expr const & e1, expr const & e2) { return mk_app({mk_Int_gt_fn(), e1, e2}); } +expr mk_Int_sub_fn(); +bool is_Int_sub_fn(expr const & e); +inline bool is_Int_sub(expr const & e) { return is_app(e) && is_Int_sub_fn(arg(e, 0)); } +inline expr mk_Int_sub(expr const & e1, expr const & e2) { return mk_app({mk_Int_sub_fn(), e1, e2}); } +expr mk_Int_neg_fn(); +bool is_Int_neg_fn(expr const & e); +inline bool is_Int_neg(expr const & e) { return is_app(e) && is_Int_neg_fn(arg(e, 0)); } +inline expr mk_Int_neg(expr const & e1) { return mk_app({mk_Int_neg_fn(), e1}); } +expr mk_Int_mod_fn(); +bool is_Int_mod_fn(expr const & e); +inline bool is_Int_mod(expr const & e) { return is_app(e) && is_Int_mod_fn(arg(e, 0)); } +inline expr mk_Int_mod(expr const & e1, expr const & e2) { return mk_app({mk_Int_mod_fn(), e1, e2}); } +expr mk_Int_divides_fn(); +bool is_Int_divides_fn(expr const & e); +inline bool is_Int_divides(expr const & e) { return is_app(e) && is_Int_divides_fn(arg(e, 0)); } +inline expr mk_Int_divides(expr const & e1, expr const & e2) { return mk_app({mk_Int_divides_fn(), e1, e2}); } +expr mk_Int_abs_fn(); +bool is_Int_abs_fn(expr const & e); +inline bool is_Int_abs(expr const & e) { return is_app(e) && is_Int_abs_fn(arg(e, 0)); } +inline expr mk_Int_abs(expr const & e1) { return mk_app({mk_Int_abs_fn(), e1}); } +expr mk_Nat_sub_fn(); +bool is_Nat_sub_fn(expr const & e); +inline bool is_Nat_sub(expr const & e) { return is_app(e) && is_Nat_sub_fn(arg(e, 0)); } +inline expr mk_Nat_sub(expr const & e1, expr const & e2) { return mk_app({mk_Nat_sub_fn(), e1, e2}); } +expr mk_Nat_neg_fn(); +bool is_Nat_neg_fn(expr const & e); +inline bool is_Nat_neg(expr const & e) { return is_app(e) && is_Nat_neg_fn(arg(e, 0)); } +inline expr mk_Nat_neg(expr const & e1) { return mk_app({mk_Nat_neg_fn(), e1}); } +} diff --git a/src/library/arith/Nat_decls.cpp b/src/library/arith/Nat_decls.cpp new file mode 100644 index 000000000..4eff54b54 --- /dev/null +++ b/src/library/arith/Nat_decls.cpp @@ -0,0 +1,45 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/environment.h" +#include "kernel/decl_macros.h" +namespace lean { +MK_CONSTANT(Nat, name("Nat")); +MK_CONSTANT(Nat_ge_fn, name({"Nat", "ge"})); +MK_CONSTANT(Nat_lt_fn, name({"Nat", "lt"})); +MK_CONSTANT(Nat_gt_fn, name({"Nat", "gt"})); +MK_CONSTANT(Nat_id_fn, name({"Nat", "id"})); +MK_CONSTANT(Nat_succ_nz_fn, name({"Nat", "succ_nz"})); +MK_CONSTANT(Nat_succ_inj_fn, name({"Nat", "succ_inj"})); +MK_CONSTANT(Nat_add_zeror_fn, name({"Nat", "add_zeror"})); +MK_CONSTANT(Nat_add_succr_fn, name({"Nat", "add_succr"})); +MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"})); +MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"})); +MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"})); +MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"})); +MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"})); +MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"})); +MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"})); +MK_CONSTANT(Nat_add_succl_fn, name({"Nat", "add_succl"})); +MK_CONSTANT(Nat_add_comm_fn, name({"Nat", "add_comm"})); +MK_CONSTANT(Nat_add_assoc_fn, name({"Nat", "add_assoc"})); +MK_CONSTANT(Nat_mul_zerol_fn, name({"Nat", "mul_zerol"})); +MK_CONSTANT(Nat_mul_succl_fn, name({"Nat", "mul_succl"})); +MK_CONSTANT(Nat_mul_onel_fn, name({"Nat", "mul_onel"})); +MK_CONSTANT(Nat_mul_oner_fn, name({"Nat", "mul_oner"})); +MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"})); +MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"})); +MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"})); +MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"})); +MK_CONSTANT(Nat_add_inj_fn, name({"Nat", "add_inj"})); +MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"})); +MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"})); +MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"})); +MK_CONSTANT(Nat_le_refl_fn, name({"Nat", "le_refl"})); +MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"})); +MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"})); +MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"})); +MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"})); +} diff --git a/src/library/arith/Nat_decls.h b/src/library/arith/Nat_decls.h new file mode 100644 index 000000000..fa0830b87 --- /dev/null +++ b/src/library/arith/Nat_decls.h @@ -0,0 +1,119 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/expr.h" +namespace lean { +expr mk_Nat(); +bool is_Nat(expr const & e); +expr mk_Nat_ge_fn(); +bool is_Nat_ge_fn(expr const & e); +inline bool is_Nat_ge(expr const & e) { return is_app(e) && is_Nat_ge_fn(arg(e, 0)); } +inline expr mk_Nat_ge(expr const & e1, expr const & e2) { return mk_app({mk_Nat_ge_fn(), e1, e2}); } +expr mk_Nat_lt_fn(); +bool is_Nat_lt_fn(expr const & e); +inline bool is_Nat_lt(expr const & e) { return is_app(e) && is_Nat_lt_fn(arg(e, 0)); } +inline expr mk_Nat_lt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_lt_fn(), e1, e2}); } +expr mk_Nat_gt_fn(); +bool is_Nat_gt_fn(expr const & e); +inline bool is_Nat_gt(expr const & e) { return is_app(e) && is_Nat_gt_fn(arg(e, 0)); } +inline expr mk_Nat_gt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_gt_fn(), e1, e2}); } +expr mk_Nat_id_fn(); +bool is_Nat_id_fn(expr const & e); +inline bool is_Nat_id(expr const & e) { return is_app(e) && is_Nat_id_fn(arg(e, 0)); } +inline expr mk_Nat_id(expr const & e1) { return mk_app({mk_Nat_id_fn(), e1}); } +expr mk_Nat_succ_nz_fn(); +bool is_Nat_succ_nz_fn(expr const & e); +inline expr mk_Nat_succ_nz_th(expr const & e1) { return mk_app({mk_Nat_succ_nz_fn(), e1}); } +expr mk_Nat_succ_inj_fn(); +bool is_Nat_succ_inj_fn(expr const & e); +inline expr mk_Nat_succ_inj_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_succ_inj_fn(), e1, e2, e3}); } +expr mk_Nat_add_zeror_fn(); +bool is_Nat_add_zeror_fn(expr const & e); +inline expr mk_Nat_add_zeror_th(expr const & e1) { return mk_app({mk_Nat_add_zeror_fn(), e1}); } +expr mk_Nat_add_succr_fn(); +bool is_Nat_add_succr_fn(expr const & e); +inline expr mk_Nat_add_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succr_fn(), e1, e2}); } +expr mk_Nat_mul_zeror_fn(); +bool is_Nat_mul_zeror_fn(expr const & e); +inline expr mk_Nat_mul_zeror_th(expr const & e1) { return mk_app({mk_Nat_mul_zeror_fn(), e1}); } +expr mk_Nat_mul_succr_fn(); +bool is_Nat_mul_succr_fn(expr const & e); +inline expr mk_Nat_mul_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succr_fn(), e1, e2}); } +expr mk_Nat_le_def_fn(); +bool is_Nat_le_def_fn(expr const & e); +inline expr mk_Nat_le_def_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_le_def_fn(), e1, e2}); } +expr mk_Nat_induction_fn(); +bool is_Nat_induction_fn(expr const & e); +inline expr mk_Nat_induction_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_fn(), e1, e2, e3, e4}); } +expr mk_Nat_pred_nz_fn(); +bool is_Nat_pred_nz_fn(expr const & e); +inline expr mk_Nat_pred_nz_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_pred_nz_fn(), e1, e2}); } +expr mk_Nat_discriminate_fn(); +bool is_Nat_discriminate_fn(expr const & e); +inline expr mk_Nat_discriminate_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_discriminate_fn(), e1, e2, e3, e4}); } +expr mk_Nat_add_zerol_fn(); +bool is_Nat_add_zerol_fn(expr const & e); +inline expr mk_Nat_add_zerol_th(expr const & e1) { return mk_app({mk_Nat_add_zerol_fn(), e1}); } +expr mk_Nat_add_succl_fn(); +bool is_Nat_add_succl_fn(expr const & e); +inline expr mk_Nat_add_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succl_fn(), e1, e2}); } +expr mk_Nat_add_comm_fn(); +bool is_Nat_add_comm_fn(expr const & e); +inline expr mk_Nat_add_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_comm_fn(), e1, e2}); } +expr mk_Nat_add_assoc_fn(); +bool is_Nat_add_assoc_fn(expr const & e); +inline expr mk_Nat_add_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_assoc_fn(), e1, e2, e3}); } +expr mk_Nat_mul_zerol_fn(); +bool is_Nat_mul_zerol_fn(expr const & e); +inline expr mk_Nat_mul_zerol_th(expr const & e1) { return mk_app({mk_Nat_mul_zerol_fn(), e1}); } +expr mk_Nat_mul_succl_fn(); +bool is_Nat_mul_succl_fn(expr const & e); +inline expr mk_Nat_mul_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succl_fn(), e1, e2}); } +expr mk_Nat_mul_onel_fn(); +bool is_Nat_mul_onel_fn(expr const & e); +inline expr mk_Nat_mul_onel_th(expr const & e1) { return mk_app({mk_Nat_mul_onel_fn(), e1}); } +expr mk_Nat_mul_oner_fn(); +bool is_Nat_mul_oner_fn(expr const & e); +inline expr mk_Nat_mul_oner_th(expr const & e1) { return mk_app({mk_Nat_mul_oner_fn(), e1}); } +expr mk_Nat_mul_comm_fn(); +bool is_Nat_mul_comm_fn(expr const & e); +inline expr mk_Nat_mul_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_comm_fn(), e1, e2}); } +expr mk_Nat_distributer_fn(); +bool is_Nat_distributer_fn(expr const & e); +inline expr mk_Nat_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributer_fn(), e1, e2, e3}); } +expr mk_Nat_distributel_fn(); +bool is_Nat_distributel_fn(expr const & e); +inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributel_fn(), e1, e2, e3}); } +expr mk_Nat_mul_assoc_fn(); +bool is_Nat_mul_assoc_fn(expr const & e); +inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); } +expr mk_Nat_add_inj_fn(); +bool is_Nat_add_inj_fn(expr const & e); +inline expr mk_Nat_add_inj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_inj_fn(), e1, e2, e3, e4}); } +expr mk_Nat_add_eqz_fn(); +bool is_Nat_add_eqz_fn(expr const & e); +inline expr mk_Nat_add_eqz_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_eqz_fn(), e1, e2, e3}); } +expr mk_Nat_le_intro_fn(); +bool is_Nat_le_intro_fn(expr const & e); +inline expr mk_Nat_le_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_intro_fn(), e1, e2, e3, e4}); } +expr mk_Nat_le_elim_fn(); +bool is_Nat_le_elim_fn(expr const & e); +inline expr mk_Nat_le_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_le_elim_fn(), e1, e2, e3}); } +expr mk_Nat_le_refl_fn(); +bool is_Nat_le_refl_fn(expr const & e); +inline expr mk_Nat_le_refl_th(expr const & e1) { return mk_app({mk_Nat_le_refl_fn(), e1}); } +expr mk_Nat_le_zero_fn(); +bool is_Nat_le_zero_fn(expr const & e); +inline expr mk_Nat_le_zero_th(expr const & e1) { return mk_app({mk_Nat_le_zero_fn(), e1}); } +expr mk_Nat_le_trans_fn(); +bool is_Nat_le_trans_fn(expr const & e); +inline expr mk_Nat_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_trans_fn(), e1, e2, e3, e4, e5}); } +expr mk_Nat_le_add_fn(); +bool is_Nat_le_add_fn(expr const & e); +inline expr mk_Nat_le_add_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_add_fn(), e1, e2, e3, e4}); } +expr mk_Nat_le_antisym_fn(); +bool is_Nat_le_antisym_fn(expr const & e); +inline expr mk_Nat_le_antisym_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_antisym_fn(), e1, e2, e3, e4}); } +} diff --git a/src/library/arith/Real_decls.cpp b/src/library/arith/Real_decls.cpp new file mode 100644 index 000000000..e4b8f173c --- /dev/null +++ b/src/library/arith/Real_decls.cpp @@ -0,0 +1,17 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/environment.h" +#include "kernel/decl_macros.h" +namespace lean { +MK_CONSTANT(Real, name("Real")); +MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); +MK_CONSTANT(Real_ge_fn, name({"Real", "ge"})); +MK_CONSTANT(Real_lt_fn, name({"Real", "lt"})); +MK_CONSTANT(Real_gt_fn, name({"Real", "gt"})); +MK_CONSTANT(Real_sub_fn, name({"Real", "sub"})); +MK_CONSTANT(Real_neg_fn, name({"Real", "neg"})); +MK_CONSTANT(Real_abs_fn, name({"Real", "abs"})); +} diff --git a/src/library/arith/Real_decls.h b/src/library/arith/Real_decls.h new file mode 100644 index 000000000..b792be274 --- /dev/null +++ b/src/library/arith/Real_decls.h @@ -0,0 +1,38 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/expr.h" +namespace lean { +expr mk_Real(); +bool is_Real(expr const & e); +expr mk_nat_to_real_fn(); +bool is_nat_to_real_fn(expr const & e); +inline bool is_nat_to_real(expr const & e) { return is_app(e) && is_nat_to_real_fn(arg(e, 0)); } +inline expr mk_nat_to_real(expr const & e1) { return mk_app({mk_nat_to_real_fn(), e1}); } +expr mk_Real_ge_fn(); +bool is_Real_ge_fn(expr const & e); +inline bool is_Real_ge(expr const & e) { return is_app(e) && is_Real_ge_fn(arg(e, 0)); } +inline expr mk_Real_ge(expr const & e1, expr const & e2) { return mk_app({mk_Real_ge_fn(), e1, e2}); } +expr mk_Real_lt_fn(); +bool is_Real_lt_fn(expr const & e); +inline bool is_Real_lt(expr const & e) { return is_app(e) && is_Real_lt_fn(arg(e, 0)); } +inline expr mk_Real_lt(expr const & e1, expr const & e2) { return mk_app({mk_Real_lt_fn(), e1, e2}); } +expr mk_Real_gt_fn(); +bool is_Real_gt_fn(expr const & e); +inline bool is_Real_gt(expr const & e) { return is_app(e) && is_Real_gt_fn(arg(e, 0)); } +inline expr mk_Real_gt(expr const & e1, expr const & e2) { return mk_app({mk_Real_gt_fn(), e1, e2}); } +expr mk_Real_sub_fn(); +bool is_Real_sub_fn(expr const & e); +inline bool is_Real_sub(expr const & e) { return is_app(e) && is_Real_sub_fn(arg(e, 0)); } +inline expr mk_Real_sub(expr const & e1, expr const & e2) { return mk_app({mk_Real_sub_fn(), e1, e2}); } +expr mk_Real_neg_fn(); +bool is_Real_neg_fn(expr const & e); +inline bool is_Real_neg(expr const & e) { return is_app(e) && is_Real_neg_fn(arg(e, 0)); } +inline expr mk_Real_neg(expr const & e1) { return mk_app({mk_Real_neg_fn(), e1}); } +expr mk_Real_abs_fn(); +bool is_Real_abs_fn(expr const & e); +inline bool is_Real_abs(expr const & e) { return is_app(e) && is_Real_abs_fn(arg(e, 0)); } +inline expr mk_Real_abs(expr const & e1) { return mk_app({mk_Real_abs_fn(), e1}); } +} diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 2c1a308cb..939370059 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -13,9 +13,11 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" #include "library/arith/int.h" #include "library/arith/nat.h" +#include "library/arith/Int_decls.cpp" namespace lean { -MK_CONSTANT(Int, "Int"); +expr mk_nat_to_int_fn(); + expr const Int = mk_Int(); expr mk_int_type() { return mk_Int(); } @@ -84,16 +86,16 @@ public: constexpr char int_add_name[] = "add"; struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; }; typedef int_bin_op int_add_value; -MK_BUILTIN(int_add_fn, int_add_value); -static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_int_add_fn(); }); -static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); }); +MK_BUILTIN(Int_add_fn, int_add_value); +static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_Int_add_fn(); }); +static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_Int_add_fn(); }); constexpr char int_mul_name[] = "mul"; struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; }; typedef int_bin_op int_mul_value; -MK_BUILTIN(int_mul_fn, int_mul_value); -static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_int_mul_fn(); }); -static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_int_mul_fn(); }); +MK_BUILTIN(Int_mul_fn, int_mul_value); +static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_Int_mul_fn(); }); +static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_Int_mul_fn(); }); constexpr char int_div_name[] = "div"; struct int_div_eval { @@ -105,9 +107,9 @@ struct int_div_eval { }; }; typedef int_bin_op int_div_value; -MK_BUILTIN(int_div_fn, int_div_value); -static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_int_div_fn(); }); -static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_int_div_fn(); }); +MK_BUILTIN(Int_div_fn, int_div_value); +static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_Int_div_fn(); }); +static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_Int_div_fn(); }); class int_le_value : public const_value { public: @@ -121,18 +123,9 @@ public: } virtual void write(serializer & s) const { s << "int_le"; } }; -MK_BUILTIN(int_le_fn, int_le_value); -static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_int_le_fn(); }); -static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_int_le_fn(); }); - -MK_CONSTANT(int_sub_fn, name({"Int", "sub"})); -MK_CONSTANT(int_neg_fn, name({"Int", "neg"})); -MK_CONSTANT(int_mod_fn, name({"Int", "mod"})); -MK_CONSTANT(int_divides_fn, name({"Int", "divides"})); -MK_CONSTANT(int_abs_fn, name({"Int", "abs"})); -MK_CONSTANT(int_ge_fn, name({"Int", "ge"})); -MK_CONSTANT(int_lt_fn, name({"Int", "lt"})); -MK_CONSTANT(int_gt_fn, name({"Int", "gt"})); +MK_BUILTIN(Int_le_fn, int_le_value); +static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_Int_le_fn(); }); +static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_Int_le_fn(); }); /** \brief Semantic attachment for the Nat to Int coercion. @@ -153,9 +146,6 @@ MK_BUILTIN(nat_to_int_fn, nat_to_int_value); static value::register_deserializer_fn nat_to_int_ds("nat_to_int", [](deserializer & ) { return mk_nat_to_int_fn(); }); static register_builtin_fn nat_to_int_blt("nat_to_int", []() { return mk_nat_to_int_fn(); }); -MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); -MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); - void import_int(environment const & env, io_state const & ios) { env->import("Int", ios); } diff --git a/src/library/arith/int.h b/src/library/arith/int.h index 39b8dd971..d06d87b13 100644 --- a/src/library/arith/int.h +++ b/src/library/arith/int.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/numerics/mpz.h" #include "kernel/expr.h" #include "kernel/builtin.h" +#include "library/arith/Int_decls.h" namespace lean { /** \brief Integer numbers type */ @@ -22,68 +23,16 @@ inline expr iVal(int v) { return mk_int_value(v); } bool is_int_value(expr const & e); mpz const & int_value_numeral(expr const & e); -/** \brief Addition, Int::add : Int -> Int -> Int */ -expr mk_int_add_fn(); -inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); } - -/** \brief Subtraction, Int::sub : Int -> Int -> Int */ -expr mk_int_sub_fn(); -inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); } - -/** \brief Unary minus, Int::neg : Int -> Int */ -expr mk_int_neg_fn(); -inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); } - -/** \brief Multiplication, Int::mul : Int -> Int -> Int */ -expr mk_int_mul_fn(); -inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); } - -/** \brief Integer division, Int::mul : Int -> Int -> Int */ -expr mk_int_div_fn(); -inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); } - -/** \brief Modulus, Int::mul : Int -> Int -> Int */ -expr mk_int_mod_fn(); -inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); } - -/** \brief Divides predicate, Int::mul : Int -> Int -> Bool */ -expr mk_int_divides_fn(); -inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_fn(), e1, e2); } - -/** \brief Absolute value function, Int::abs : Int -> Int */ -expr mk_int_abs_fn(); -inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); } - -/** \brief Less than or equal to, Int::le : Int -> Int -> Bool */ -expr mk_int_le_fn(); -inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); } - -/** \brief Greater than or equal to, Int::ge : Int -> Int -> Bool */ -expr mk_int_ge_fn(); -inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); } - -/** \brief Less than, Int::lt : Int -> Int -> Bool */ -expr mk_int_lt_fn(); -inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); } - -/** \brief Greater than, Int::gt : Int -> Int -> Bool */ -expr mk_int_gt_fn(); -inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); } - -/** \brief If-then-else for integers */ -inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); } - -/** \brief Coercion from natural to integer */ +expr mk_Int_add_fn(); +inline expr mk_Int_add(expr const & e1, expr const & e2) { return mk_app(mk_Int_add_fn(), e1, e2); } +expr mk_Int_mul_fn(); +inline expr mk_Int_mul(expr const & e1, expr const & e2) { return mk_app(mk_Int_mul_fn(), e1, e2); } +expr mk_Int_div_fn(); +inline expr mk_Int_div(expr const & e1, expr const & e2) { return mk_app(mk_Int_div_fn(), e1, e2); } +expr mk_Int_le_fn(); +inline expr mk_Int_le(expr const & e1, expr const & e2) { return mk_app(mk_Int_le_fn(), e1, e2); } expr mk_nat_to_int_fn(); -inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); } - -/** \brief Subtraction (for naturals), Nat::sub : Nat -> Nat -> Int */ -expr mk_nat_sub_fn(); -inline expr nSub(expr const & e1, expr const & e2) { return mk_app(mk_nat_sub_fn(), e1, e2); } - -/** \brief Unary minus (for naturals), Nat::neg : Nat -> Int */ -expr mk_nat_neg_fn(); -inline expr nNeg(expr const & e1, expr const & e2) { return mk_app(mk_nat_neg_fn(), e1, e2); } +inline expr mk_nat_to_int(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); } class environment; /** diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 52e70aefd..37f611e69 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -12,9 +12,9 @@ Author: Leonardo de Moura #include "kernel/decl_macros.h" #include "library/kernel_bindings.h" #include "library/arith/nat.h" +#include "library/arith/Nat_decls.cpp" namespace lean { -MK_CONSTANT(Nat, "Nat"); expr const Nat = mk_Nat(); expr mk_nat_type() { return mk_Nat(); } @@ -78,17 +78,17 @@ constexpr char nat_add_name[] = "add"; /** \brief Evaluator for + : Nat -> Nat -> Nat */ struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; }; typedef nat_bin_op nat_add_value; -MK_BUILTIN(nat_add_fn, nat_add_value); -static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_nat_add_fn(); }); -static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_nat_add_fn(); }); +MK_BUILTIN(Nat_add_fn, nat_add_value); +static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_Nat_add_fn(); }); +static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_Nat_add_fn(); }); constexpr char nat_mul_name[] = "mul"; /** \brief Evaluator for * : Nat -> Nat -> Nat */ struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; }; typedef nat_bin_op nat_mul_value; -MK_BUILTIN(nat_mul_fn, nat_mul_value); -static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_nat_mul_fn(); }); -static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_nat_mul_fn(); }); +MK_BUILTIN(Nat_mul_fn, nat_mul_value); +static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_Nat_mul_fn(); }); +static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_Nat_mul_fn(); }); /** \brief Semantic attachment for less than or equal to operator with type @@ -106,14 +106,9 @@ public: } virtual void write(serializer & s) const { s << "nat_le"; } }; -MK_BUILTIN(nat_le_fn, nat_le_value); -static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_nat_le_fn(); }); -static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_nat_le_fn(); }); - -MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"})); -MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"})); -MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"})); -MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); +MK_BUILTIN(Nat_le_fn, nat_le_value); +static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_Nat_le_fn(); }); +static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_Nat_le_fn(); }); void import_nat(environment const & env, io_state const & ios) { env->import("Nat", ios); diff --git a/src/library/arith/nat.h b/src/library/arith/nat.h index 04db17abe..9a6c519cf 100644 --- a/src/library/arith/nat.h +++ b/src/library/arith/nat.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/builtin.h" #include "util/numerics/mpz.h" +#include "library/arith/Nat_decls.h" namespace lean { /** \brief Natural numbers type */ @@ -22,36 +23,12 @@ inline expr nVal(unsigned v) { return mk_nat_value(v); } bool is_nat_value(expr const & e); mpz const & nat_value_numeral(expr const & e); -/** \brief Addition, Nat::add : Nat -> Nat -> Nat */ -expr mk_nat_add_fn(); -inline expr nAdd(expr const & e1, expr const & e2) { return mk_app(mk_nat_add_fn(), e1, e2); } - -/** \brief Multiplication, Nat::mul : Nat -> Nat -> Nat */ -expr mk_nat_mul_fn(); -inline expr nMul(expr const & e1, expr const & e2) { return mk_app(mk_nat_mul_fn(), e1, e2); } - -/** \brief Less than or equal to, Nat::le : Nat -> Nat -> Bool */ -expr mk_nat_le_fn(); -inline expr nLe(expr const & e1, expr const & e2) { return mk_app(mk_nat_le_fn(), e1, e2); } - -/** \brief Greater than or equal to, Nat::ge : Nat -> Nat -> Bool */ -expr mk_nat_ge_fn(); -inline expr nGe(expr const & e1, expr const & e2) { return mk_app(mk_nat_ge_fn(), e1, e2); } - -/** \brief Less than, Nat::lt : Nat -> Nat -> Bool */ -expr mk_nat_lt_fn(); -inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn(), e1, e2); } - -/** \brief Greater than, Nat::gt : Nat -> Nat -> Bool */ -expr mk_nat_gt_fn(); -inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); } - -/** \brief Identity function for natural numbers, Nat::id : Nat -> Nat */ -expr mk_nat_id_fn(); -inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); } - -/** \brief If-then-else for natural numbers */ -inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); } +expr mk_Nat_add_fn(); +inline expr mk_Nat_add(expr const & e1, expr const & e2) { return mk_app(mk_Nat_add_fn(), e1, e2); } +expr mk_Nat_mul_fn(); +inline expr mk_Nat_mul(expr const & e1, expr const & e2) { return mk_app(mk_Nat_mul_fn(), e1, e2); } +expr mk_Nat_le_fn(); +inline expr mk_Nat_le(expr const & e1, expr const & e2) { return mk_app(mk_Nat_le_fn(), e1, e2); } class environment; /** \brief Import Natural number library in the given environment (if it has not been imported already). */ diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index f02d18c5a..ed8a8a5fb 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -14,9 +14,9 @@ Author: Leonardo de Moura #include "library/arith/real.h" #include "library/arith/int.h" #include "library/arith/nat.h" +#include "library/arith/Real_decls.cpp" namespace lean { -MK_CONSTANT(Real, "Real"); expr const Real = mk_Real(); expr mk_real_type() { return mk_Real(); } @@ -85,18 +85,18 @@ constexpr char real_add_name[] = "add"; /** \brief Evaluator for + : Real -> Real -> Real */ struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; }; typedef real_bin_op real_add_value; -MK_BUILTIN(real_add_fn, real_add_value); -static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_real_add_fn(); }); -static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_real_add_fn(); }); +MK_BUILTIN(Real_add_fn, real_add_value); +static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_Real_add_fn(); }); +static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_Real_add_fn(); }); constexpr char real_mul_name[] = "mul"; /** \brief Evaluator for * : Real -> Real -> Real */ struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; }; typedef real_bin_op real_mul_value; -MK_BUILTIN(real_mul_fn, real_mul_value); -static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_real_mul_fn(); }); -static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_real_mul_fn(); }); +MK_BUILTIN(Real_mul_fn, real_mul_value); +static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_Real_mul_fn(); }); +static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_Real_mul_fn(); }); constexpr char real_div_name[] = "div"; /** \brief Evaluator for / : Real -> Real -> Real */ @@ -109,9 +109,9 @@ struct real_div_eval { }; }; typedef real_bin_op real_div_value; -MK_BUILTIN(real_div_fn, real_div_value); -static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_real_div_fn(); }); -static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_real_div_fn(); }); +MK_BUILTIN(Real_div_fn, real_div_value); +static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_Real_div_fn(); }); +static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_Real_div_fn(); }); /** \brief Semantic attachment for less than or equal to operator with type @@ -129,9 +129,9 @@ public: } virtual void write(serializer & s) const { s << "real_le"; } }; -MK_BUILTIN(real_le_fn, real_le_value); -static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_real_le_fn(); }); -static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_real_le_fn(); }); +MK_BUILTIN(Real_le_fn, real_le_value); +static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_Real_le_fn(); }); +static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_Real_le_fn(); }); class int_to_real_value : public const_value { public: @@ -149,14 +149,6 @@ MK_BUILTIN(int_to_real_fn, int_to_real_value); static value::register_deserializer_fn int_to_real_ds("int_to_real", [](deserializer & ) { return mk_int_to_real_fn(); }); static register_builtin_fn int_to_real_blt("int_to_real", []() { return mk_int_to_real_fn(); }); -MK_CONSTANT(real_sub_fn, name({"Real", "sub"})); -MK_CONSTANT(real_neg_fn, name({"Real", "neg"})); -MK_CONSTANT(real_abs_fn, name({"Real", "abs"})); -MK_CONSTANT(real_ge_fn, name({"Real", "ge"})); -MK_CONSTANT(real_lt_fn, name({"Real", "lt"})); -MK_CONSTANT(real_gt_fn, name({"Real", "gt"})); -MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); - void import_real(environment const & env, io_state const & ios) { env->import("Real", ios); } diff --git a/src/library/arith/real.h b/src/library/arith/real.h index 166c8eb0e..0deb3cae7 100644 --- a/src/library/arith/real.h +++ b/src/library/arith/real.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/numerics/mpq.h" #include "kernel/expr.h" #include "kernel/builtin.h" +#include "library/arith/Real_decls.h" namespace lean { /** \brief Real numbers type */ @@ -22,48 +23,14 @@ inline expr rVal(int v) { return mk_real_value(v); } bool is_real_value(expr const & e); mpq const & real_value_numeral(expr const & e); -/** \brief Addition, Real::add : Real -> Real -> Real */ -expr mk_real_add_fn(); -inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); } - -/** \brief Subtraction, Real::sub : Real -> Real -> Real */ -expr mk_real_sub_fn(); -inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); } - -/** \brief Unary minus, Real::neg : Real -> Real */ -expr mk_real_neg_fn(); -inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); } - -/** \brief Multiplication, Real::mul : Real -> Real -> Real */ -expr mk_real_mul_fn(); -inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); } - -/** \brief Division, Real::mul : Real -> Real -> Real */ -expr mk_real_div_fn(); -inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); } - -/** \brief Absolute value function, Real::abs : Real -> Real */ -expr mk_real_abs_fn(); -inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); } - -/** \brief Less than or equal to, Real::le : Real -> Real -> Bool */ -expr mk_real_le_fn(); -inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); } - -/** \brief Greater than or equal to, Real::ge : Real -> Real -> Bool */ -expr mk_real_ge_fn(); -inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); } - -/** \brief Less than, Real::lt : Real -> Real -> Bool */ -expr mk_real_lt_fn(); -inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); } - -/** \brief Greater than, Real::gt : Real -> Real -> Bool */ -expr mk_real_gt_fn(); -inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); } - -/** \brief If-then-else for reals */ -inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); } +expr mk_Real_add_fn(); +inline expr mk_Real_add(expr const & e1, expr const & e2) { return mk_app(mk_Real_add_fn(), e1, e2); } +expr mk_Real_mul_fn(); +inline expr mk_Real_mul(expr const & e1, expr const & e2) { return mk_app(mk_Real_mul_fn(), e1, e2); } +expr mk_Real_div_fn(); +inline expr mk_Real_div(expr const & e1, expr const & e2) { return mk_app(mk_Real_div_fn(), e1, e2); } +expr mk_Real_le_fn(); +inline expr mk_Real_le(expr const & e1, expr const & e2) { return mk_app(mk_Real_le_fn(), e1, e2); } class environment; /** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */ @@ -71,10 +38,7 @@ void import_real(environment const & env, io_state const & ios); /** \brief Coercion from int to real */ expr mk_int_to_real_fn(); -inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); } -/** \brief Coercion from nat to real */ -expr mk_nat_to_real_fn(); -inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); } +inline expr mk_int_to_real(expr const & e) { return mk_app(mk_int_to_real_fn(), e); } /** \brief Import the coercions \c i2r and \c n2r. The Integer and (basic) Real libraries are also imported. */ void import_int_to_real_coercions(environment const & env); diff --git a/src/library/bin_op.h b/src/library/bin_op.h index b7ac18462..89ebabaf7 100644 --- a/src/library/bin_op.h +++ b/src/library/bin_op.h @@ -30,7 +30,4 @@ inline expr And(std::initializer_list const & l) { return mk_and(l.size(), inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); } inline expr Or(std::initializer_list const & l) { return mk_or(l.size(), l.begin()); } - -inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); } -inline expr Iff(std::initializer_list const & l) { return mk_iff(l.size(), l.begin()); } } diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 3b8d180b6..a8921fe6b 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -43,7 +43,7 @@ class deep_copy_fn { new_args.push_back(apply(old_arg)); return save_result(a, mk_app(new_args), sh); } - case expr_kind::Eq: return save_result(a, mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))), sh); + case expr_kind::HEq: return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh); case expr_kind::Lambda: return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh); case expr_kind::Pi: return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh); case expr_kind::Let: return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 4d414cc80..43f157a75 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -621,7 +621,7 @@ class elaborator::imp { } void process_eq(context const & ctx, expr & a) { - if (is_eq(a) && m_use_normalizer) { + if (is_heq(a) && m_use_normalizer) { a = normalize(ctx, a); } } @@ -840,16 +840,17 @@ class elaborator::imp { push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption); } imitation = mk_lambda(arg_types, mk_app(imitation_args)); - } else if (is_eq(b)) { + } else if (is_heq(b)) { // Imitation for equality // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), (h_1 x_1 ... x_{num_a}) = (h_2 x_1 ... x_{num_a}) // New constraints (h_1 a_1 ... a_{num_a}) == eq_lhs(b) // (h_2 a_1 ... a_{num_a}) == eq_rhs(b) expr h_1 = new_state.m_menv->mk_metavar(ctx); expr h_2 = new_state.m_menv->mk_metavar(ctx); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption); - imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), mk_app_vars(add_lift(h_2, 0, num_a - 1), num_a - 1))); + push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption); + push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption); + imitation = mk_lambda(arg_types, mk_heq(mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), + mk_app_vars(add_lift(h_2, 0, num_a - 1), num_a - 1))); } else if (is_abstraction(b)) { // Imitation for lambdas and Pis // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), @@ -1063,7 +1064,7 @@ class elaborator::imp { void imitate_equality(expr const & a, expr const & b, unification_constraint const & c) { lean_assert(is_metavar(a)); static_cast(b); // this line is just to avoid a warning, b is only used in an assertion - lean_assert(is_eq(b)); + lean_assert(is_heq(b)); lean_assert(!is_assigned(a)); lean_assert(has_local_context(a)); // imitate @@ -1074,7 +1075,7 @@ class elaborator::imp { context ctx_m = m_state.m_menv->get_context(m); expr h1 = m_state.m_menv->mk_metavar(ctx_m); expr h2 = m_state.m_menv->mk_metavar(ctx_m); - expr imitation = mk_eq(h1, h2); + expr imitation = mk_heq(h1, h2); justification new_jst(new imitation_justification(c)); push_new_constraint(true, ctx_m, m, imitation, new_jst); } @@ -1137,7 +1138,7 @@ class elaborator::imp { } else if (is_app(b) && !has_metavar(arg(b, 0))) { imitate_application(a, b, c); return true; - } else if (is_eq(b)) { + } else if (is_heq(b)) { imitate_equality(a, b, c); return true; } diff --git a/src/library/eq_heq.cpp b/src/library/eq_heq.cpp index fb0098610..19b6d6dfe 100644 --- a/src/library/eq_heq.cpp +++ b/src/library/eq_heq.cpp @@ -9,13 +9,13 @@ Author: Leonardo de Moura namespace lean { bool is_eq_heq(expr const & e) { - return is_eq(e) || is_homo_eq(e); + return is_heq(e) || is_eq(e); } expr_pair eq_heq_args(expr const & e) { - lean_assert(is_eq(e) || is_homo_eq(e)); - if (is_eq(e)) - return expr_pair(eq_lhs(e), eq_rhs(e)); + lean_assert(is_heq(e) || is_eq(e)); + if (is_heq(e)) + return expr_pair(heq_lhs(e), heq_rhs(e)); else return expr_pair(arg(e, 2), arg(e, 3)); } diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index 8da4cd39a..e355cb0ff 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -37,11 +37,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(arg(a, i), arg(b, i), use_hash); } lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Eq: - if (eq_lhs(a) != eq_lhs(b)) - return is_lt(eq_lhs(a), eq_lhs(b), use_hash); + case expr_kind::HEq: + if (heq_lhs(a) != heq_lhs(b)) + return is_lt(heq_lhs(a), heq_lhs(b), use_hash); else - return is_lt(eq_rhs(a), eq_rhs(b), use_hash); + return is_lt(heq_rhs(a), heq_rhs(b), use_hash); case expr_kind::Lambda: // Remark: we ignore get_abs_name because we want alpha-equivalence case expr_kind::Pi: if (abst_domain(a) != abst_domain(b)) diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index 3e29fb3d5..0ad2e2d65 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -62,7 +62,7 @@ optional fo_unify(expr e1, expr e2) { } } break; - case expr_kind::Eq: + case expr_kind::HEq: lean_unreachable(); break; // LCOV_EXCL_LINE case expr_kind::Lambda: case expr_kind::Pi: todo.emplace_back(abst_body(e1), abst_body(e2)); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 9a2054387..96440e7fc 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -322,8 +322,8 @@ static int expr_mk_app(lua_State * L) { return push_expr(L, mk_app(args)); } -static int expr_mk_eq(lua_State * L) { - return push_expr(L, mk_eq(to_expr(L, 1), to_expr(L, 2))); +static int expr_mk_heq(lua_State * L) { + return push_expr(L, mk_heq(to_expr(L, 1), to_expr(L, 2))); } static int expr_mk_lambda(lua_State * L) { @@ -437,7 +437,7 @@ static int expr_ ## P(lua_State * L) { \ EXPR_PRED(is_constant) EXPR_PRED(is_var) EXPR_PRED(is_app) -EXPR_PRED(is_eq) +EXPR_PRED(is_heq) EXPR_PRED(is_lambda) EXPR_PRED(is_pi) EXPR_PRED(is_abstraction) @@ -450,12 +450,8 @@ EXPR_PRED(has_metavar) EXPR_PRED(is_not) EXPR_PRED(is_and) EXPR_PRED(is_or) -EXPR_PRED(is_if) -EXPR_PRED(is_iff) EXPR_PRED(is_implies) -EXPR_PRED(is_forall) EXPR_PRED(is_exists) -EXPR_PRED(is_homo_eq) /** \brief Iterator (closure base function) for application args. See \c expr_args @@ -502,7 +498,7 @@ static int expr_fields(lua_State * L) { case expr_kind::Type: return push_level(L, ty_level(e)); case expr_kind::Value: return to_value(e).push_lua(L); case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2; - case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2; + case expr_kind::HEq: push_expr(L, heq_lhs(e)); push_expr(L, heq_rhs(e)); return 2; case expr_kind::Lambda: case expr_kind::Pi: push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3; @@ -617,7 +613,7 @@ static const struct luaL_Reg expr_m[] = { {"is_var", safe_function}, {"is_constant", safe_function}, {"is_app", safe_function}, - {"is_eq", safe_function}, + {"is_heq", safe_function}, {"is_lambda", safe_function}, {"is_pi", safe_function}, {"is_abstraction", safe_function}, @@ -644,12 +640,8 @@ static const struct luaL_Reg expr_m[] = { {"is_not", safe_function}, {"is_and", safe_function}, {"is_or", safe_function}, - {"is_if", safe_function}, - {"is_iff", safe_function}, {"is_implies", safe_function}, - {"is_forall", safe_function}, {"is_exists", safe_function}, - {"is_home_eq", safe_function}, {0, 0} }; @@ -669,8 +661,8 @@ static void open_expr(lua_State * L) { SET_GLOBAL_FUN(expr_mk_var, "mk_var"); SET_GLOBAL_FUN(expr_mk_var, "Var"); SET_GLOBAL_FUN(expr_mk_app, "mk_app"); - SET_GLOBAL_FUN(expr_mk_eq, "mk_eq"); - SET_GLOBAL_FUN(expr_mk_eq, "Eq"); + SET_GLOBAL_FUN(expr_mk_heq, "mk_heq"); + SET_GLOBAL_FUN(expr_mk_heq, "HEq"); SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda"); SET_GLOBAL_FUN(expr_mk_pi, "mk_pi"); SET_GLOBAL_FUN(expr_mk_arrow, "mk_arrow"); @@ -690,7 +682,7 @@ static void open_expr(lua_State * L) { SET_ENUM("Type", expr_kind::Type); SET_ENUM("Value", expr_kind::Value); SET_ENUM("App", expr_kind::App); - SET_ENUM("Eq", expr_kind::Eq); + SET_ENUM("HEq", expr_kind::HEq); SET_ENUM("Lambda", expr_kind::Lambda); SET_ENUM("Pi", expr_kind::Pi); SET_ENUM("Let", expr_kind::Let); diff --git a/src/library/printer.cpp b/src/library/printer.cpp index 4383f3167..d4c1e1e7a 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -18,7 +18,7 @@ bool is_atomic(expr const & e) { case expr_kind::Type: case expr_kind::MetaVar: return true; case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: - case expr_kind::Eq: case expr_kind::Let: + case expr_kind::HEq: case expr_kind::Let: return false; } return false; @@ -55,10 +55,10 @@ struct print_expr_fn { } } - void print_eq(expr const & a, context const & c) { - print_child(eq_lhs(a), c); + void print_heq(expr const & a, context const & c) { + print_child(heq_lhs(a), c); out() << " == "; - print_child(eq_rhs(a), c); + print_child(heq_rhs(a), c); } void print_app(expr const & e, context const & c) { @@ -114,8 +114,8 @@ struct print_expr_fn { case expr_kind::App: print_app(a, c); break; - case expr_kind::Eq: - print_eq(a, c); + case expr_kind::HEq: + print_heq(a, c); break; case expr_kind::Lambda: out() << "fun " << abst_name(a) << " : "; diff --git a/src/library/rewriter/fo_match.cpp b/src/library/rewriter/fo_match.cpp index 54b05c050..21c99587b 100644 --- a/src/library/rewriter/fo_match.cpp +++ b/src/library/rewriter/fo_match.cpp @@ -117,11 +117,11 @@ bool fo_match::match_type(expr const & p, expr const & t, unsigned, subst_map &) return p == t; } -bool fo_match::match_eq(expr const & p, expr const & t, unsigned o, subst_map & s) { +bool fo_match::match_heq(expr const & p, expr const & t, unsigned o, subst_map & s) { lean_trace("fo_match", tout << "match_eq : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE - if (!is_eq(t)) + if (!is_heq(t)) return false; - return match_main(eq_lhs(p), eq_lhs(t), o, s) && match_main(eq_rhs(p), eq_rhs(t), o, s); + return match_main(heq_lhs(p), heq_lhs(t), o, s) && match_main(heq_rhs(p), heq_rhs(t), o, s); } bool fo_match::match_let(expr const & p, expr const & t, unsigned o, subst_map & s) { @@ -176,8 +176,8 @@ bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map return match_pi(p, t, o, s); case expr_kind::Type: return match_type(p, t, o, s); - case expr_kind::Eq: - return match_eq(p, t, o, s); + case expr_kind::HEq: + return match_heq(p, t, o, s); case expr_kind::Let: return match_let(p, t, o, s); case expr_kind::MetaVar: diff --git a/src/library/rewriter/fo_match.h b/src/library/rewriter/fo_match.h index e65b456ce..edf2e5ecf 100644 --- a/src/library/rewriter/fo_match.h +++ b/src/library/rewriter/fo_match.h @@ -22,7 +22,7 @@ private: bool match_lambda(expr const & p, expr const & t, unsigned o, subst_map & s); bool match_pi(expr const & p, expr const & t, unsigned o, subst_map & s); bool match_type(expr const & p, expr const & t, unsigned o, subst_map & s); - bool match_eq(expr const & p, expr const & t, unsigned o, subst_map & s); + bool match_heq(expr const & p, expr const & t, unsigned o, subst_map & s); bool match_let(expr const & p, expr const & t, unsigned o, subst_map & s); bool match_metavar(expr const & p, expr const & t, unsigned o, subst_map & s); bool match_main(expr const & p, expr const & t, unsigned o, subst_map & s); diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 05db681c1..a8cb14fdb 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -47,7 +47,7 @@ pair rewrite_lambda_type(environment const & env, context & ctx, exp expr const & new_ty = result_ty.first; expr const & ty_v = ti(v, ctx); if (ty == new_ty) { - return make_pair(v, Refl(ty_v, v)); + return make_pair(v, mk_refl_th(ty_v, v)); } else { name const & n = abst_name(v); expr const & body = abst_body(v); @@ -55,10 +55,10 @@ pair rewrite_lambda_type(environment const & env, context & ctx, exp expr const & new_v = mk_lambda(n, new_ty, body); expr const & ty_ty = ti(ty, ctx); lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types - expr const & proof = Subst(ty_ty, ty, new_ty, + expr const & proof = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("T"), ty_ty}, - mk_eq(v, mk_lambda(n, Const("T"), body))), - Refl(ty_v, v), pf_ty); + mk_heq(v, mk_lambda(n, Const("T"), body))), + mk_refl_th(ty_v, v), pf_ty); return make_pair(new_v, proof); } } @@ -83,7 +83,7 @@ pair rewrite_lambda_body(environment const & env, context & ctx, exp expr const & new_body = result_body.first; expr const & ty_v = ti(v, ctx); if (body == new_body) { - return make_pair(v, Refl(ty_v, v)); + return make_pair(v, mk_refl_th(ty_v, v)); } else { name const & n = abst_name(v); expr const & ty = abst_domain(v); @@ -91,7 +91,7 @@ pair rewrite_lambda_body(environment const & env, context & ctx, exp expr const & new_v = mk_lambda(n, ty, new_body); expr const & ty_body = ti(body, extend(ctx, n, ty)); lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types - expr const & proof = Abst(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body)); + expr const & proof = mk_funext_th(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body)); return make_pair(new_v, proof); } } @@ -128,18 +128,18 @@ pair rewrite_lambda(environment const & env, context & ctx, expr con expr const & ty_new_v1 = ti(v, ctx); expr const & new_v2 = mk_lambda(n, new_ty, new_body); // proof1 : v = new_v1 - expr const & proof1 = Subst(ty_ty, ty, new_ty, - Fun({Const("T"), ty_ty}, - mk_eq(v, mk_lambda(n, Const("T"), body))), - Refl(ty_v, v), - pf_ty); + expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty, + Fun({Const("T"), ty_ty}, + mk_heq(v, mk_lambda(n, Const("T"), body))), + mk_refl_th(ty_v, v), + pf_ty); // proof2 : new_v1 = new_v2 - expr const & proof2 = Subst(ty_body, body, new_body, - Fun({Const("e"), ty_body}, - mk_eq(new_v1, mk_lambda(n, new_ty, Const("e")))), - Refl(ty_new_v1, new_v1), - pf_body); - expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2); + expr const & proof2 = mk_subst_th(ty_body, body, new_body, + Fun({Const("e"), ty_body}, + mk_heq(new_v1, mk_lambda(n, new_ty, Const("e")))), + mk_refl_th(ty_new_v1, new_v1), + pf_body); + expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); return make_pair(new_v2, proof); } @@ -166,11 +166,11 @@ pair rewrite_pi_type(environment const & env, context & ctx, expr co expr const & new_v = mk_pi(n, new_ty, body); expr const & ty_ty = ti(ty, ctx); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_ty, ty, new_ty, - Fun({Const("T"), ty_ty}, - mk_eq(v, mk_pi(n, Const("T"), body))), - Refl(ty_v, v), - pf); + expr const & proof = mk_subst_th(ty_ty, ty, new_ty, + Fun({Const("T"), ty_ty}, + mk_heq(v, mk_pi(n, Const("T"), body))), + mk_refl_th(ty_v, v), + pf); return make_pair(new_v, proof); } @@ -198,10 +198,10 @@ pair rewrite_pi_body(environment const & env, context & ctx, expr co expr const & new_v = mk_pi(n, ty, new_body); expr const & ty_body = ti(body, extend(ctx, n, ty)); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_body, body, new_body, + expr const & proof = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, - mk_eq(v, mk_pi(n, ty, Const("e")))), - Refl(ty_v, v), + mk_heq(v, mk_pi(n, ty, Const("e")))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } @@ -237,17 +237,17 @@ pair rewrite_pi(environment const & env, context & ctx, expr const & expr const & new_v1 = mk_pi(n, new_ty, body); expr const & ty_new_v1 = ti(v, ctx); expr const & new_v2 = mk_pi(n, new_ty, new_body); - expr const & proof1 = Subst(ty_ty, ty, new_ty, + expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("T"), ty_ty}, - mk_eq(v, mk_pi(n, Const("T"), body))), - Refl(ty_v, v), + mk_heq(v, mk_pi(n, Const("T"), body))), + mk_refl_th(ty_v, v), pf_ty); - expr const & proof2 = Subst(ty_body, body, new_body, + expr const & proof2 = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, - mk_eq(new_v1, mk_pi(n, new_ty, Const("e")))), - Refl(ty_new_v1, new_v1), + mk_heq(new_v1, mk_pi(n, new_ty, Const("e")))), + mk_refl_th(ty_new_v1, new_v1), pf_body); - expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2); + expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); return make_pair(new_v2, proof); } @@ -264,19 +264,19 @@ pair rewrite_pi(environment const & env, context & ctx, expr const & \return pair of v' = (lhs' = rhs), and proof of v = v' */ pair rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, pair const & result_lhs) { - lean_assert(is_eq(v)); + lean_assert(is_heq(v)); type_inferer ti(env); - expr const & lhs = eq_lhs(v); - expr const & rhs = eq_rhs(v); + expr const & lhs = heq_lhs(v); + expr const & rhs = heq_rhs(v); expr const & new_lhs = result_lhs.first; expr const & pf = result_lhs.second; - expr const & new_v = mk_eq(new_lhs, rhs); + expr const & new_v = mk_heq(new_lhs, rhs); expr const & ty_lhs = ti(lhs, ctx); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_lhs, lhs, new_lhs, + expr const & proof = mk_subst_th(ty_lhs, lhs, new_lhs, Fun({Const("x"), ty_lhs}, - mk_eq(v, mk_eq(Const("x"), rhs))), - Refl(ty_v, v), + mk_heq(v, mk_heq(Const("x"), rhs))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } @@ -294,19 +294,19 @@ pair rewrite_eq_lhs(environment const & env, context & ctx, expr con \return pair of v' = (lhs = rhs'), and proof of v = v' */ pair rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, pair const & result_rhs) { - lean_assert(is_eq(v)); + lean_assert(is_heq(v)); type_inferer ti(env); - expr const & lhs = eq_lhs(v); - expr const & rhs = eq_rhs(v); + expr const & lhs = heq_lhs(v); + expr const & rhs = heq_rhs(v); expr const & new_rhs = result_rhs.first; expr const & pf = result_rhs.second; - expr const & new_v = mk_eq(rhs, new_rhs); + expr const & new_v = mk_heq(rhs, new_rhs); expr const & ty_rhs = ti(rhs, ctx); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_rhs, rhs, new_rhs, + expr const & proof = mk_subst_th(ty_rhs, rhs, new_rhs, Fun({Const("x"), ty_rhs}, - mk_eq(v, mk_eq(lhs, Const("x")))), - Refl(ty_v, v), + mk_heq(v, mk_heq(lhs, Const("x")))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } @@ -326,31 +326,31 @@ pair rewrite_eq_rhs(environment const & env, context & ctx, expr con \return pair of v' = (lhs' = rhs'), and proof of v = v' */ pair rewrite_eq(environment const & env, context & ctx, expr const & v, pair const & result_lhs, pair const & result_rhs) { - lean_assert(is_eq(v)); + lean_assert(is_heq(v)); type_inferer ti(env); - expr const & lhs = eq_lhs(v); - expr const & rhs = eq_rhs(v); + expr const & lhs = heq_lhs(v); + expr const & rhs = heq_rhs(v); expr const & new_lhs = result_lhs.first; expr const & pf_lhs = result_lhs.second; expr const & new_rhs = result_rhs.first; expr const & pf_rhs = result_rhs.second; - expr const & new_v1 = mk_eq(new_lhs, rhs); - expr const & new_v2 = mk_eq(new_lhs, new_rhs); + expr const & new_v1 = mk_heq(new_lhs, rhs); + expr const & new_v2 = mk_heq(new_lhs, new_rhs); expr const & ty_lhs = ti(lhs, ctx); expr const & ty_rhs = ti(rhs, ctx); expr const & ty_v = ti(v, ctx); expr const & ty_new_v1 = ti(new_v1, ctx); - expr const & proof1 = Subst(ty_lhs, lhs, new_lhs, + expr const & proof1 = mk_subst_th(ty_lhs, lhs, new_lhs, Fun({Const("x"), ty_lhs}, - mk_eq(v, mk_eq(Const("x"), rhs))), - Refl(ty_v, v), + mk_heq(v, mk_heq(Const("x"), rhs))), + mk_refl_th(ty_v, v), pf_lhs); - expr const & proof2 = Subst(ty_rhs, rhs, new_rhs, + expr const & proof2 = mk_subst_th(ty_rhs, rhs, new_rhs, Fun({Const("x"), ty_rhs}, - mk_eq(v, mk_eq(lhs, Const("x")))), - Refl(ty_new_v1, new_v1), + mk_heq(v, mk_heq(lhs, Const("x")))), + mk_refl_th(ty_new_v1, new_v1), pf_rhs); - expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2); + expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); return make_pair(new_v2, proof); } @@ -379,10 +379,10 @@ pair rewrite_let_type(environment const & env, context & ctx, expr c expr const & new_v = mk_let(n, new_ty, val, body); expr const & ty_ty = ti(ty, ctx); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_ty, ty, new_ty, + expr const & proof = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("x"), ty_ty}, - mk_eq(v, mk_let(n, Const("x"), val, body))), - Refl(ty_v, v), + mk_heq(v, mk_let(n, Const("x"), val, body))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } else { @@ -414,10 +414,10 @@ pair rewrite_let_value(environment const & env, context & ctx, expr expr const & new_v = mk_let(n, ty, new_val, body); expr const & ty_val = ti(val, ctx); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_val, val, new_val, + expr const & proof = mk_subst_th(ty_val, val, new_val, Fun({Const("x"), ty_val}, - mk_eq(v, mk_let(n, ty, Const("x"), body))), - Refl(ty_v, v), + mk_heq(v, mk_let(n, ty, Const("x"), body))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } @@ -447,10 +447,10 @@ pair rewrite_let_body(environment const & env, context & ctx, expr c expr const & new_v = mk_let(n, ty, val, new_body); expr const & ty_body = ti(body, extend(ctx, n, ty, body)); expr const & ty_v = ti(v, ctx); - expr const & proof = Subst(ty_body, body, new_body, + expr const & proof = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, - mk_eq(v, mk_let(n, ty, val, Const("e")))), - Refl(ty_v, v), + mk_heq(v, mk_let(n, ty, val, Const("e")))), + mk_refl_th(ty_v, v), pf); return make_pair(new_v, proof); } @@ -483,22 +483,22 @@ pair rewrite_app(environment const & env, context & ctx, expr const bool f_changed = f != new_f; if (f_changed) { if (arg(v, i) != results[i].first) { - // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi + // congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi // (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f // a = g b - pf = Congr(f_ty_domain, f_ty_body, f, new_f, e_i, new_e_i, pf, pf_e_i); + pf = mk_congr_th(f_ty_domain, f_ty_body, f, new_f, e_i, new_e_i, pf, pf_e_i); } else { - // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi + // congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi // (x : A) B x) (a : A) (H : f = g), f a = g a - pf = Congr1(f_ty_domain, f_ty_body, f, new_f, e_i, pf); + pf = mk_congr1_th(f_ty_domain, f_ty_body, f, new_f, e_i, pf); } } else { if (arg(v, i) != results[i].first) { - // Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b - pf = Congr2(f_ty_domain, f_ty_body, e_i, new_e_i, f, pf_e_i); + // congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b + pf = mk_congr2_th(f_ty_domain, f_ty_body, e_i, new_e_i, f, pf_e_i); } else { - // Refl - pf = Refl(ti(f(e_i), ctx), f(e_i)); + // refl + pf = mk_refl_th(ti(f(e_i), ctx), f(e_i)); } } f = f (e_i); @@ -527,12 +527,12 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod m_pattern = abst_body(m_pattern); m_num_args++; } - if (!is_eq(m_pattern)) { + if (!is_heq(m_pattern)) { lean_trace("rewriter", tout << "Theorem " << m_type << " is not in the form of " << "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;); } - m_rhs = eq_rhs(m_pattern); - m_pattern = eq_lhs(m_pattern); + m_rhs = heq_rhs(m_pattern); + m_pattern = heq_lhs(m_pattern); lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;); } @@ -631,7 +631,7 @@ pair then_rewriter_cell::operator()(environment const & env, context expr const & ty = type_inferer(env)(v, ctx); if (v != new_result.first) { result = make_pair(new_result.first, - Trans(ty, v, result.first, new_result.first, result.second, new_result.second)); + mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second)); } } return result; @@ -661,7 +661,7 @@ pair try_rewriter_cell::operator()(environment const & env, context } // If the execution reaches here, it means every rewriter failed. expr const & t = type_inferer(env)(v, ctx); - return make_pair(v, Refl(t, v)); + return make_pair(v, mk_refl_th(t, v)); } ostream & try_rewriter_cell::display(ostream & out) const { out << "Try_RW({"; @@ -705,7 +705,7 @@ pair lambda_type_rewriter_cell::operator()(environment const & env, return rewrite_lambda_type(env, ctx, v, result_ty); } else { // nothing changed - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & lambda_type_rewriter_cell::display(ostream & out) const { @@ -733,7 +733,7 @@ pair lambda_body_rewriter_cell::operator()(environment const & env, } else { // nothing changed type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & lambda_body_rewriter_cell::display(ostream & out) const { @@ -774,7 +774,7 @@ pair pi_type_rewriter_cell::operator()(environment const & env, cont } else { // nothing changed type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & pi_type_rewriter_cell::display(ostream & out) const { @@ -802,7 +802,7 @@ pair pi_body_rewriter_cell::operator()(environment const & env, cont } else { // nothing changed type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & pi_body_rewriter_cell::display(ostream & out) const { @@ -842,7 +842,7 @@ pair let_type_rewriter_cell::operator()(environment const & env, con return rewrite_let_type(env, ctx, v, result_ty); } else { type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & let_type_rewriter_cell::display(ostream & out) const { @@ -865,7 +865,7 @@ pair let_value_rewriter_cell::operator()(environment const & env, co return rewrite_let_value(env, ctx, v, result_val); } else { type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & let_value_rewriter_cell::display(ostream & out) const { @@ -890,7 +890,7 @@ pair let_body_rewriter_cell::operator()(environment const & env, con return rewrite_let_body(env, ctx, v, result_body); } else { type_inferer ti(env); - return make_pair(v, Refl(ti(v, ctx), v)); + return make_pair(v, mk_refl_th(ti(v, ctx), v)); } } ostream & let_body_rewriter_cell::display(ostream & out) const { @@ -931,7 +931,7 @@ success_rewriter_cell::success_rewriter_cell():rewriter_cell(rewriter_kind::Succ success_rewriter_cell::~success_rewriter_cell() { } pair success_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { expr const & t = type_inferer(env)(v, ctx); - return make_pair(v, Refl(t, v)); + return make_pair(v, mk_refl_th(t, v)); } ostream & success_rewriter_cell::display(ostream & out) const { out << "Success_RW()"; @@ -951,7 +951,7 @@ pair repeat_rewriter_cell::operator()(environment const & env, conte break; expr const & ty = ti(v, ctx); result = make_pair(new_result.first, - Trans(ty, v, result.first, new_result.first, result.second, new_result.second)); + mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second)); } } catch (rewriter_exception &) { return result; diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index f945763ce..320732bae 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -382,14 +382,14 @@ class apply_rewriter_fn { result = rewrite_app(env, ctx, v, results); std::pair tmp = m_rw(env, ctx, result.first); if (result.first != tmp.first) { - tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second); + tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); result = tmp; } } break; - case expr_kind::Eq: { - expr const & lhs = eq_lhs(v); - expr const & rhs = eq_rhs(v); + case expr_kind::HEq: { + expr const & lhs = heq_lhs(v); + expr const & rhs = heq_rhs(v); std::pair result_lhs = apply(env, ctx, lhs); std::pair result_rhs = apply(env, ctx, rhs); expr const & new_lhs = result_lhs.first; @@ -408,12 +408,12 @@ class apply_rewriter_fn { result = rewrite_eq_rhs(env, ctx, v, result_rhs); } else { // nothing changed - result = std::make_pair(v, Refl(ti(v, ctx), v)); + result = std::make_pair(v, mk_refl_th(ti(v, ctx), v)); } } std::pair tmp = m_rw(env, ctx, result.first); if (result.first != tmp.first) { - tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second); + tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); result = tmp; } } @@ -439,12 +439,12 @@ class apply_rewriter_fn { result = rewrite_lambda_body(env, ctx, v, result_body); } else { // nothing changed - result = std::make_pair(v, Refl(ti(v, ctx), v)); + result = std::make_pair(v, mk_refl_th(ti(v, ctx), v)); } } std::pair tmp = m_rw(env, ctx, result.first); if (result.first != tmp.first) { - tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second); + tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); result = tmp; } } @@ -471,12 +471,12 @@ class apply_rewriter_fn { result = rewrite_pi_body(env, ctx, v, result_body); } else { // nothing changed - result = std::make_pair(v, Refl(ti(v, ctx), v)); + result = std::make_pair(v, mk_refl_th(ti(v, ctx), v)); } } std::pair tmp = m_rw(env, ctx, result.first); if (result.first != tmp.first) { - tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second); + tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); result = tmp; } } @@ -489,7 +489,7 @@ class apply_rewriter_fn { expr new_v = v; expr ty_v = ti(v, ctx); - expr pf = Refl(ty_v, v); + expr pf = mk_refl_th(ty_v, v); bool changed = false; if (ty) { @@ -507,7 +507,7 @@ class apply_rewriter_fn { if (val != result_val.first) { result = rewrite_let_value(env, ctx, new_v, result_val); if (changed) { - pf = Trans(ty_v, v, new_v, result.first, pf, result.second); + pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second); } else { pf = result.second; } @@ -520,7 +520,7 @@ class apply_rewriter_fn { if (body != result_body.first) { result = rewrite_let_body(env, ctx, new_v, result_body); if (changed) { - pf = Trans(ty_v, v, new_v, result.first, pf, result.second); + pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second); } else { pf = result.second; } @@ -531,7 +531,7 @@ class apply_rewriter_fn { std::pair tmp = m_rw(env, ctx, result.first); if (result.first != tmp.first) { - tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second); + tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); result = tmp; } } diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp index 077f1ae1d..c1c3c7b31 100644 --- a/src/library/tactic/boolean_tactics.cpp +++ b/src/library/tactic/boolean_tactics.cpp @@ -44,7 +44,7 @@ tactic conj_tactic(bool all) { for (auto nc : proof_info) { name const & n = nc.first; expr const & c = nc.second; - new_m.insert(n, Conj(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2)))); + new_m.insert(n, mk_and_intro_th(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2)))); new_m.erase(name(n, 1)); new_m.erase(name(n, 2)); } @@ -104,9 +104,9 @@ tactic conj_hyp_tactic(bool all) { expr const & H_1 = mk_constant(name(H_name, 1)); expr const & H_2 = mk_constant(name(H_name, 2)); if (occurs(H_1, pr)) - pr = Let_simp(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); + pr = Let_simp(H_1, mk_and_eliml_th(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); if (occurs(H_2, pr)) - pr = Let_simp(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); + pr = Let_simp(H_2, mk_and_elimr_th(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); } new_m.insert(goal_name, pr); } @@ -161,7 +161,7 @@ optional disj_hyp_tactic_core(name const & goal_name, name const & expr pr2 = find(m, name(goal_name, 2)); pr1 = Fun(hyp_name, arg(Href, 1), pr1); pr2 = Fun(hyp_name, arg(Href, 2), pr2); - new_m.insert(goal_name, DisjCases(arg(Href, 1), arg(Href, 2), conclusion, mk_constant(hyp_name), pr1, pr2)); + new_m.insert(goal_name, mk_or_elim_th(arg(Href, 1), arg(Href, 2), conclusion, mk_constant(hyp_name), pr1, pr2)); new_m.erase(name(goal_name, 1)); new_m.erase(name(goal_name, 2)); return pb(new_m, a); @@ -241,12 +241,12 @@ optional disj_tactic(proof_state const & s, name gname) { proof_builder pb = s.get_proof_builder(); proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); - new_m.insert(gname, Disj1(arg(*conclusion, 1), find(m, gname), arg(*conclusion, 2))); + new_m.insert(gname, mk_or_introl_th(arg(*conclusion, 1), find(m, gname), arg(*conclusion, 2))); return pb(new_m, a); }); proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { proof_map new_m(m); - new_m.insert(gname, Disj2(arg(*conclusion, 2), arg(*conclusion, 1), find(m, gname))); + new_m.insert(gname, mk_or_intror_th(arg(*conclusion, 2), arg(*conclusion, 1), find(m, gname))); return pb(new_m, a); }); proof_state s1(precision::Over, new_gs1, s.get_menv(), new_pb1, s.get_cex_builder()); @@ -296,7 +296,7 @@ tactic absurd_tactic() { expr a = arg(p1.second, 1); for (auto const & p2 : g.get_hypotheses()) { if (p2.second == a) { - expr pr = AbsurdElim(a, c, mk_constant(p2.first), mk_constant(p1.first)); + expr pr = mk_absurd_elim_th(a, c, mk_constant(p2.first), mk_constant(p1.first)); proofs.emplace_front(gname, pr); return optional(); // remove goal } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 5610bdf7f..40de4e172 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -215,7 +215,7 @@ tactic trivial_tactic() { goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional { expr const & c = env->normalize(g.get_conclusion(), context(), true); if (c == True) { - proofs.emplace_front(gname, Trivial); + proofs.emplace_front(gname, mk_trivial()); return optional(); } else { return some(g); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index b633f0b7d..bce0bd571 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -71,12 +71,12 @@ static void tst3() { } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } - env->add_definition("a", Int, iAdd(iVal(1), iVal(2))); + env->add_definition("a", Int, mk_Int_add(iVal(1), iVal(2))); std::cout << env << "\n"; - expr t = iAdd(Const("a"), iVal(1)); + expr t = mk_Int_add(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; lean_assert(normalize(t, env) == iVal(4)); - env->add_definition("b", Int, iMul(iVal(2), Const("a"))); + env->add_definition("b", Int, mk_Int_mul(iVal(2), Const("a"))); std::cout << "b --> " << normalize(Const("b"), env) << "\n"; lean_assert(normalize(Const("b"), env) == iVal(6)); try { @@ -111,21 +111,21 @@ static void tst4() { std::cout << "tst4\n"; environment env; init_test_frontend(env); env->add_definition("a", Int, iVal(1), true); // add opaque definition - expr t = iAdd(Const("a"), iVal(1)); + expr t = mk_Int_add(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; lean_assert(normalize(t, env) == t); - env->add_definition("b", Int, iAdd(Const("a"), iVal(1))); - expr t2 = iSub(Const("b"), iVal(9)); + env->add_definition("b", Int, mk_Int_add(Const("a"), iVal(1))); + expr t2 = mk_Int_sub(Const("b"), iVal(9)); std::cout << t2 << " --> " << normalize(t2, env) << "\n"; lean_assert_eq(normalize(t2, env, context()), - iSub(iAdd(Const("a"), iVal(1)), iVal(9))); + mk_Int_sub(mk_Int_add(Const("a"), iVal(1)), iVal(9))); } static void tst5() { environment env; init_test_frontend(env); env->add_definition("a", Int, iVal(1), true); // add opaque definition try { - std::cout << type_check(iAdd(Const("a"), Int), env) << "\n"; + std::cout << type_check(mk_Int_add(Const("a"), Int), env) << "\n"; lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; @@ -163,10 +163,6 @@ static void tst7() { environment env; init_test_frontend(env); env->add_var("a", Int); env->add_var("b", Int); - expr t = If(Int, True, Const("a"), Const("b")); - std::cout << t << " --> " << normalize(t, env) << "\n"; - std::cout << type_check(t, env) << "\n"; - std::cout << "Environment\n" << env; } static void tst8() { @@ -208,11 +204,11 @@ static void tst10() { expr a = Const("a"); expr b = Const("b"); expr c = Const("c"); - env->add_definition("b", Int, iAdd(a, a)); + env->add_definition("b", Int, mk_Int_add(a, a)); lean_assert(env->get_object("b").get_weight() == 2); - env->add_definition("c", Int, iAdd(a, b)); + env->add_definition("c", Int, mk_Int_add(a, b)); lean_assert(env->get_object("c").get_weight() == 3); - env->add_definition("d", Int, iAdd(b, b)); + env->add_definition("d", Int, mk_Int_add(b, b)); lean_assert(env->get_object("d").get_weight() == 3); } diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 6a9d5f7ed..cb2702554 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -76,8 +76,8 @@ static unsigned depth2(expr const & e) { std::accumulate(begin_args(e), end_args(e), 0, [](unsigned m, expr const & arg){ return std::max(depth2(arg), m); }) + 1; - case expr_kind::Eq: - return std::max(depth2(eq_lhs(e)), depth2(eq_rhs(e))) + 1; + case expr_kind::HEq: + return std::max(depth2(heq_lhs(e)), depth2(heq_rhs(e))) + 1; case expr_kind::Lambda: case expr_kind::Pi: return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1; case expr_kind::Let: @@ -135,8 +135,8 @@ static unsigned count_core(expr const & a, expr_set & s) { case expr_kind::App: return std::accumulate(begin_args(a), end_args(a), 1, [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); }); - case expr_kind::Eq: - return count_core(eq_lhs(a), s) + count_core(eq_rhs(a), s) + 1; + case expr_kind::HEq: + return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1; case expr_kind::Let: @@ -295,7 +295,7 @@ static void tst13() { } static void tst14() { - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); check_serializer(t); std::cout << t << "\n"; expr l = mk_let("a", none_expr(), Const("b"), Var(0)); @@ -329,9 +329,9 @@ static void tst15() { lean_assert(has_metavar(f(a, a, m))); lean_assert(has_metavar(f(a, m, a, a))); lean_assert(!has_metavar(f(a, a, a, a))); - lean_assert(!has_metavar(Eq(a, f(a)))); - lean_assert(has_metavar(Eq(m, f(a)))); - lean_assert(has_metavar(Eq(a, f(m)))); + lean_assert(!has_metavar(HEq(a, f(a)))); + lean_assert(has_metavar(HEq(m, f(a)))); + lean_assert(has_metavar(HEq(a, f(m)))); } static void check_copy(expr const & e) { @@ -346,7 +346,7 @@ static void tst16() { expr a = Const("a"); check_copy(iVal(10)); check_copy(f(a)); - check_copy(Eq(f(a), a)); + check_copy(HEq(f(a), a)); check_copy(mk_metavar("M")); check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_pi("x", a, Var(0))); diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index cc13f722c..6128106d4 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -75,11 +75,11 @@ static void tst4() { lean_assert(fn(Fun({x, Type()}, Var(0))) == 0); lean_assert(fn(Fun({x, Var(0)}, Var(0))) == 1); lean_assert(fn(Fun({x, Var(0)}, Var(2))) == 2); - lean_assert(fn(Fun({x, Var(0)}, Eq(Var(2), Var(1)))) == 2); + lean_assert(fn(Fun({x, Var(0)}, HEq(Var(2), Var(1)))) == 2); lean_assert(fn(Pi({x, Type()}, Var(0))) == 0); lean_assert(fn(Pi({x, Var(0)}, Var(0))) == 1); lean_assert(fn(Pi({x, Var(0)}, Var(2))) == 2); - lean_assert(fn(Pi({x, Var(0)}, Eq(Var(2), Var(1)))) == 2); + lean_assert(fn(Pi({x, Var(0)}, HEq(Var(2), Var(1)))) == 2); context ctx; ctx = extend(ctx, name("x"), Bool); ctx = extend(ctx, name("y"), Bool); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index cd3f45aa4..530c3caae 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -275,7 +275,7 @@ static void tst14() { expr y = Const("y"); env->add_var("h", Pi({N, Type()}, N >> (N >> N))); expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}}, - (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a)); + (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a)); metavar_env menv2 = menv.copy(); menv2->assign(m1, h(Var(4), Var(1), Var(3))); normalizer norm(env); @@ -288,10 +288,10 @@ static void tst14() { lean_assert(menv2->instantiate_metavars(norm(F1)) == norm(menv2->instantiate_metavars(F1))); expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}}, - (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M); + (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a, m2)))(M); std::cout << norm(F2) << "\n"; expr F3 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}}, - (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(b, m2)))(M); + (Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(b, m2)))(M); std::cout << norm(F3) << "\n"; } diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 6b40a588f..d1a94ab21 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -76,8 +76,8 @@ unsigned count_core(expr const & a, expr_set & s) { case expr_kind::App: return std::accumulate(begin_args(a), end_args(a), 1, [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); }); - case expr_kind::Eq: - return count_core(eq_lhs(a), s) + count_core(eq_rhs(a), s) + 1; + case expr_kind::HEq: + return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1; case expr_kind::Let: @@ -197,9 +197,9 @@ static void tst3() { env->add_var("a", Bool); expr t1 = Const("a"); expr t2 = Const("a"); - expr e = Eq(t1, t2); + expr e = HEq(t1, t2); std::cout << e << " --> " << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == Eq(t1, t2)); + lean_assert(normalize(e, env) == HEq(t1, t2)); } static void tst4() { @@ -286,7 +286,7 @@ static void tst8() { expr P = Const("P"); expr v0 = Var(0); expr v1 = Var(1); - expr F = mk_forall(Int, mk_lambda("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0)))); + expr F = mk_pi("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0))); normalizer proc(env); expr N1 = proc(F); expr N2 = proc(deep_copy(F)); diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index fe31fe4d4..1c1a803f9 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -80,7 +80,7 @@ static void tst2() { static void tst3() { environment env; init_test_frontend(env); - expr f = Fun("a", Bool, Eq(Const("a"), True)); + expr f = Fun("a", Bool, HEq(Const("a"), True)); std::cout << type_check(f, env) << "\n"; lean_assert(type_check(f, env) == mk_arrow(Bool, Bool)); expr t = mk_let("a", none_expr(), True, Var(0)); @@ -90,7 +90,7 @@ static void tst3() { static void tst4() { environment env; init_test_frontend(env); - expr a = Eq(iVal(1), iVal(2)); + expr a = HEq(iVal(1), iVal(2)); expr pr = mk_lambda("x", a, Var(0)); std::cout << type_check(pr, env) << "\n"; } @@ -105,7 +105,7 @@ static void tst5() { expr prop = P; expr pr = H; for (unsigned i = 1; i < n; i++) { - pr = Conj(P, prop, H, pr); + pr = mk_and_intro_th(P, prop, H, pr); prop = And(P, prop); } } @@ -191,8 +191,8 @@ static void tst10() { expr t1 = Let({{a, f(b)}, {a, f(a)}}, f(a)); expr t2 = f(f(f(b))); std::cout << t1 << " --> " << normalize(t1, env) << "\n"; - expr prop = Eq(t1, t2); - expr proof = Refl(Int, t1); + expr prop = HEq(t1, t2); + expr proof = mk_refl_th(Int, t1); env->add_theorem("simp_eq", prop, proof); std::cout << env->get_object("simp_eq").get_name() << "\n"; } @@ -215,8 +215,8 @@ static void tst11() { t3 = f(t3, t3); } lean_assert(t1 != t2); - env->add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1)); - env->add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1)); + env->add_theorem("eqs1", HEq(t1, t2), mk_refl_th(Int, t1)); + env->add_theorem("eqs2", HEq(t1, t3), mk_refl_th(Int, t1)); } static expr mk_big(unsigned depth) { @@ -257,7 +257,7 @@ static void tst13() { env->add_var("f", Type() >> Type()); expr f = Const("f"); std::cout << type_check(f(Bool), env) << "\n"; - std::cout << type_check(f(Eq(True, False)), env) << "\n"; + std::cout << type_check(f(HEq(True, False)), env) << "\n"; } static void tst14() { @@ -383,8 +383,8 @@ static void tst18() { lean_assert(type_of(f(a, a)) == Int); lean_assert(type_of(f(a)) == Int >> Int); lean_assert(is_bool(type_of(And(a, f(a))))); - lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int); - lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int); + lean_assert(type_of(Fun({a, Int}, mk_Int_add(a, iVal(1)))) == Int >> Int); + lean_assert(type_of(Let({a, iVal(10)}, mk_Int_add(a, b))) == Int); lean_assert(type_of(Type()) == Type(level() + 1)); lean_assert(type_of(Bool) == Type()); lean_assert(type_of(Pi({a, Type()}, Type(level() + 2))) == Type(level() + 3)); @@ -399,7 +399,7 @@ static expr mk_big(unsigned val, unsigned depth) { if (depth == 0) return iVal(val); else - return iAdd(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1)); + return mk_Int_add(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1)); } static void tst19() { diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index df6e2b9cc..0c4e984fd 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -22,28 +22,28 @@ static void tst0() { env->add_var("n", Nat); expr n = Const("n"); lean_assert_eq(mk_nat_type(), Nat); - lean_assert_eq(norm(nMul(nVal(2), nVal(3))), nVal(6)); - lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True); - lean_assert_eq(norm(nLe(nVal(5), nVal(3))), False); - lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True); - lean_assert_eq(norm(nLe(n, nVal(3))), nLe(n, nVal(3))); + lean_assert_eq(norm(mk_Nat_mul(nVal(2), nVal(3))), nVal(6)); + lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True); + lean_assert_eq(norm(mk_Nat_le(nVal(5), nVal(3))), False); + lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True); + lean_assert_eq(norm(mk_Nat_le(n, nVal(3))), mk_Nat_le(n, nVal(3))); env->add_var("x", Real); expr x = Const("x"); lean_assert_eq(mk_real_type(), Real); - lean_assert_eq(norm(rMul(rVal(2), rVal(3))), rVal(6)); - lean_assert_eq(norm(rDiv(rVal(2), rVal(0))), rVal(0)); - lean_assert_eq(norm(rLe(rVal(2), rVal(3))), True); - lean_assert_eq(norm(rLe(rVal(5), rVal(3))), False); - lean_assert_eq(norm(rLe(rVal(2), rVal(3))), True); - lean_assert_eq(norm(rLe(x, rVal(3))), rLe(x, rVal(3))); + lean_assert_eq(norm(mk_Real_mul(rVal(2), rVal(3))), rVal(6)); + lean_assert_eq(norm(mk_Real_div(rVal(2), rVal(0))), rVal(0)); + lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True); + lean_assert_eq(norm(mk_Real_le(rVal(5), rVal(3))), False); + lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True); + lean_assert_eq(norm(mk_Real_le(x, rVal(3))), mk_Real_le(x, rVal(3))); env->add_var("i", Int); expr i = Const("i"); - lean_assert_eq(norm(i2r(i)), i2r(i)); - lean_assert_eq(norm(i2r(iVal(2))), rVal(2)); + lean_assert_eq(norm(mk_int_to_real(i)), mk_int_to_real(i)); + lean_assert_eq(norm(mk_int_to_real(iVal(2))), rVal(2)); lean_assert_eq(mk_int_type(), Int); - lean_assert_eq(norm(n2i(n)), n2i(n)); - lean_assert_eq(norm(n2i(nVal(2))), iVal(2)); - lean_assert_eq(norm(iDiv(iVal(2), iVal(0))), iVal(0)); + lean_assert_eq(norm(mk_nat_to_int(n)), mk_nat_to_int(n)); + lean_assert_eq(norm(mk_nat_to_int(nVal(2))), iVal(2)); + lean_assert_eq(norm(mk_Int_div(iVal(2), iVal(0))), iVal(0)); } static void tst1() { @@ -58,76 +58,76 @@ static void tst1() { static void tst2() { environment env; init_test_frontend(env); - expr e = iAdd(iVal(10), iVal(30)); + expr e = mk_Int_add(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; lean_assert(normalize(e, env) == iVal(40)); - std::cout << type_check(mk_int_add_fn(), env) << "\n"; + std::cout << type_check(mk_Int_add_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); - lean_assert(type_check(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int)); + lean_assert(type_check(mk_app(mk_Int_add_fn(), iVal(10)), env) == (Int >> Int)); lean_assert(is_int_value(normalize(e, env))); - expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30)))); + expr e2 = Fun("a", Int, mk_Int_add(Const("a"), mk_Int_add(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == mk_arrow(Int, Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(40)))); + lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_add(Const("a"), iVal(40)))); } static void tst3() { environment env; init_test_frontend(env); - expr e = iMul(iVal(10), iVal(30)); + expr e = mk_Int_mul(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; lean_assert(normalize(e, env) == iVal(300)); - std::cout << type_check(mk_int_mul_fn(), env) << "\n"; + std::cout << type_check(mk_Int_mul_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); - lean_assert(type_check(mk_app(mk_int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int)); + lean_assert(type_check(mk_app(mk_Int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int)); lean_assert(is_int_value(normalize(e, env))); - expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30)))); + expr e2 = Fun("a", Int, mk_Int_mul(Const("a"), mk_Int_mul(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == (Int >> Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iMul(Const("a"), iVal(300)))); + lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_mul(Const("a"), iVal(300)))); } static void tst4() { environment env; init_test_frontend(env); - expr e = iSub(iVal(10), iVal(30)); + expr e = mk_Int_sub(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; lean_assert(normalize(e, env, context(), true) == iVal(-20)); - std::cout << type_check(mk_int_sub_fn(), env) << "\n"; + std::cout << type_check(mk_Int_sub_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); - lean_assert(type_check(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); + lean_assert(type_check(mk_app(mk_Int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); lean_assert(is_int_value(normalize(e, env, context(), true))); - expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30)))); + expr e2 = Fun("a", Int, mk_Int_sub(Const("a"), mk_Int_sub(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == (Int >> Int)); - lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, iAdd(Const("a"), iVal(20)))); + lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, mk_Int_add(Const("a"), iVal(20)))); } static void tst5() { environment env; init_test_frontend(env); env->add_var(name("a"), Int); - expr e = Eq(iVal(3), iVal(4)); + expr e = HEq(iVal(3), iVal(4)); std::cout << e << " --> " << normalize(e, env) << "\n"; lean_assert(normalize(e, env) == False); - lean_assert(normalize(Eq(Const("a"), iVal(3)), env) == Eq(Const("a"), iVal(3))); + lean_assert(normalize(HEq(Const("a"), iVal(3)), env) == HEq(Const("a"), iVal(3))); } static void tst6() { std::cout << "tst6\n"; - std::cout << mk_int_add_fn().raw() << "\n"; - std::cout << mk_int_add_fn().raw() << "\n"; + std::cout << mk_Int_add_fn().raw() << "\n"; + std::cout << mk_Int_add_fn().raw() << "\n"; #ifndef __APPLE__ - thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; }); + thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_Int_add_fn().raw() << "\n"; }); t1.join(); - thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; }); + thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_Int_add_fn().raw() << "\n"; }); t2.join(); #endif - std::cout << mk_int_add_fn().raw() << "\n"; + std::cout << mk_Int_add_fn().raw() << "\n"; } int main() { diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp index b1e8b3c2f..dce67335d 100644 --- a/src/tests/library/deep_copy.cpp +++ b/src/tests/library/deep_copy.cpp @@ -18,7 +18,7 @@ static void tst1() { expr z = Const("z"); local_context lctx{mk_lift(0, 1), mk_inst(0, a)}; expr m = mk_metavar("a", lctx); - expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m))))); + expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), HEq(x, m))))); expr G = deep_copy(F); lean_assert(F == G); lean_assert(!is_eqp(F, G)); diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index f6693a0db..38a68587b 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -95,7 +95,7 @@ static void tst2() { expr F = m1(g(m2, m3(a)), m4(nVal(0))); std::cout << F << "\n"; std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); + ucs.push_back(mk_choice_constraint(context(), m1, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); elaborator elb(env, menv, ucs.size(), ucs.data()); @@ -138,7 +138,7 @@ static void tst3() { expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a)); std::cout << F << "\n"; std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); + ucs.push_back(mk_choice_constraint(context(), m2, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification())); elaborator elb(env, menv, ucs.size(), ucs.data()); @@ -183,7 +183,7 @@ static void tst4() { expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b); std::cout << F << "\n"; std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); + ucs.push_back(mk_choice_constraint(context(), m3, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification())); elaborator elb(env, menv, ucs.size(), ucs.data()); elb.next(); @@ -257,10 +257,10 @@ static void tst6() { env->add_var("f", Int >> (Int >> Int)); env->add_var("a", Int); env->add_var("b", Int); - env->add_axiom("H1", Eq(f(a, f(a, b)), a)); - env->add_axiom("H2", Eq(a, b)); - expr V = Subst(m1, m2, m3, m4, H1, H2); - expr expected = Eq(f(a, f(b, b)), a); + env->add_axiom("H1", HEq(f(a, f(a, b)), a)); + env->add_axiom("H2", HEq(a, b)); + expr V = mk_subst_th(m1, m2, m3, m4, H1, H2); + expr expected = HEq(f(a, f(b, b)), a); expr given = checker.check(V, context(), menv, ucs); ucs.push_back(mk_eq_constraint(context(), expected, given, justification())); elaborator elb(env, menv, ucs.size(), ucs.data()); @@ -339,17 +339,17 @@ static void tst8() { env->add_var("a", Bool); env->add_var("b", Bool); env->add_var("c", Bool); - env->add_axiom("H1", Eq(a, b)); - env->add_axiom("H2", Eq(b, c)); - success(Trans(_, _, _, _, H1, H2), Trans(Bool, a, b, c, H1, H2), env); - success(Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)), - Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1)), env); - success(Symm(_, _, _, Trans(_, _ , _ , _ , Symm(_, _, _, H2), Symm(_, _, _, H1))), - Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), env); + env->add_axiom("H1", HEq(a, b)); + env->add_axiom("H2", HEq(b, c)); + success(mk_trans_th(_, _, _, _, H1, H2), mk_trans_th(Bool, a, b, c, H1, H2), env); + success(mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)), + mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1)), env); + success(mk_symm_th(_, _, _, mk_trans_th(_, _ , _ , _ , mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), + mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), env); env->add_axiom("H3", a); expr H3 = Const("H3"); - success(EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3)), - EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3)), + success(mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3)), + mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3)), env); } @@ -370,19 +370,19 @@ static void tst9() { expr fact = Const("fact"); env->add_var("a", Nat); env->add_var("b", Nat); - env->add_definition("fact", Bool, Eq(a, b)); + env->add_definition("fact", Bool, HEq(a, b)); env->add_axiom("H", fact); - success(Congr2(_, _, _, _, f, H), - Congr2(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env); + success(mk_congr2_th(_, _, _, _, f, H), + mk_congr2_th(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env); env->add_var("g", Pi({n, Nat}, vec(n) >> Nat)); expr g = Const("g"); - env->add_axiom("H2", Eq(f, g)); + env->add_axiom("H2", HEq(f, g)); expr H2 = Const("H2"); - success(Congr(_, _, _, _, _, _, H2, H), - Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env); - success(Congr(_, _, _, _, _, _, Refl(_, f), H), - Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat), f), H), env); - success(Refl(_, a), Refl(Nat, a), env); + success(mk_congr_th(_, _, _, _, _, _, H2, H), + mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env); + success(mk_congr_th(_, _, _, _, _, _, mk_refl_th(_, f), H), + mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(n) >> Nat), f), H), env); + success(mk_refl_th(_, a), mk_refl_th(Nat, a), env); } static void tst10() { @@ -402,11 +402,11 @@ static void tst10() { expr z = Const("z"); success(Fun({{x, _}, {y, _}}, f(x, y)), Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env); - success(Fun({{x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))), - Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env); + success(Fun({{x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))), + Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env); expr A = Const("A"); - success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))), - Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env); + success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))), + Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env); } static void tst11() { @@ -464,11 +464,11 @@ static void tst13() { Fun({{A, Type()}, {x, A}}, f(A, x)), env); success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)), Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))), - Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))), - Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env); - unsolved(Fun({{A, _}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))), env); + success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))), + Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env); + success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))), + Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env); + unsolved(Fun({{A, _}, {B, _}, {x, _}}, HEq(f(B, x), f(_, x))), env); } static void tst14() { @@ -495,20 +495,20 @@ static void tst14() { env); success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, - Fun({{x, _}, {y, _}}, Eq(f(_, x), f(_, y))), + Fun({{x, _}, {y, _}}, HEq(f(_, x), f(_, y))), Fun({{x, N}, {y, Bool}}, True))), Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g((N >> (Bool >> Bool)), - Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))), + Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))), Fun({{x, N}, {y, Bool}}, True))), env); success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, - Fun({{x, N}, {y, _}}, Eq(f(_, x), f(_, y))), + Fun({{x, N}, {y, _}}, HEq(f(_, x), f(_, y))), Fun({{x, _}, {y, Bool}}, True))), Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g((N >> (Bool >> Bool)), - Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))), + Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))), Fun({{x, N}, {y, Bool}}, True))), env); } @@ -550,29 +550,29 @@ static void tst16() { env->add_var("a", Bool); env->add_var("b", Bool); env->add_var("c", Bool); - success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Trans(_, _, _, _, H1, H2)), - Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Trans(Bool, a, b, c, H1, H2)), + success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}}, + mk_trans_th(_, _, _, _, H1, H2)), + Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}}, + mk_trans_th(Bool, a, b, c, H1, H2)), env); expr H3 = Const("H3"); - success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, - EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))), - Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, - EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))), + success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))), + Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))), env); environment env2; init_test_frontend(env2); - success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, - EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))), - Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}}, - EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))), + success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))), + Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))), env2); expr A = Const("A"); - success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)))), - Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Symm(A, c, a, Trans(A, c, b, a, Symm(A, b, c, H2), Symm(A, a, b, H1)))), + success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}}, + mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)))), + Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}}, + mk_symm_th(A, c, a, mk_trans_th(A, c, b, a, mk_symm_th(A, b, c, H2), mk_symm_th(A, a, b, H1)))), env2); } @@ -682,7 +682,7 @@ void tst21() { expr b = Const("b"); expr m1 = menv->mk_metavar(); expr l = m1(b, a); - expr r = Fun({x, N}, f(x, Eq(a, b))); + expr r = Fun({x, N}, f(x, HEq(a, b))); elaborator elb(env, menv, context(), l, r); while (true) { try { @@ -715,8 +715,8 @@ void tst22() { expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); - expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1)))); - expr r = f(m2(b), iAdd(iVal(1), iVal(2))); + expr l = f(m1(a), mk_Int_add(m3, mk_Int_add(iVal(1), iVal(1)))); + expr r = f(m2(b), mk_Int_add(iVal(1), iVal(2))); elaborator elb(env, menv, context(), l, r); while (true) { try { @@ -745,8 +745,8 @@ void tst23() { expr f = Const("f"); expr m1 = menv->mk_metavar(); expr m2 = menv->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))); + expr l = Fun({{x, N}, {y, N}}, HEq(y, f(x, m1))); + expr r = Fun({{x, N}, {y, N}}, HEq(m2, f(m1, x))); elaborator elb(env, menv, context(), l, r); while (true) { try { @@ -832,13 +832,13 @@ void tst26() { expr a = Const("a"); env->add_var("a", Type(level()+1)); expr m1 = menv->mk_metavar(); - expr F = Eq(g(m1, a), a); + expr F = HEq(g(m1, a), a); std::cout << F << "\n"; std::cout << checker.check(F, context(), menv, ucs) << "\n"; elaborator elb(env, menv, ucs.size(), ucs.data()); metavar_env s = elb.next(); std::cout << s->instantiate_metavars(F) << "\n"; - lean_assert_eq(s->instantiate_metavars(F), Eq(g(Type(level()+1), a), a)); + lean_assert_eq(s->instantiate_metavars(F), HEq(g(Type(level()+1), a), a)); } void tst27() { diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp index 53a0ed92d..ea6374a1a 100644 --- a/src/tests/library/expr_lt.cpp +++ b/src/tests/library/expr_lt.cpp @@ -34,10 +34,10 @@ static void tst1() { lt(Const("a"), Const("b"), true); lt(Const("a"), Const("a"), false); lt(Var(1), Const("a"), true); - lt(Eq(Var(0), Var(1)), Eq(Var(1), Var(1)), true); - lt(Eq(Var(1), Var(0)), Eq(Var(1), Var(1)), true); - lt(Eq(Var(1), Var(1)), Eq(Var(1), Var(1)), false); - lt(Eq(Var(2), Var(1)), Eq(Var(1), Var(1)), false); + lt(HEq(Var(0), Var(1)), HEq(Var(1), Var(1)), true); + lt(HEq(Var(1), Var(0)), HEq(Var(1), Var(1)), true); + lt(HEq(Var(1), Var(1)), HEq(Var(1), Var(1)), false); + lt(HEq(Var(2), Var(1)), HEq(Var(1), Var(1)), false); lt(Const("f")(Var(0)), Const("f")(Var(0), Const("a")), true); lt(Const("f")(Var(0), Const("a"), Const("b")), Const("f")(Var(0), Const("a")), false); lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true); diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 7e55baa78..1f7d14d04 100644 --- a/src/tests/library/formatter.cpp +++ b/src/tests/library/formatter.cpp @@ -30,13 +30,13 @@ static void tst1() { expr x = Const("x"); expr y = Const("y"); expr N = Const("N"); - expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a))))); + expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(HEq(x, f(y, a))))); check(fmt(F), "fun x : (Pi x : N, (x#0 -> x#1)), (let y := f a in (f (x#1 == (f y#0 a))))"); check(fmt(env->get_object("N")), "variable N : Type"); context ctx; ctx = extend(ctx, "x", f(a)); ctx = extend(ctx, "y", f(Var(0), N >> N)); - ctx = extend(ctx, "z", N, Eq(Var(0), Var(1))); + ctx = extend(ctx, "z", N, HEq(Var(0), Var(1))); check(fmt(ctx), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1]"); check(fmt(ctx, f(Var(0), Var(2))), "f z#0 x#2"); check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1] |- f z#0 x#2"); diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp index 11fc67302..f614a789f 100644 --- a/src/tests/library/max_sharing.cpp +++ b/src/tests/library/max_sharing.cpp @@ -15,10 +15,10 @@ static void tst1() { max_sharing_fn max_fn; expr a1 = Const("a"); expr a2 = Const("a"); - expr F1 = Eq(a1, a2); - lean_assert(!is_eqp(eq_lhs(F1), eq_rhs(F1))); + expr F1 = HEq(a1, a2); + lean_assert(!is_eqp(heq_lhs(F1), heq_rhs(F1))); expr F2 = max_fn(F1); - lean_assert(is_eqp(eq_lhs(F2), eq_rhs(F2))); + lean_assert(is_eqp(heq_lhs(F2), heq_rhs(F2))); expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); diff --git a/src/tests/library/rewriter/fo_match.cpp b/src/tests/library/rewriter/fo_match.cpp index 580bbe9cb..62681b7df 100644 --- a/src/tests/library/rewriter/fo_match.cpp +++ b/src/tests/library/rewriter/fo_match.cpp @@ -273,7 +273,7 @@ static void match_let_tst1() { static void match_let_tst2() { cout << "--- match_let_tst2() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l = mk_let("a", Type(), Const("b"), Var(0)); subst_map s; bool result = test_match(l, t, 0, s); @@ -283,7 +283,7 @@ static void match_let_tst2() { static void match_let_tst3() { cout << "--- match_let_tst3() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Var(0), Const("b"), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Var(0)); subst_map s; @@ -295,7 +295,7 @@ static void match_let_tst3() { static void match_let_tst4() { cout << "--- match_let_tst4() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Nat, Const("b"), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Var(0)); subst_map s; @@ -306,7 +306,7 @@ static void match_let_tst4() { static void match_let_tst5() { cout << "--- match_let_tst5() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Int, Var(3), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Const("b")); subst_map s; @@ -317,7 +317,7 @@ static void match_let_tst5() { static void match_let_tst6() { cout << "--- match_let_tst6() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Var(0), Var(1), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Const("b")); subst_map s; @@ -328,7 +328,7 @@ static void match_let_tst6() { static void match_let_tst7() { cout << "--- match_let_tst7() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Var(0), Var(1), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Var(0)); subst_map s; @@ -341,7 +341,7 @@ static void match_let_tst7() { static void match_let_tst8() { cout << "--- match_let_tst8() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Nat, Var(1), Var(0)); expr l2 = mk_let("a", Int, Const("b"), Var(0)); subst_map s; @@ -352,7 +352,7 @@ static void match_let_tst8() { static void match_let_tst9() { cout << "--- match_let_tst9() ---" << endl; - expr t = Eq(Const("a"), Const("b")); + expr t = HEq(Const("a"), Const("b")); expr l1 = mk_let("a", Var(0), Var(0), Var(0)); expr l2 = mk_let("a", Nat, Const("b"), Const("a")); subst_map s; @@ -367,7 +367,7 @@ static void match_eq_tst1() { expr f = Const("f"); expr a = Const("a"); subst_map s; - bool result = test_match(mk_eq(x, a), mk_eq(f, a), 0, s); + bool result = test_match(mk_heq(x, a), mk_heq(f, a), 0, s); lean_assert_eq(result, true); lean_assert_eq(s.find(0)->second, f); lean_assert_eq(s.size(), 1); @@ -379,7 +379,7 @@ static void match_eq_tst2() { expr f = Const("f"); expr a = Const("a"); subst_map s; - bool result = test_match(mk_eq(nAdd(x, a), x), mk_eq(nAdd(f, a), f), 0, s); + bool result = test_match(mk_heq(mk_Nat_add(x, a), x), mk_heq(mk_Nat_add(f, a), f), 0, s); lean_assert_eq(result, true); lean_assert_eq(s.find(0)->second, f); lean_assert_eq(s.size(), 1); @@ -391,7 +391,7 @@ static void match_eq_tst3() { expr f = Const("f"); expr a = Const("a"); subst_map s; - bool result = test_match(mk_eq(nAdd(x, a), x), f, 0, s); + bool result = test_match(mk_heq(mk_Nat_add(x, a), x), f, 0, s); lean_assert_eq(result, false); lean_assert_eq(s.empty(), true); } diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index ce58beeb2..e48216377 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -32,11 +32,11 @@ static void theorem_rewriter1_tst() { // Result : (b + a, ADD_COMM a b) expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); environment env; init_test_frontend(env); @@ -48,13 +48,13 @@ static void theorem_rewriter1_tst() { rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); context ctx; pair result = add_comm_thm_rewriter(env, ctx, a_plus_b); - expr concl = mk_eq(a_plus_b, result.first); + expr concl = mk_heq(a_plus_b, result.first); expr proof = result.second; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); + lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); env->add_theorem("New_theorem1", concl, proof); } @@ -66,9 +66,9 @@ static void theorem_rewriter2_tst() { // Result : (a, ADD_ID a) expr a = Const("a"); // a : at expr zero = nVal(0); // zero : Nat - expr a_plus_zero = nAdd(a, zero); + expr a_plus_zero = mk_Nat_add(a, zero); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -79,13 +79,13 @@ static void theorem_rewriter2_tst() { rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body); context ctx; pair result = add_id_thm_rewriter(env, ctx, a_plus_zero); - expr concl = mk_eq(a_plus_zero, result.first); + expr concl = mk_heq(a_plus_zero, result.first); expr proof = result.second; cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(a_plus_zero, a)); + lean_assert_eq(concl, mk_heq(a_plus_zero, a)); lean_assert_eq(proof, Const("ADD_ID")(a)); env->add_theorem("New_theorem2", concl, proof); } @@ -99,14 +99,14 @@ static void then_rewriter1_tst() { expr a = Const("a"); // a : Nat expr zero = nVal(0); // zero : Nat - expr a_plus_zero = nAdd(a, zero); - expr zero_plus_a = nAdd(zero, a); + expr a_plus_zero = mk_Nat_add(a, zero); + expr zero_plus_a = mk_Nat_add(zero, a); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -120,15 +120,15 @@ static void then_rewriter1_tst() { rewriter then_rewriter1 = mk_then_rewriter(add_comm_thm_rewriter, add_id_thm_rewriter); context ctx; pair result = then_rewriter1(env, ctx, zero_plus_a); - expr concl = mk_eq(zero_plus_a, result.first); + expr concl = mk_heq(zero_plus_a, result.first); expr proof = result.second; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(zero_plus_a, a)); - lean_assert(proof == Trans(Nat, zero_plus_a, a_plus_zero, a, + lean_assert_eq(concl, mk_heq(zero_plus_a, a)); + lean_assert(proof == mk_trans_th(Nat, zero_plus_a, a_plus_zero, a, Const("ADD_COMM")(zero, a), Const("ADD_ID")(a))); env->add_theorem("New_theorem3", concl, proof); @@ -147,22 +147,22 @@ static void then_rewriter2_tst() { expr a = Const("a"); // a : Nat expr zero = nVal(0); // zero : Nat - expr zero_plus_a = nAdd(zero, a); - expr a_plus_zero = nAdd(a, zero); - expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero)); - expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero); + expr zero_plus_a = mk_Nat_add(zero, a); + expr a_plus_zero = mk_Nat_add(a, zero); + expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero)); + expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -181,17 +181,17 @@ static void then_rewriter2_tst() { add_id_thm_rewriter}); context ctx; pair result = then_rewriter2(env, ctx, zero_plus_a_plus_zero); - expr concl = mk_eq(zero_plus_a_plus_zero, result.first); + expr concl = mk_heq(zero_plus_a_plus_zero, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a)); - lean_assert(proof == Trans(Nat, zero_plus_a_plus_zero, a_plus_zero, a, - Trans(Nat, zero_plus_a_plus_zero, zero_plus_a, a_plus_zero, - Trans(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a, + lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a)); + lean_assert(proof == mk_trans_th(Nat, zero_plus_a_plus_zero, a_plus_zero, a, + mk_trans_th(Nat, zero_plus_a_plus_zero, zero_plus_a, a_plus_zero, + mk_trans_th(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a, Const("ADD_ASSOC")(zero, a, zero), Const("ADD_ID")(zero_plus_a)), Const("ADD_COMM")(zero, a)), Const("ADD_ID")(a))); @@ -208,20 +208,20 @@ static void orelse_rewriter1_tst() { expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -238,7 +238,7 @@ static void orelse_rewriter1_tst() { add_id_thm_rewriter}); context ctx; pair result = add_assoc_or_comm_thm_rewriter(env, ctx, a_plus_b); - expr concl = mk_eq(a_plus_b, result.first); + expr concl = mk_heq(a_plus_b, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; @@ -246,7 +246,7 @@ static void orelse_rewriter1_tst() { cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); + lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); env->add_theorem("New_theorem5", concl, proof); } @@ -259,16 +259,16 @@ static void orelse_rewriter2_tst() { expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -304,20 +304,20 @@ static void try_rewriter1_tst() { expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -333,7 +333,7 @@ static void try_rewriter1_tst() { add_id_thm_rewriter}); context ctx; pair result = add_try_rewriter(env, ctx, a_plus_b); - expr concl = mk_eq(a_plus_b, result.first); + expr concl = mk_heq(a_plus_b, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; @@ -341,7 +341,7 @@ static void try_rewriter1_tst() { cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b)); + lean_assert_eq(concl, mk_heq(a_plus_b, a_plus_b)); lean_assert_eq(proof, Const("refl")(Nat, a_plus_b)); env->add_theorem("New_theorem6", concl, proof); } @@ -355,20 +355,20 @@ static void try_rewriter2_tst() { expr a = Const("a"); // a : Nat expr b = Const("b"); // b : Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -385,7 +385,7 @@ static void try_rewriter2_tst() { add_id_thm_rewriter}); context ctx; pair result = add_try_rewriter(env, ctx, a_plus_b); - expr concl = mk_eq(a_plus_b, result.first); + expr concl = mk_heq(a_plus_b, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; @@ -393,7 +393,7 @@ static void try_rewriter2_tst() { cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); + lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); env->add_theorem("try2", concl, proof); } @@ -410,11 +410,11 @@ static void app_rewriter1_tst() { expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); environment env; init_test_frontend(env); @@ -436,32 +436,32 @@ static void app_rewriter1_tst() { expr v = f1(nVal(0)); pair result = app_try_comm_rewriter(env, ctx, v); - expr concl = mk_eq(v, result.first); + expr concl = mk_heq(v, result.first); expr proof = result.second; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, f1(nVal(0)))); - lean_assert_eq(proof, Refl(Nat, f1(nVal(0)))); + lean_assert_eq(concl, mk_heq(v, f1(nVal(0)))); + lean_assert_eq(proof, mk_refl_th(Nat, f1(nVal(0)))); env->add_theorem("app_rewriter1", concl, proof); cout << "====================================================" << std::endl; v = f1(a_plus_b); result = app_try_comm_rewriter(env, ctx, v); - concl = mk_eq(v, result.first); + concl = mk_heq(v, result.first); proof = result.second; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, f1(b_plus_a))); + lean_assert_eq(concl, mk_heq(v, f1(b_plus_a))); lean_assert_eq(proof, Const("congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b))); env->add_theorem("app_rewriter2", concl, proof); cout << "====================================================" << std::endl; v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a); result = app_try_comm_rewriter(env, ctx, v); - concl = mk_eq(v, result.first); + concl = mk_heq(v, result.first); proof = result.second; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, f4(nVal(0), b_plus_a, nVal(0), a_plus_b))); + lean_assert_eq(concl, mk_heq(v, f4(nVal(0), b_plus_a, nVal(0), a_plus_b))); // Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a) lean_assert_eq(proof, @@ -489,22 +489,22 @@ static void repeat_rewriter1_tst() { expr a = Const("a"); // a : Nat expr zero = nVal(0); // zero : Nat - expr zero_plus_a = nAdd(zero, a); - expr a_plus_zero = nAdd(a, zero); - expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero)); - expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero); + expr zero_plus_a = mk_Nat_add(zero, a); + expr a_plus_zero = mk_Nat_add(a, zero); + expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero)); + expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -523,14 +523,14 @@ static void repeat_rewriter1_tst() { rewriter repeat_rw = mk_repeat_rewriter(or_rewriter); context ctx; pair result = repeat_rw(env, ctx, zero_plus_a_plus_zero); - expr concl = mk_eq(zero_plus_a_plus_zero, result.first); + expr concl = mk_heq(zero_plus_a_plus_zero, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a)); + lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a)); env->add_theorem("repeat_thm1", concl, proof); } @@ -547,22 +547,22 @@ static void repeat_rewriter2_tst() { expr a = Const("a"); // a : Nat expr zero = nVal(0); // zero : Nat - expr zero_plus_a = nAdd(zero, a); - expr a_plus_zero = nAdd(a, zero); - expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero)); - expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero); + expr zero_plus_a = mk_Nat_add(zero, a); + expr a_plus_zero = mk_Nat_add(a, zero); + expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero)); + expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero); expr add_assoc_thm_type = Pi("x", Nat, Pi("y", Nat, Pi("z", Nat, - Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))), - nAdd(nAdd(Const("x"), Const("y")), Const("z")))))); + HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))), + mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z")))))); expr add_assoc_thm_body = Const("ADD_ASSOC"); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); expr add_id_thm_type = Pi("x", Nat, - Eq(nAdd(Const("x"), zero), Const("x"))); + HEq(mk_Nat_add(Const("x"), zero), Const("x"))); expr add_id_thm_body = Const("ADD_ID"); environment env; init_test_frontend(env); @@ -582,14 +582,14 @@ static void repeat_rewriter2_tst() { rewriter repeat_rw = mk_repeat_rewriter(try_rw); context ctx; pair result = repeat_rw(env, ctx, zero_plus_a_plus_zero); - expr concl = mk_eq(zero_plus_a_plus_zero, result.first); + expr concl = mk_heq(zero_plus_a_plus_zero, result.first); expr proof = result.second; cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl; cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a)); + lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a)); env->add_theorem("repeat_thm2", concl, proof); } @@ -605,11 +605,11 @@ static void depth_rewriter1_tst() { expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); environment env; init_test_frontend(env); @@ -629,13 +629,13 @@ static void depth_rewriter1_tst() { cout << "RW = " << depth_rewriter << std::endl; - expr v = nAdd(f1(nAdd(a, b)), f3(a, b, nAdd(a, b))); + expr v = mk_Nat_add(f1(mk_Nat_add(a, b)), f3(a, b, mk_Nat_add(a, b))); pair result = depth_rewriter(env, ctx, v); - expr concl = mk_eq(v, result.first); + expr concl = mk_heq(v, result.first); expr proof = result.second; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, nAdd(f3(a, b, nAdd(b, a)), f1(nAdd(b, a))))); + lean_assert_eq(concl, mk_heq(v, mk_Nat_add(f3(a, b, mk_Nat_add(b, a)), f1(mk_Nat_add(b, a))))); env->add_theorem("depth_rewriter1", concl, proof); cout << "====================================================" << std::endl; } @@ -652,11 +652,11 @@ static void lambda_body_rewriter_tst() { expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat expr zero = nVal(0); // zero : Nat - expr a_plus_b = nAdd(a, b); - expr b_plus_a = nAdd(b, a); + expr a_plus_b = mk_Nat_add(a, b); + expr b_plus_a = mk_Nat_add(b, a); expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, - Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); environment env; init_test_frontend(env); @@ -673,27 +673,27 @@ static void lambda_body_rewriter_tst() { rewriter lambda_rewriter = mk_lambda_body_rewriter(add_comm_thm_rewriter); context ctx; cout << "RW = " << lambda_rewriter << std::endl; - expr v = mk_lambda("x", Nat, nAdd(b, a)); + expr v = mk_lambda("x", Nat, mk_Nat_add(b, a)); pair result = lambda_rewriter(env, ctx, v); - expr concl = mk_eq(v, result.first); + expr concl = mk_heq(v, result.first); expr proof = result.second; cout << "v = " << v << std::endl; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, b)))); + lean_assert_eq(concl, mk_heq(v, mk_lambda("x", Nat, mk_Nat_add(a, b)))); env->add_theorem("lambda_rewriter1", concl, proof); // Theorem: Pi(x y : N), x + y = y + x := ADD_COMM x y // Term : fun (x : Nat), (x + a) // Result : fun (x : Nat), (a + x) - v = mk_lambda("x", Nat, nAdd(Var(0), a)); + v = mk_lambda("x", Nat, mk_Nat_add(Var(0), a)); result = lambda_rewriter(env, ctx, v); - concl = mk_eq(v, result.first); + concl = mk_heq(v, result.first); proof = result.second; cout << "v = " << v << std::endl; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0))))); + lean_assert_eq(concl, mk_heq(v, mk_lambda("x", Nat, mk_Nat_add(a, Var(0))))); env->add_theorem("lambda_rewriter2", concl, proof); cout << "====================================================" << std::endl; } @@ -711,7 +711,7 @@ static void lambda_type_rewriter_tst() { env->add_var("b", Nat); expr vec = Const("vec"); env->add_var("vec", Type() >> (Nat >> Type())); // vec : Type -> Nat -> Type - expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x"))))); + expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x"))))); expr add_comm_thm_body = Const("ADD_COMM"); env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -719,14 +719,14 @@ static void lambda_type_rewriter_tst() { rewriter depth_rewriter = mk_depth_rewriter(try_rewriter); rewriter lambda_rewriter = mk_lambda_type_rewriter(depth_rewriter); - expr v = mk_lambda("x", vec(Nat, nAdd(a, b)), Var(0)); + expr v = mk_lambda("x", vec(Nat, mk_Nat_add(a, b)), Var(0)); pair result = lambda_rewriter(env, ctx, v); - expr concl = mk_eq(v, result.first); + expr concl = mk_heq(v, result.first); expr proof = result.second; cout << "v = " << v << std::endl; cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; - lean_assert_eq(concl, mk_eq(v, mk_lambda("x", vec(Nat, nAdd(b, a)), Var(0)))); + lean_assert_eq(concl, mk_heq(v, mk_lambda("x", vec(Nat, mk_Nat_add(b, a)), Var(0)))); env->add_theorem("lambda_type_rewriter", concl, proof); cout << "====================================================" << std::endl; } diff --git a/src/tests/library/update_expr.cpp b/src/tests/library/update_expr.cpp index 0664585cb..da79317fc 100644 --- a/src/tests/library/update_expr.cpp +++ b/src/tests/library/update_expr.cpp @@ -12,11 +12,11 @@ using namespace lean; static void tst1() { expr a = Const("a"); expr b = Const("b"); - expr eq1 = Eq(a, b); - expr eq2 = update_eq(eq1, a, a); - expr eq3 = update_eq(eq1, a, b); - lean_assert(eq_lhs(eq3) == a); - lean_assert(eq_rhs(eq3) == b); + expr eq1 = HEq(a, b); + expr eq2 = update_heq(eq1, a, a); + expr eq3 = update_heq(eq1, a, b); + lean_assert(heq_lhs(eq3) == a); + lean_assert(heq_rhs(eq3) == b); lean_assert(is_eqp(eq1, eq3)); } diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 8fb58abc7..7ae5fe8ce 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -26,8 +26,8 @@ local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Cons assert(not ok) print(msg) assert(child:normalize(Const("val2")) == Const("val2")) -child:add_theorem("Th1", Eq(iVal(0), iVal(0)), Const("trivial")) -child:add_axiom("H1", Eq(Const("x"), iVal(0))) +child:add_theorem("Th1", HEq(iVal(0), iVal(0)), Const("trivial")) +child:add_axiom("H1", HEq(Const("x"), iVal(0))) assert(child:has_object("H1")) local ctx = context(context(), "x", Const("Int"), iVal(10)) assert(child:normalize(Var(0), ctx) == iVal(10)) diff --git a/tests/lua/expr5.lua b/tests/lua/expr5.lua index e8342baa4..70f33e198 100644 --- a/tests/lua/expr5.lua +++ b/tests/lua/expr5.lua @@ -1,9 +1,9 @@ e = context_entry("a", Const("a")) n = e:get_body() -check_error(function() mk_eq(n, Const("a")) end) +check_error(function() mk_heq(n, Const("a")) end) print(Const("a") < Const("b")) check_error(function() mk_app(Const("a")) end) -print(mk_eq(Const("a"), Const("b"))) +print(mk_heq(Const("a"), Const("b"))) print(mk_pi("x", Const("N"), Var(0))) print(Pi("x", Const("N"), Const("x"))) assert(mk_pi("x", Const("N"), Var(0)) == Pi("x", Const("N"), Const("x"))) diff --git a/tests/lua/expr6.lua b/tests/lua/expr6.lua index fa7be96b2..6124dd912 100644 --- a/tests/lua/expr6.lua +++ b/tests/lua/expr6.lua @@ -22,7 +22,7 @@ function print_leaves(e, ctx) print("abstraction var name: " .. tostring(name)) print_leaves(domain, ctx) print_leaves(body, ctx:extend(name, domain)) - elseif k == expr_kind.Eq then + elseif k == expr_kind.HEq then local lhs, rhs = e:fields() print_leaves(lhs, ctx) print_leaves(rhs, ctx) @@ -43,6 +43,6 @@ local x, y, z = Consts("x, y, z") assert(is_expr(f)) local F = fun(h, mk_arrow(N, N), - Let(x, h(a), Eq(f(x), h(x)))) + Let(x, h(a), HEq(f(x), h(x)))) print(F) print_leaves(F, context()) diff --git a/tests/lua/expr8.lua b/tests/lua/expr8.lua index f99956853..4b9257c8b 100644 --- a/tests/lua/expr8.lua +++ b/tests/lua/expr8.lua @@ -25,7 +25,7 @@ assert(mk_metavar("M"):is_metavar()) assert(mk_real_value(mpq(10)):is_value()) assert(not F:has_metavar()) assert(f(mk_metavar("M")):has_metavar()) -assert(Eq(a, b):is_eq()) +assert(HEq(a, b):is_heq()) assert(F:num_args() == 3) assert(F:arg(0) == f) assert(F:arg(1) == g(x, a)) diff --git a/tests/lua/unify1.lua b/tests/lua/unify1.lua index 1408a2fdb..978e69396 100644 --- a/tests/lua/unify1.lua +++ b/tests/lua/unify1.lua @@ -16,7 +16,7 @@ function must_unify(t1, t2) assert(s:apply(t1) == s:apply(t2)) end Bool = Const("Bool") -must_unify(Eq(a, m1), Eq(m2, m2)) +must_unify(HEq(a, m1), HEq(m2, m2)) must_unify(Type(), m1) must_unify(fun(x, Bool, x), fun(x, Bool, m1)) must_unify(Pi(x, Bool, x), Pi(x, Bool, m1))