chore(library/arith): remove unnecessary library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
69bfc682b4
commit
cd30bb49c1
18 changed files with 0 additions and 1112 deletions
|
|
@ -215,8 +215,6 @@ add_subdirectory(kernel)
|
||||||
set(LEAN_LIBS ${LEAN_LIBS} kernel)
|
set(LEAN_LIBS ${LEAN_LIBS} kernel)
|
||||||
add_subdirectory(library)
|
add_subdirectory(library)
|
||||||
set(LEAN_LIBS ${LEAN_LIBS} library)
|
set(LEAN_LIBS ${LEAN_LIBS} library)
|
||||||
# add_subdirectory(library/arith)
|
|
||||||
# set(LEAN_LIBS ${LEAN_LIBS} arithlib)
|
|
||||||
# add_subdirectory(library/rewriter)
|
# add_subdirectory(library/rewriter)
|
||||||
# set(LEAN_LIBS ${LEAN_LIBS} rewriter)
|
# set(LEAN_LIBS ${LEAN_LIBS} rewriter)
|
||||||
# add_subdirectory(library/simplifier)
|
# add_subdirectory(library/simplifier)
|
||||||
|
|
|
||||||
|
|
@ -1,2 +0,0 @@
|
||||||
add_library(arithlib nat.cpp int.cpp real.cpp arith.cpp)
|
|
||||||
target_link_libraries(arithlib ${LEAN_LIBS})
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
/*
|
|
||||||
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"}));
|
|
||||||
}
|
|
||||||
|
|
@ -1,50 +0,0 @@
|
||||||
/*
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
inline expr mk_Nat_neg(expr const & e1) { return mk_app({mk_Nat_neg_fn(), e1}); }
|
|
||||||
}
|
|
||||||
|
|
@ -1,60 +0,0 @@
|
||||||
/*
|
|
||||||
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_induction_on_fn, name({"Nat", "induction_on"}));
|
|
||||||
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_left_comm_fn, name({"Nat", "add_left_comm"}));
|
|
||||||
MK_CONSTANT(Nat_mul_left_comm_fn, name({"Nat", "mul_left_comm"}));
|
|
||||||
MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"}));
|
|
||||||
MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"}));
|
|
||||||
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"}));
|
|
||||||
MK_CONSTANT(Nat_not_lt_0_fn, name({"Nat", "not_lt_0"}));
|
|
||||||
MK_CONSTANT(Nat_lt_intro_fn, name({"Nat", "lt_intro"}));
|
|
||||||
MK_CONSTANT(Nat_lt_elim_fn, name({"Nat", "lt_elim"}));
|
|
||||||
MK_CONSTANT(Nat_lt_le_fn, name({"Nat", "lt_le"}));
|
|
||||||
MK_CONSTANT(Nat_lt_ne_fn, name({"Nat", "lt_ne"}));
|
|
||||||
MK_CONSTANT(Nat_lt_nrefl_fn, name({"Nat", "lt_nrefl"}));
|
|
||||||
MK_CONSTANT(Nat_lt_trans_fn, name({"Nat", "lt_trans"}));
|
|
||||||
MK_CONSTANT(Nat_lt_le_trans_fn, name({"Nat", "lt_le_trans"}));
|
|
||||||
MK_CONSTANT(Nat_le_lt_trans_fn, name({"Nat", "le_lt_trans"}));
|
|
||||||
MK_CONSTANT(Nat_ne_lt_succ_fn, name({"Nat", "ne_lt_succ"}));
|
|
||||||
MK_CONSTANT(Nat_strong_induction_fn, name({"Nat", "strong_induction"}));
|
|
||||||
}
|
|
||||||
|
|
@ -1,164 +0,0 @@
|
||||||
/*
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
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_induction_on_fn();
|
|
||||||
bool is_Nat_induction_on_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_induction_on_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_on_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_left_comm_fn();
|
|
||||||
bool is_Nat_add_left_comm_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_add_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_left_comm_fn(), e1, e2, e3}); }
|
|
||||||
expr mk_Nat_mul_left_comm_fn();
|
|
||||||
bool is_Nat_mul_left_comm_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_mul_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_left_comm_fn(), e1, e2, e3}); }
|
|
||||||
expr mk_Nat_add_injr_fn();
|
|
||||||
bool is_Nat_add_injr_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_add_injr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injr_fn(), e1, e2, e3, e4}); }
|
|
||||||
expr mk_Nat_add_injl_fn();
|
|
||||||
bool is_Nat_add_injl_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_add_injl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injl_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}); }
|
|
||||||
expr mk_Nat_not_lt_0_fn();
|
|
||||||
bool is_Nat_not_lt_0_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_not_lt_0_th(expr const & e1) { return mk_app({mk_Nat_not_lt_0_fn(), e1}); }
|
|
||||||
expr mk_Nat_lt_intro_fn();
|
|
||||||
bool is_Nat_lt_intro_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_lt_intro_fn(), e1, e2, e3, e4}); }
|
|
||||||
expr mk_Nat_lt_elim_fn();
|
|
||||||
bool is_Nat_lt_elim_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_elim_fn(), e1, e2, e3}); }
|
|
||||||
expr mk_Nat_lt_le_fn();
|
|
||||||
bool is_Nat_lt_le_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_le_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_le_fn(), e1, e2, e3}); }
|
|
||||||
expr mk_Nat_lt_ne_fn();
|
|
||||||
bool is_Nat_lt_ne_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_ne_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_ne_fn(), e1, e2, e3}); }
|
|
||||||
expr mk_Nat_lt_nrefl_fn();
|
|
||||||
bool is_Nat_lt_nrefl_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_nrefl_th(expr const & e1) { return mk_app({mk_Nat_lt_nrefl_fn(), e1}); }
|
|
||||||
expr mk_Nat_lt_trans_fn();
|
|
||||||
bool is_Nat_lt_trans_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_trans_fn(), e1, e2, e3, e4, e5}); }
|
|
||||||
expr mk_Nat_lt_le_trans_fn();
|
|
||||||
bool is_Nat_lt_le_trans_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_lt_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_le_trans_fn(), e1, e2, e3, e4, e5}); }
|
|
||||||
expr mk_Nat_le_lt_trans_fn();
|
|
||||||
bool is_Nat_le_lt_trans_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_le_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_lt_trans_fn(), e1, e2, e3, e4, e5}); }
|
|
||||||
expr mk_Nat_ne_lt_succ_fn();
|
|
||||||
bool is_Nat_ne_lt_succ_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_ne_lt_succ_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_ne_lt_succ_fn(), e1, e2, e3, e4}); }
|
|
||||||
expr mk_Nat_strong_induction_fn();
|
|
||||||
bool is_Nat_strong_induction_fn(expr const & e);
|
|
||||||
inline expr mk_Nat_strong_induction_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_strong_induction_fn(), e1, e2, e3}); }
|
|
||||||
}
|
|
||||||
|
|
@ -1,17 +0,0 @@
|
||||||
/*
|
|
||||||
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"}));
|
|
||||||
}
|
|
||||||
|
|
@ -1,38 +0,0 @@
|
||||||
/*
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 3; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
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)) && num_args(e) == 2; }
|
|
||||||
inline expr mk_Real_abs(expr const & e1) { return mk_app({mk_Real_abs_fn(), e1}); }
|
|
||||||
}
|
|
||||||
|
|
@ -1,15 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#include "library/arith/arith.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
void import_arith(environment const & env, io_state const & ios) {
|
|
||||||
import_nat(env, ios);
|
|
||||||
import_int(env, ios);
|
|
||||||
import_real(env, ios);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,18 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#pragma once
|
|
||||||
#include "library/arith/nat.h"
|
|
||||||
#include "library/arith/int.h"
|
|
||||||
#include "library/arith/real.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
class environment;
|
|
||||||
/**
|
|
||||||
\brief Import all arithmetic related builtin libraries.
|
|
||||||
*/
|
|
||||||
void import_arith(environment const & env, io_state const & ios);
|
|
||||||
}
|
|
||||||
|
|
@ -1,162 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#include <string>
|
|
||||||
#include "kernel/abstract.h"
|
|
||||||
#include "kernel/environment.h"
|
|
||||||
#include "kernel/value.h"
|
|
||||||
#include "kernel/io_state.h"
|
|
||||||
#include "kernel/decl_macros.h"
|
|
||||||
#include "library/kernel_bindings.h"
|
|
||||||
#include "library/arith/int.h"
|
|
||||||
#include "library/arith/nat.h"
|
|
||||||
#include "library/arith/Int_decls.cpp"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
expr mk_nat_to_int_fn();
|
|
||||||
|
|
||||||
expr const Int = mk_Int();
|
|
||||||
expr mk_int_type() { return mk_Int(); }
|
|
||||||
|
|
||||||
class int_value_value : public value {
|
|
||||||
mpz m_val;
|
|
||||||
protected:
|
|
||||||
virtual bool lt(value const & other) const {
|
|
||||||
return m_val < static_cast<int_value_value const &>(other).m_val;
|
|
||||||
}
|
|
||||||
public:
|
|
||||||
int_value_value(mpz const & v):m_val(v) {}
|
|
||||||
virtual ~int_value_value() {}
|
|
||||||
virtual expr get_type() const { return Int; }
|
|
||||||
virtual name get_name() const { return name{"Int", "numeral"}; }
|
|
||||||
virtual bool operator==(value const & other) const {
|
|
||||||
int_value_value const * _other = dynamic_cast<int_value_value const*>(&other);
|
|
||||||
return _other && _other->m_val == m_val;
|
|
||||||
}
|
|
||||||
virtual void display(std::ostream & out) const { out << m_val; }
|
|
||||||
virtual format pp() const { return pp(false, false); }
|
|
||||||
virtual format pp(bool unicode, bool coercion) const {
|
|
||||||
if (coercion && m_val >= 0)
|
|
||||||
return format{to_value(mk_nat_to_int_fn()).pp(unicode, coercion), space(), format(m_val)};
|
|
||||||
else
|
|
||||||
return format(m_val);
|
|
||||||
}
|
|
||||||
virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion || m_val < 0; }
|
|
||||||
virtual unsigned hash() const { return m_val.hash(); }
|
|
||||||
virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
|
|
||||||
mpz const & get_num() const { return m_val; }
|
|
||||||
virtual void write(serializer & s) const { s << "int" << m_val; }
|
|
||||||
};
|
|
||||||
|
|
||||||
expr mk_int_value(mpz const & v) {
|
|
||||||
return mk_value(*(new int_value_value(v)));
|
|
||||||
}
|
|
||||||
static value::register_deserializer_fn int_value_ds("int", [](deserializer & d) { return mk_int_value(read_mpz(d)); });
|
|
||||||
static register_builtin_fn int_value_blt(name({"Int", "numeral"}), []() { return mk_int_value(mpz(0)); }, true);
|
|
||||||
|
|
||||||
bool is_int_value(expr const & e) {
|
|
||||||
return is_value(e) && dynamic_cast<int_value_value const *>(&to_value(e)) != nullptr;
|
|
||||||
}
|
|
||||||
|
|
||||||
mpz const & int_value_numeral(expr const & e) {
|
|
||||||
lean_assert(is_int_value(e));
|
|
||||||
return static_cast<int_value_value const &>(to_value(e)).get_num();
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Template for semantic attachments that are binary operators of
|
|
||||||
the form Int -> Int -> Int
|
|
||||||
*/
|
|
||||||
template<char const * Name, typename F>
|
|
||||||
class int_bin_op : public const_value {
|
|
||||||
public:
|
|
||||||
int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
|
|
||||||
return some_expr(mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
virtual void write(serializer & s) const { s << (std::string("int_") + Name); }
|
|
||||||
};
|
|
||||||
|
|
||||||
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_name, int_add_eval> 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(); });
|
|
||||||
|
|
||||||
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_name, int_mul_eval> 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(); });
|
|
||||||
|
|
||||||
constexpr char int_div_name[] = "div";
|
|
||||||
struct int_div_eval {
|
|
||||||
mpz operator()(mpz const & v1, mpz const & v2) {
|
|
||||||
if (v2.is_zero())
|
|
||||||
return v2;
|
|
||||||
else
|
|
||||||
return v1 / v2;
|
|
||||||
};
|
|
||||||
};
|
|
||||||
typedef int_bin_op<int_div_name, int_div_eval> 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(); });
|
|
||||||
|
|
||||||
class int_le_value : public const_value {
|
|
||||||
public:
|
|
||||||
int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
|
|
||||||
return some_expr(mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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(); });
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Semantic attachment for the Nat to Int coercion.
|
|
||||||
*/
|
|
||||||
class nat_to_int_value : public const_value {
|
|
||||||
public:
|
|
||||||
nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 2 && is_nat_value(args[1])) {
|
|
||||||
return some_expr(mk_int_value(nat_value_numeral(args[1])));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
virtual void write(serializer & s) const { s << "nat_to_int"; }
|
|
||||||
};
|
|
||||||
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(); });
|
|
||||||
|
|
||||||
void import_int(environment const & env, io_state const & ios) {
|
|
||||||
env->import("Int", ios);
|
|
||||||
}
|
|
||||||
|
|
||||||
static int mk_int_value(lua_State * L) {
|
|
||||||
return push_expr(L, mk_int_value(to_mpz_ext(L, 1)));
|
|
||||||
}
|
|
||||||
|
|
||||||
void open_int(lua_State * L) {
|
|
||||||
SET_GLOBAL_FUN(mk_int_value, "mk_int_value");
|
|
||||||
SET_GLOBAL_FUN(mk_int_value, "iVal");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,45 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#pragma once
|
|
||||||
#include "util/lua.h"
|
|
||||||
#include "util/numerics/mpz.h"
|
|
||||||
#include "kernel/expr.h"
|
|
||||||
#include "kernel/kernel.h"
|
|
||||||
#include "library/arith/Int_decls.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/** \brief Integer numbers type */
|
|
||||||
expr mk_int_type();
|
|
||||||
extern expr const Int;
|
|
||||||
|
|
||||||
/** \brief Return the value of type Integer that represents \c v. */
|
|
||||||
expr mk_int_value(mpz const & v);
|
|
||||||
inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); }
|
|
||||||
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);
|
|
||||||
|
|
||||||
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 mk_nat_to_int(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
|
|
||||||
|
|
||||||
class environment;
|
|
||||||
/**
|
|
||||||
\brief Import Integer number library in the given environment (if it has not been imported already).
|
|
||||||
It will also load the natural number library.
|
|
||||||
*/
|
|
||||||
void import_int(environment const & env, io_state const & ios);
|
|
||||||
|
|
||||||
void open_int(lua_State * L);
|
|
||||||
}
|
|
||||||
|
|
@ -1,129 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#include <string>
|
|
||||||
#include "kernel/abstract.h"
|
|
||||||
#include "kernel/environment.h"
|
|
||||||
#include "kernel/value.h"
|
|
||||||
#include "kernel/io_state.h"
|
|
||||||
#include "kernel/decl_macros.h"
|
|
||||||
#include "library/kernel_bindings.h"
|
|
||||||
#include "library/arith/nat.h"
|
|
||||||
#include "library/arith/Nat_decls.cpp"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
expr const Nat = mk_Nat();
|
|
||||||
expr mk_nat_type() { return mk_Nat(); }
|
|
||||||
|
|
||||||
class nat_value_value : public value {
|
|
||||||
mpz m_val;
|
|
||||||
protected:
|
|
||||||
virtual bool lt(value const & other) const {
|
|
||||||
return m_val < static_cast<nat_value_value const &>(other).m_val;
|
|
||||||
}
|
|
||||||
public:
|
|
||||||
nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); }
|
|
||||||
virtual ~nat_value_value() {}
|
|
||||||
virtual expr get_type() const { return Nat; }
|
|
||||||
virtual name get_name() const { return name{"Nat", "numeral"}; }
|
|
||||||
virtual bool operator==(value const & other) const {
|
|
||||||
nat_value_value const * _other = dynamic_cast<nat_value_value const*>(&other);
|
|
||||||
return _other && _other->m_val == m_val;
|
|
||||||
}
|
|
||||||
virtual void display(std::ostream & out) const { out << m_val; }
|
|
||||||
virtual format pp() const { return format(m_val); }
|
|
||||||
virtual format pp(bool, bool) const { return pp(); }
|
|
||||||
virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT
|
|
||||||
virtual unsigned hash() const { return m_val.hash(); }
|
|
||||||
virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
|
|
||||||
mpz const & get_num() const { return m_val; }
|
|
||||||
virtual void write(serializer & s) const { s << "nat" << m_val; }
|
|
||||||
};
|
|
||||||
expr mk_nat_value(mpz const & v) {
|
|
||||||
return mk_value(*(new nat_value_value(v)));
|
|
||||||
}
|
|
||||||
static value::register_deserializer_fn nat_value_ds("nat", [](deserializer & d) { return mk_nat_value(read_mpz(d)); });
|
|
||||||
static register_builtin_fn nat_value_blt(name({"Nat", "numeral"}), []() { return mk_nat_value(mpz(0)); }, true);
|
|
||||||
|
|
||||||
bool is_nat_value(expr const & e) {
|
|
||||||
return is_value(e) && dynamic_cast<nat_value_value const *>(&to_value(e)) != nullptr;
|
|
||||||
}
|
|
||||||
|
|
||||||
mpz const & nat_value_numeral(expr const & e) {
|
|
||||||
lean_assert(is_nat_value(e));
|
|
||||||
return static_cast<nat_value_value const &>(to_value(e)).get_num();
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Template for semantic attachments that are binary operators of
|
|
||||||
the form Nat -> Nat -> Nat
|
|
||||||
*/
|
|
||||||
template<char const * Name, typename F>
|
|
||||||
class nat_bin_op : public const_value {
|
|
||||||
public:
|
|
||||||
nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
|
|
||||||
return some_expr(mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
virtual void write(serializer & s) const { s << (std::string("nat_") + Name); }
|
|
||||||
};
|
|
||||||
|
|
||||||
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_name, nat_add_eval> 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(); });
|
|
||||||
|
|
||||||
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_name, nat_mul_eval> 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(); });
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Semantic attachment for less than or equal to operator with type
|
|
||||||
<code>Nat -> Nat -> Bool</code>
|
|
||||||
*/
|
|
||||||
class nat_le_value : public const_value {
|
|
||||||
public:
|
|
||||||
nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
|
|
||||||
return some_expr(mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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(); });
|
|
||||||
|
|
||||||
void import_nat(environment const & env, io_state const & ios) {
|
|
||||||
env->import("Nat", ios);
|
|
||||||
}
|
|
||||||
|
|
||||||
static int mk_nat_value(lua_State * L) {
|
|
||||||
mpz v = to_mpz_ext(L, 1);
|
|
||||||
if (v < 0)
|
|
||||||
throw exception("arg #1 must be non-negative");
|
|
||||||
return push_expr(L, mk_nat_value(v));
|
|
||||||
}
|
|
||||||
|
|
||||||
void open_nat(lua_State * L) {
|
|
||||||
SET_GLOBAL_FUN(mk_nat_value, "mk_nat_value");
|
|
||||||
SET_GLOBAL_FUN(mk_nat_value, "nVal");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,38 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#pragma once
|
|
||||||
#include "util/lua.h"
|
|
||||||
#include "kernel/expr.h"
|
|
||||||
#include "kernel/kernel.h"
|
|
||||||
#include "util/numerics/mpz.h"
|
|
||||||
#include "library/arith/Nat_decls.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/** \brief Natural numbers type */
|
|
||||||
expr mk_nat_type();
|
|
||||||
extern expr const Nat;
|
|
||||||
|
|
||||||
/** \brief Return the value of type Natural number that represents \c v. */
|
|
||||||
expr mk_nat_value(mpz const & v);
|
|
||||||
inline expr mk_nat_value(unsigned v) { return mk_nat_value(mpz(v)); }
|
|
||||||
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);
|
|
||||||
|
|
||||||
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). */
|
|
||||||
void import_nat(environment const & env, io_state const & ios);
|
|
||||||
|
|
||||||
void open_nat(lua_State * L);
|
|
||||||
}
|
|
||||||
|
|
@ -1,165 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#include <string>
|
|
||||||
#include "kernel/abstract.h"
|
|
||||||
#include "kernel/environment.h"
|
|
||||||
#include "kernel/value.h"
|
|
||||||
#include "kernel/io_state.h"
|
|
||||||
#include "kernel/decl_macros.h"
|
|
||||||
#include "library/kernel_bindings.h"
|
|
||||||
#include "library/arith/real.h"
|
|
||||||
#include "library/arith/int.h"
|
|
||||||
#include "library/arith/nat.h"
|
|
||||||
#include "library/arith/Real_decls.cpp"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
expr const Real = mk_Real();
|
|
||||||
expr mk_real_type() { return mk_Real(); }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Semantic attachment for "Real" values.
|
|
||||||
It is actually for rational values. We should eventually rename it to
|
|
||||||
rat_value_value
|
|
||||||
*/
|
|
||||||
class real_value_value : public value {
|
|
||||||
mpq m_val;
|
|
||||||
protected:
|
|
||||||
virtual bool lt(value const & other) const {
|
|
||||||
return m_val < static_cast<real_value_value const &>(other).m_val;
|
|
||||||
}
|
|
||||||
public:
|
|
||||||
real_value_value(mpq const & v):m_val(v) {}
|
|
||||||
virtual ~real_value_value() {}
|
|
||||||
virtual expr get_type() const { return Real; }
|
|
||||||
virtual name get_name() const { return name{"Real", "numeral"}; }
|
|
||||||
virtual bool operator==(value const & other) const {
|
|
||||||
real_value_value const * _other = dynamic_cast<real_value_value const*>(&other);
|
|
||||||
return _other && _other->m_val == m_val;
|
|
||||||
}
|
|
||||||
virtual void display(std::ostream & out) const { out << m_val; }
|
|
||||||
virtual format pp() const { return pp(false, false); }
|
|
||||||
virtual format pp(bool, bool coercion) const {
|
|
||||||
if (coercion)
|
|
||||||
return format{format(const_name(mk_nat_to_real_fn())), space(), format(m_val)};
|
|
||||||
else
|
|
||||||
return format(m_val);
|
|
||||||
}
|
|
||||||
virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion; }
|
|
||||||
virtual unsigned hash() const { return m_val.hash(); }
|
|
||||||
virtual int push_lua(lua_State * L) const { return push_mpq(L, m_val); }
|
|
||||||
mpq const & get_num() const { return m_val; }
|
|
||||||
virtual void write(serializer & s) const { s << "real" << m_val; }
|
|
||||||
};
|
|
||||||
|
|
||||||
expr mk_real_value(mpq const & v) { return mk_value(*(new real_value_value(v))); }
|
|
||||||
bool is_real_value(expr const & e) { return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr; }
|
|
||||||
mpq const & real_value_numeral(expr const & e) {
|
|
||||||
lean_assert(is_real_value(e));
|
|
||||||
return static_cast<real_value_value const &>(to_value(e)).get_num();
|
|
||||||
}
|
|
||||||
static value::register_deserializer_fn real_value_ds("real", [](deserializer & d) { return mk_real_value(read_mpq(d)); });
|
|
||||||
static register_builtin_fn real_value_blt(name({"Real", "numeral"}), []() { return mk_real_value(mpq(0)); }, true);
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Template for semantic attachments that are binary operators of
|
|
||||||
the form Real -> Real -> Real
|
|
||||||
*/
|
|
||||||
template<char const * Name, typename F>
|
|
||||||
class real_bin_op : public const_value {
|
|
||||||
public:
|
|
||||||
real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
|
|
||||||
return some_expr(mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
virtual void write(serializer & s) const { s << (std::string("real_") + Name); }
|
|
||||||
};
|
|
||||||
|
|
||||||
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_name, real_add_eval> 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(); });
|
|
||||||
|
|
||||||
|
|
||||||
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_name, real_mul_eval> 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(); });
|
|
||||||
|
|
||||||
constexpr char real_div_name[] = "div";
|
|
||||||
/** \brief Evaluator for / : Real -> Real -> Real */
|
|
||||||
struct real_div_eval {
|
|
||||||
mpq operator()(mpq const & v1, mpq const & v2) {
|
|
||||||
if (v2.is_zero())
|
|
||||||
return v2;
|
|
||||||
else
|
|
||||||
return v1 / v2;
|
|
||||||
};
|
|
||||||
};
|
|
||||||
typedef real_bin_op<real_div_name, real_div_eval> 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(); });
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Semantic attachment for less than or equal to operator with type
|
|
||||||
<code>Real -> Real -> Bool</code>
|
|
||||||
*/
|
|
||||||
class real_le_value : public const_value {
|
|
||||||
public:
|
|
||||||
real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
|
|
||||||
return some_expr(mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
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(); });
|
|
||||||
|
|
||||||
class int_to_real_value : public const_value {
|
|
||||||
public:
|
|
||||||
int_to_real_value():const_value("int_to_real", Int >> Real) {}
|
|
||||||
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
|
|
||||||
if (num_args == 2 && is_int_value(args[1])) {
|
|
||||||
return some_expr(mk_real_value(mpq(int_value_numeral(args[1]))));
|
|
||||||
} else {
|
|
||||||
return none_expr();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
virtual void write(serializer & s) const { s << "int_to_real"; }
|
|
||||||
};
|
|
||||||
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(); });
|
|
||||||
|
|
||||||
void import_real(environment const & env, io_state const & ios) {
|
|
||||||
env->import("Real", ios);
|
|
||||||
}
|
|
||||||
|
|
||||||
static int mk_real_value(lua_State * L) {
|
|
||||||
return push_expr(L, mk_real_value(to_mpq_ext(L, 1)));
|
|
||||||
}
|
|
||||||
|
|
||||||
void open_real(lua_State * L) {
|
|
||||||
SET_GLOBAL_FUN(mk_real_value, "mk_real_value");
|
|
||||||
SET_GLOBAL_FUN(mk_real_value, "rVal");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,47 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#pragma once
|
|
||||||
#include "util/lua.h"
|
|
||||||
#include "util/numerics/mpq.h"
|
|
||||||
#include "kernel/expr.h"
|
|
||||||
#include "kernel/kernel.h"
|
|
||||||
#include "library/arith/Real_decls.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
/** \brief Real numbers type */
|
|
||||||
expr mk_real_type();
|
|
||||||
extern expr const Real;
|
|
||||||
|
|
||||||
/** \brief Return the value of type Real that represents \c v. */
|
|
||||||
expr mk_real_value(mpq const & v);
|
|
||||||
inline expr mk_real_value(int v) { return mk_real_value(mpq(v)); }
|
|
||||||
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);
|
|
||||||
|
|
||||||
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). */
|
|
||||||
void import_real(environment const & env, io_state const & ios);
|
|
||||||
|
|
||||||
/** \brief Coercion from int to real */
|
|
||||||
expr mk_int_to_real_fn();
|
|
||||||
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);
|
|
||||||
|
|
||||||
void open_real(lua_State * L);
|
|
||||||
}
|
|
||||||
|
|
@ -1,22 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#pragma once
|
|
||||||
#include "util/script_state.h"
|
|
||||||
#include "library/arith/nat.h"
|
|
||||||
#include "library/arith/int.h"
|
|
||||||
#include "library/arith/real.h"
|
|
||||||
|
|
||||||
namespace lean {
|
|
||||||
inline void open_arith_module(lua_State * L) {
|
|
||||||
open_nat(L);
|
|
||||||
open_int(L);
|
|
||||||
open_real(L);
|
|
||||||
}
|
|
||||||
inline void register_arith_module() {
|
|
||||||
script_state::register_module(open_arith_module);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,118 +0,0 @@
|
||||||
/*
|
|
||||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
|
||||||
*/
|
|
||||||
#include "util/thread.h"
|
|
||||||
#include "util/test.h"
|
|
||||||
#include "kernel/kernel.h"
|
|
||||||
#include "kernel/normalizer.h"
|
|
||||||
#include "kernel/type_checker.h"
|
|
||||||
#include "kernel/abstract.h"
|
|
||||||
#include "library/io_state_stream.h"
|
|
||||||
#include "library/arith/arith.h"
|
|
||||||
#include "frontends/lean/frontend.h"
|
|
||||||
#include "frontends/lua/register_modules.h"
|
|
||||||
using namespace lean;
|
|
||||||
|
|
||||||
static void tst0() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
normalizer norm(env);
|
|
||||||
env->add_var("n", Nat);
|
|
||||||
expr n = Const("n");
|
|
||||||
lean_assert_eq(mk_nat_type(), Nat);
|
|
||||||
env->add_var("x", Real);
|
|
||||||
expr x = Const("x");
|
|
||||||
lean_assert_eq(mk_real_type(), Real);
|
|
||||||
env->add_var("i", Int);
|
|
||||||
expr i = Const("i");
|
|
||||||
lean_assert_eq(mk_int_type(), Int);
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst1() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
expr e = mk_int_value(mpz(10));
|
|
||||||
lean_assert(is_int_value(e));
|
|
||||||
lean_assert(type_check(e, env) == Int);
|
|
||||||
std::cout << "e: " << e << "\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst2() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
expr e = mk_Int_add(iVal(10), iVal(30));
|
|
||||||
std::cout << e << "\n";
|
|
||||||
std::cout << normalize(e, 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));
|
|
||||||
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));
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst3() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
expr e = mk_Int_mul(iVal(10), iVal(30));
|
|
||||||
std::cout << e << "\n";
|
|
||||||
std::cout << normalize(e, 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));
|
|
||||||
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));
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst4() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
expr e = mk_Int_sub(iVal(10), iVal(30));
|
|
||||||
std::cout << e << "\n";
|
|
||||||
std::cout << normalize(e, 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));
|
|
||||||
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));
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst5() {
|
|
||||||
environment env;
|
|
||||||
init_test_frontend(env);
|
|
||||||
env->add_var(name("a"), Int);
|
|
||||||
expr e = mk_eq(Int, iVal(3), iVal(4));
|
|
||||||
std::cout << e << " --> " << normalize(e, env) << "\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
static void tst6() {
|
|
||||||
std::cout << "tst6\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"; });
|
|
||||||
t1.join();
|
|
||||||
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";
|
|
||||||
}
|
|
||||||
|
|
||||||
int main() {
|
|
||||||
save_stack_info();
|
|
||||||
register_modules();
|
|
||||||
tst0();
|
|
||||||
tst1();
|
|
||||||
tst2();
|
|
||||||
tst3();
|
|
||||||
tst4();
|
|
||||||
tst5();
|
|
||||||
tst6();
|
|
||||||
return has_violations() ? 1 : 0;
|
|
||||||
}
|
|
||||||
Loading…
Reference in a new issue