michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Refactor arith libraries

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-06 23:17:24 -07:00
parent b92bbeb83b
commit 7a9d53d0d7
30 changed files with 873 additions and 682 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/CMakeLists.txt
View file

@ -82,8 +82,9 @@ include_directories(${LEAN_SOURCE_DIR}/util/numerics)
include_directories(${LEAN_SOURCE_DIR}/util/sexpr)
include_directories(${LEAN_SOURCE_DIR}/interval)
include_directories(${LEAN_SOURCE_DIR}/kernel)
include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
include_directories(${LEAN_SOURCE_DIR}/library)
include_directories(${LEAN_SOURCE_DIR}/library/arith)
include_directories(${LEAN_SOURCE_DIR}/library/import_all)
include_directories(${LEAN_SOURCE_DIR}/parsers)
include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
@ -97,10 +98,12 @@ add_subdirectory(interval)
set(LEAN_LIBS ${LEAN_LIBS} interval)
add_subdirectory(kernel)
set(LEAN_LIBS ${LEAN_LIBS} kernel)
add_subdirectory(kernel/arith)
set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
add_subdirectory(library)
set(LEAN_LIBS ${LEAN_LIBS} library)
add_subdirectory(library/arith)
set(LEAN_LIBS ${LEAN_LIBS} arithlib)
add_subdirectory(library/import_all)
set(LEAN_LIBS ${LEAN_LIBS} import_all)
add_subdirectory(frontends/lean)
set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")

4
src/frontends/lean/lean_frontend.cpp
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#include <atomic>
#include <unordered_set>
#include "environment.h"
#include "toplevel.h"
#include "import_all.h"
#include "map.h"
#include "state.h"
#include "sstream.h"
@ -362,7 +362,7 @@ struct frontend::imp {
};
frontend::frontend():m_imp(new imp(*this)) {
init_toplevel(m_imp->m_env);
import_all(m_imp->m_env);
init_builtin_notation(*this);
m_imp->m_state.set_formatter(mk_pp_formatter(*this));
}

2
src/frontends/lean/lean_notation.cpp
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#include "builtin.h"
#include "basic_thms.h"
#include "lean_frontend.h"
#include "arith.h"
#include "arithlibs.h"
namespace lean {
/**

2
src/frontends/lean/lean_parser.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "type_checker.h"
#include "free_vars.h"
#include "builtin.h"
#include "arith.h"
#include "arithlibs.h"
#include "printer.h"
#include "state.h"
#include "option_declarations.h"

2
src/kernel/arith/CMakeLists.txt
View file

@ -1,2 +0,0 @@
add_library(kernel_arith arith.cpp)
target_link_libraries(kernel_arith ${LEAN_LIBS})

437
src/kernel/arith/arith.cpp
View file

@ -1,437 +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 "builtin.h"
#include "arith.h"
#include "abstract.h"
#include "value.h"
#include "environment.h"
namespace lean {
class num_type_value : public type_value {
name m_unicode;
public:
num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
virtual ~num_type_value() {}
virtual name get_unicode_name() const { return m_unicode; }
};
// =======================================
// Natural numbers
class nat_type_value : public num_type_value {
public:
nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
};
expr const Nat = mk_value(*(new nat_type_value()));
expr mk_nat_type() { return Nat; }
class nat_value_value : public value {
mpz 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 unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpz const & get_num() const { return m_val; }
};
expr mk_nat_value(mpz const & v) {
return mk_value(*(new nat_value_value(v)));
}
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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
constexpr char nat_add_name[] = "add";
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);
constexpr char nat_mul_name[] = "mul";
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);
class nat_le_value : public const_value {
public:
nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(nat_le_fn, nat_le_value);
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_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
// =======================================
// =======================================
// Integers
class int_type_value : public num_type_value {
public:
int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
};
expr const Int = mk_value(*(new int_type_value()));
expr mk_int_type() { return Int; }
class int_value_value : public value {
mpz 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 format(m_val); }
virtual format pp(bool unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpz const & get_num() const { return m_val; }
};
expr mk_int_value(mpz const & v) {
return mk_value(*(new int_value_value(v)));
}
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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
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);
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);
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);
class int_le_value : public const_value {
public:
int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(int_le_fn, int_le_value);
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"}));
// =======================================
// =======================================
// Reals
class real_type_value : public num_type_value {
public:
real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
};
expr const Real = mk_value(*(new real_type_value()));
expr mk_real_type() { return Real; }
class real_value_value : public value {
mpq 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 format(m_val); }
virtual format pp(bool unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpq const & get_num() const { return 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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
constexpr char real_add_name[] = "add";
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);
constexpr char real_mul_name[] = "mul";
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);
constexpr char real_div_name[] = "div";
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);
class real_le_value : public const_value {
public:
real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(real_le_fn, real_le_value);
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(exp_fn, name("exp"));
MK_CONSTANT(log_fn, name("log"));
MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
MK_CONSTANT(sin_fn, name("sin"));
MK_CONSTANT(cos_fn, name("cos"));
MK_CONSTANT(tan_fn, name("tan"));
MK_CONSTANT(cot_fn, name("cot"));
MK_CONSTANT(sec_fn, name("sec"));
MK_CONSTANT(csc_fn, name("csc"));
MK_CONSTANT(sinh_fn, name("sinh"));
MK_CONSTANT(cosh_fn, name("cosh"));
MK_CONSTANT(tanh_fn, name("tanh"));
MK_CONSTANT(coth_fn, name("coth"));
MK_CONSTANT(sech_fn, name("sech"));
MK_CONSTANT(csch_fn, name("csch"));
// =======================================
// =======================================
// Coercions
class nat_to_int_value : public const_value {
public:
nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 2 && is_nat_value(args[1])) {
r = mk_int_value(nat_value_numeral(args[1]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
class int_to_real_value : public const_value {
public:
int_to_real_value():const_value("int_to_real", Int >> Real) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 2 && is_int_value(args[1])) {
r = mk_real_value(mpq(int_value_numeral(args[1])));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(int_to_real_fn, int_to_real_value);
MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
// =======================================
void add_arith_theory(environment & env) {
expr nn_b = Nat >> (Nat >> Bool);
expr ii_b = Int >> (Int >> Bool);
expr ii_i = Int >> (Int >> Int);
expr rr_b = Real >> (Real >> Bool);
expr rr_r = Real >> (Real >> Real);
expr i_i = Int >> Int;
expr r_r = Real >> Real;
expr x = Const("x");
expr y = Const("y");
env.add_builtin(Nat);
env.add_builtin_set(nVal(0));
env.add_builtin(mk_nat_add_fn());
env.add_builtin(mk_nat_mul_fn());
env.add_builtin(mk_nat_le_fn());
env.add_builtin(Int);
env.add_builtin_set(iVal(0));
env.add_builtin(mk_int_add_fn());
env.add_builtin(mk_int_mul_fn());
env.add_builtin(mk_int_div_fn());
env.add_builtin(mk_int_le_fn());
env.add_builtin(Real);
env.add_builtin_set(rVal(0));
env.add_builtin(mk_real_add_fn());
env.add_builtin(mk_real_mul_fn());
env.add_builtin(mk_real_div_fn());
env.add_builtin(mk_real_le_fn());
env.add_builtin(mk_nat_to_int_fn());
env.add_builtin(mk_int_to_real_fn());
env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
env.add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
env.add_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
env.add_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
env.add_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x)));
env.add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
env.add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x)));
env.add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
env.add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
env.add_var(exp_fn_name, r_r);
env.add_var(log_fn_name, r_r);
env.add_var(real_pi_name, Real);
env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
env.add_var(sin_fn_name, r_r);
env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
}
}

216
src/kernel/arith/arith.h
View file

@ -1,216 +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 "expr.h"
#include "builtin.h"
#include "mpz.h"
#include "mpq.h"
namespace lean {
// =======================================
// Natural numbers
expr mk_nat_type();
extern expr const Nat;
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);
/** \brief 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 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 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); }
/** \brief 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 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 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 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 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); }
expr mk_nat_id_fn();
inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); }
inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); }
// =======================================
// =======================================
// Integers
expr mk_int_type();
extern expr const Int;
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 iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); }
expr mk_int_sub_fn();
inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
expr mk_int_neg_fn();
inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); }
expr mk_int_mul_fn();
inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
expr mk_int_div_fn();
inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
expr mk_int_mod_fn();
inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); }
expr mk_int_divides_fn();
inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_fn(), e1, e2); }
expr mk_int_abs_fn();
inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); }
expr mk_int_le_fn();
inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
expr mk_int_ge_fn();
inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); }
expr mk_int_lt_fn();
inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); }
expr mk_int_gt_fn();
inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
// =======================================
// =======================================
// Reals
expr mk_real_type();
extern expr const Real;
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 rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); }
expr mk_real_sub_fn();
inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); }
expr mk_real_neg_fn();
inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); }
expr mk_real_mul_fn();
inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
expr mk_real_div_fn();
inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); }
expr mk_real_abs_fn();
inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); }
expr mk_real_le_fn();
inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); }
expr mk_real_ge_fn();
inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); }
expr mk_real_lt_fn();
inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); }
expr mk_real_gt_fn();
inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); }
inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
expr mk_exp_fn();
inline expr Exp(expr const & e) { return mk_app(mk_exp_fn(), e); }
expr mk_log_fn();
inline expr Log(expr const & e) { return mk_app(mk_log_fn(), e); }
// =======================================
// =======================================
// Transcendental and Hyperbolic
expr mk_real_pi();
expr mk_sin_fn();
inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
expr mk_cos_fn();
inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
expr mk_tan_fn();
inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
expr mk_cot_fn();
inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
expr mk_sec_fn();
inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
expr mk_csc_fn();
inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
expr mk_sinh_fn();
inline expr Sinh(expr const & e) { return mk_app(mk_sinh_fn(), e); }
expr mk_cosh_fn();
inline expr Cosh(expr const & e) { return mk_app(mk_cosh_fn(), e); }
expr mk_tanh_fn();
inline expr Tanh(expr const & e) { return mk_app(mk_tanh_fn(), e); }
expr mk_coth_fn();
inline expr Coth(expr const & e) { return mk_app(mk_coth_fn(), e); }
expr mk_sech_fn();
inline expr Sech(expr const & e) { return mk_app(mk_sech_fn(), e); }
expr mk_csch_fn();
inline expr Csch(expr const & e) { return mk_app(mk_csch_fn(), e); }
// =======================================
// =======================================
// Coercions
expr mk_nat_to_int_fn();
inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
expr mk_int_to_real_fn();
inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
expr mk_nat_to_real_fn();
inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); }
// =======================================
class environment;
void add_arith_theory(environment & env);
}

2
src/library/CMakeLists.txt
View file

@ -1,4 +1,4 @@
add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
printer.cpp formatter.cpp context_to_lambda.cpp
state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp)
target_link_libraries(library ${LEAN_LIBS})

2
src/library/arith/CMakeLists.txt Normal file
View file

@ -0,0 +1,2 @@
add_library(arithlib natlib.cpp intlib.cpp reallib.cpp specialfnlib.cpp arithlibs.cpp)
target_link_libraries(arithlib ${LEAN_LIBS})

17
src/library/arith/arithlibs.cpp Normal file
View file

@ -0,0 +1,17 @@
/*
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 "arithlibs.h"
namespace lean {
void import_arithlibs(environment & env) {
import_natlib(env);
import_intlib(env);
import_reallib(env);
import_int_to_real_coercions(env);
import_specialfnlib(env);
}
}

19
src/library/arith/arithlibs.h Normal file
View file

@ -0,0 +1,19 @@
/*
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 "natlib.h"
#include "intlib.h"
#include "reallib.h"
#include "specialfnlib.h"
namespace lean {
class environment;
/**
\brief Import all arithmetic related builtin libraries.
*/
void import_arithlibs(environment & env);
}

158
src/library/arith/intlib.cpp Normal file
View file

@ -0,0 +1,158 @@
/*
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 "intlib.h"
#include "natlib.h"
#include "numtype.h"
#include "abstract.h"
#include "environment.h"
namespace lean {
class int_type_value : public num_type_value {
public:
int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
};
expr const Int = mk_value(*(new int_type_value()));
expr mk_int_type() { return Int; }
class int_value_value : public value {
mpz 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 format(m_val); }
virtual format pp(bool unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpz const & get_num() const { return m_val; }
};
expr mk_int_value(mpz const & v) {
return mk_value(*(new int_value_value(v)));
}
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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
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);
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);
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);
class int_le_value : public const_value {
public:
int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(int_le_fn, int_le_value);
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"}));
class nat_to_int_value : public const_value {
public:
nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 2 && is_nat_value(args[1])) {
r = mk_int_value(nat_value_numeral(args[1]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
void import_intlib(environment & env) {
if (env.find_object(to_value(Int).get_name()))
return;
import_natlib(env);
expr i_i = Int >> Int;
expr ii_b = Int >> (Int >> Bool);
expr ii_i = Int >> (Int >> Int);
expr x = Const("x");
expr y = Const("y");
env.add_builtin(Int);
env.add_builtin_set(iVal(0));
env.add_builtin(mk_int_add_fn());
env.add_builtin(mk_int_mul_fn());
env.add_builtin(mk_int_div_fn());
env.add_builtin(mk_int_le_fn());
env.add_builtin(mk_nat_to_int_fn());
env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
env.add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
env.add_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
env.add_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
env.add_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
}
}

93
src/library/arith/intlib.h Normal file
View file

@ -0,0 +1,93 @@
/*
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 "expr.h"
#include "builtin.h"
#include "mpz.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);
/** \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_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); }
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_intlib(environment & env);
}

112
src/library/arith/natlib.cpp Normal file
View file

@ -0,0 +1,112 @@
/*
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 "natlib.h"
#include "numtype.h"
#include "abstract.h"
#include "environment.h"
namespace lean {
class nat_type_value : public num_type_value {
public:
nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
};
expr const Nat = mk_value(*(new nat_type_value()));
expr mk_nat_type() { return Nat; }
class nat_value_value : public value {
mpz 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 unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpz const & get_num() const { return m_val; }
};
expr mk_nat_value(mpz const & v) {
return mk_value(*(new nat_value_value(v)));
}
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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
constexpr char nat_add_name[] = "add";
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);
constexpr char nat_mul_name[] = "mul";
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);
class nat_le_value : public const_value {
public:
nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(nat_le_fn, nat_le_value);
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"}));
void import_natlib(environment & env) {
if (env.find_object(to_value(Nat).get_name()))
return;
expr nn_b = Nat >> (Nat >> Bool);
expr x = Const("x");
expr y = Const("y");
env.add_builtin(Nat);
env.add_builtin_set(nVal(0));
env.add_builtin(mk_nat_add_fn());
env.add_builtin(mk_nat_mul_fn());
env.add_builtin(mk_nat_le_fn());
env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
}
}

58
src/library/arith/natlib.h Normal file
View file

@ -0,0 +1,58 @@
/*
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 "expr.h"
#include "builtin.h"
#include "mpz.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);
/** \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); }
class environment;
/** \brief Import Natural number library in the given environment (if it has not been imported already). */
void import_natlib(environment & env);
}

20
src/library/arith/numtype.h Normal file
View file

@ -0,0 +1,20 @@
/*
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 "expr.h"
#include "value.h"
namespace lean {
/** \brief Base class for numeric types */
class num_type_value : public type_value {
name m_unicode;
public:
num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
virtual ~num_type_value() {}
virtual name get_unicode_name() const { return m_unicode; }
};
}

159
src/library/arith/reallib.cpp Normal file
View file

@ -0,0 +1,159 @@
/*
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 "reallib.h"
#include "intlib.h"
#include "natlib.h"
#include "numtype.h"
#include "abstract.h"
#include "environment.h"
namespace lean {
class real_type_value : public num_type_value {
public:
real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
};
expr const Real = mk_value(*(new real_type_value()));
expr mk_real_type() { return Real; }
class real_value_value : public value {
mpq 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 format(m_val); }
virtual format pp(bool unicode) const { return pp(); }
virtual unsigned hash() const { return m_val.hash(); }
mpq const & get_num() const { return 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();
}
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 bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
return true;
} else {
return false;
}
}
};
constexpr char real_add_name[] = "add";
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);
constexpr char real_mul_name[] = "mul";
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);
constexpr char real_div_name[] = "div";
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);
class real_le_value : public const_value {
public:
real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(real_le_fn, real_le_value);
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"}));
void import_reallib(environment & env) {
if (env.find_object(to_value(Real).get_name()))
return;
expr rr_b = Real >> (Real >> Bool);
expr rr_r = Real >> (Real >> Real);
expr r_r = Real >> Real;
expr x = Const("x");
expr y = Const("y");
env.add_builtin(Real);
env.add_builtin_set(rVal(0));
env.add_builtin(mk_real_add_fn());
env.add_builtin(mk_real_mul_fn());
env.add_builtin(mk_real_div_fn());
env.add_builtin(mk_real_le_fn());
env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x)));
env.add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
env.add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x)));
env.add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
env.add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
}
class int_to_real_value : public const_value {
public:
int_to_real_value():const_value("int_to_real", Int >> Real) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 2 && is_int_value(args[1])) {
r = mk_real_value(mpq(int_value_numeral(args[1])));
return true;
} else {
return false;
}
}
};
MK_BUILTIN(int_to_real_fn, int_to_real_value);
MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
void import_int_to_real_coercions(environment & env) {
if (env.find_object(to_value(mk_int_to_real_fn()).get_name()))
return;
import_intlib(env);
import_reallib(env);
env.add_builtin(mk_int_to_real_fn());
expr x = Const("x");
env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
}
}

80
src/library/arith/reallib.h Normal file
View file

@ -0,0 +1,80 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
#include "builtin.h"
#include "mpq.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);
/** \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); }
class environment;
/** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */
void import_reallib(environment & env);
/** \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); }
/** \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 & env);
}

60
src/library/arith/specialfnlib.cpp Normal file
View file

@ -0,0 +1,60 @@
/*
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 "specialfnlib.h"
#include "reallib.h"
#include "abstract.h"
#include "environment.h"
namespace lean {
MK_CONSTANT(exp_fn, name("exp"));
MK_CONSTANT(log_fn, name("log"));
MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
MK_CONSTANT(sin_fn, name("sin"));
MK_CONSTANT(cos_fn, name("cos"));
MK_CONSTANT(tan_fn, name("tan"));
MK_CONSTANT(cot_fn, name("cot"));
MK_CONSTANT(sec_fn, name("sec"));
MK_CONSTANT(csc_fn, name("csc"));
MK_CONSTANT(sinh_fn, name("sinh"));
MK_CONSTANT(cosh_fn, name("cosh"));
MK_CONSTANT(tanh_fn, name("tanh"));
MK_CONSTANT(coth_fn, name("coth"));
MK_CONSTANT(sech_fn, name("sech"));
MK_CONSTANT(csch_fn, name("csch"));
void import_specialfnlib(environment & env) {
if (env.find_object(const_name(mk_exp_fn())))
return;
import_reallib(env);
expr r_r = Real >> Real;
expr x = Const("x");
env.add_var(exp_fn_name, r_r);
env.add_var(log_fn_name, r_r);
env.add_var(real_pi_name, Real);
env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
env.add_var(sin_fn_name, r_r);
env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
}
}

63
src/library/arith/specialfnlib.h Normal file
View file

@ -0,0 +1,63 @@
/*
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 "expr.h"
namespace lean {
// Special functions library
expr mk_exp_fn();
inline expr Exp(expr const & e) { return mk_app(mk_exp_fn(), e); }
expr mk_log_fn();
inline expr Log(expr const & e) { return mk_app(mk_log_fn(), e); }
expr mk_real_pi();
expr mk_sin_fn();
inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
expr mk_cos_fn();
inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
expr mk_tan_fn();
inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
expr mk_cot_fn();
inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
expr mk_sec_fn();
inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
expr mk_csc_fn();
inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
expr mk_sinh_fn();
inline expr Sinh(expr const & e) { return mk_app(mk_sinh_fn(), e); }
expr mk_cosh_fn();
inline expr Cosh(expr const & e) { return mk_app(mk_cosh_fn(), e); }
expr mk_tanh_fn();
inline expr Tanh(expr const & e) { return mk_app(mk_tanh_fn(), e); }
expr mk_coth_fn();
inline expr Coth(expr const & e) { return mk_app(mk_coth_fn(), e); }
expr mk_sech_fn();
inline expr Sech(expr const & e) { return mk_app(mk_sech_fn(), e); }
expr mk_csch_fn();
inline expr Csch(expr const & e) { return mk_app(mk_csch_fn(), e); }
class environment;
/**
\brief Import the special function library (if it has not been imported already).
The (basic) Real Number library is also imported.
*/
void import_specialfnlib(environment & env);
}

2
src/library/import_all/CMakeLists.txt Normal file
View file

@ -0,0 +1,2 @@
add_library(import_all import_all.cpp)
target_link_libraries(import_all ${LEAN_LIBS})

10
src/library/toplevel.cpp → src/library/import_all/import_all.cpp
View file

@ -4,20 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "toplevel.h"
#include "import_all.h"
#include "builtin.h"
#include "basic_thms.h"
#include "arith.h"
#include "arithlibs.h"
namespace lean {
void init_toplevel(environment & env) {
void import_all(environment & env) {
add_basic_theory(env);
add_basic_thms(env);
add_arith_theory(env);
import_arithlibs(env);
}
environment mk_toplevel() {
environment r;
init_toplevel(r);
import_all(r);
return r;
}
}

6
src/library/toplevel.h → src/library/import_all/import_all.h
View file

@ -8,8 +8,8 @@ Author: Leonardo de Moura
#include "environment.h"
namespace lean {
/** \brief Initialize environment with builtin objects and basic theorems. */
void init_toplevel(environment & env);
/** \brief Create top-level environment with builtin objects and basic theorems. */
/** \brief Import all builtin libraries and theorems */
void import_all(environment & env);
/** \brief Create top-level environment with all builtin libraries and theorems */
environment mk_toplevel();
}

2
src/tests/frontends/lean/implicit_args.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "printer.h"
#include "occurs.h"
#include "abstract.h"
#include "toplevel.h"
#include "import_all.h"
#include "basic_thms.h"
#include "type_checker.h"
#include "kernel_exception.h"

4
src/tests/kernel/arith.cpp
View file

@ -8,9 +8,9 @@ Author: Leonardo de Moura
#include "environment.h"
#include "type_checker.h"
#include "builtin.h"
#include "arith.h"
#include "arithlibs.h"
#include "normalizer.h"
#include "toplevel.h"
#include "import_all.h"
#include "abstract.h"
#include "printer.h"
#include "test.h"

4
src/tests/kernel/environment.cpp
View file

@ -8,9 +8,9 @@ Author: Leonardo de Moura
#include "environment.h"
#include "type_checker.h"
#include "printer.h"
#include "toplevel.h"
#include "import_all.h"
#include "builtin.h"
#include "arith.h"
#include "arithlibs.h"
#include "normalizer.h"
#include "abstract.h"
#include "exception.h"

2
src/tests/kernel/expr.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "instantiate.h"
#include "printer.h"
#include "deep_copy.h"
#include "arith.h"
#include "arithlibs.h"
using namespace lean;
void tst1() {

2
src/tests/kernel/normalizer.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "expr_sets.h"
#include "abstract.h"
#include "kernel_exception.h"
#include "toplevel.h"
#include "import_all.h"
#include "printer.h"
using namespace lean;

4
src/tests/kernel/threads.cpp
View file

@ -13,8 +13,8 @@ Author: Leonardo de Moura
#include "deep_copy.h"
#include "abstract.h"
#include "normalizer.h"
#include "toplevel.h"
#include "arith.h"
#include "import_all.h"
#include "arithlibs.h"
#include "test.h"
using namespace lean;

4
src/tests/kernel/type_checker.cpp
View file

@ -11,10 +11,10 @@ Author: Leonardo de Moura
#include "environment.h"
#include "abstract.h"
#include "exception.h"
#include "toplevel.h"
#include "import_all.h"
#include "basic_thms.h"
#include "builtin.h"
#include "arith.h"
#include "arithlibs.h"
#include "normalizer.h"
#include "printer.h"
#include "trace.h"