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

refactor(library/arith): move int and nat declarations to .lean files.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-30 03:29:20 -08:00
parent 097b10e424
commit c3bc6afb12
19 changed files with 198 additions and 118 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
examples/lean/ex4.lean
View file

@ -1,6 +1,7 @@
Import tactic
Definition a : Nat := 10
(* Trivial indicates a "proof by evaluation" *)
Theorem T1 : a > 0 := Trivial
Theorem T2 : a - 5 > 3 := Trivial
Theorem T1 : a > 0 := (by trivial)
Theorem T2 : a - 5 > 3 := (by trivial)
(* The next one is commented because it fails *)
(* Theorem T3 : a > 11 := Trivial *)

16
src/builtin/CMakeLists.txt
View file

@ -31,8 +31,8 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME}
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
add_custom_target(${FNAME}_builtin DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${FNAME}_builtin)
add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${BASENAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
endfunction()
@ -45,8 +45,8 @@ function(copy_olean FILE)
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME} ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME})
add_custom_target(${FNAME}_builtin DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${FNAME}_builtin)
add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
add_dependencies(builtin ${BASENAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
endfunction()
@ -67,4 +67,12 @@ function(add_theory FILE)
endfunction()
add_kernel_theory("basic.lean")
add_kernel_theory("nat.lean")
add_dependencies(nat_builtin basic_builtin)
add_kernel_theory("int.lean")
add_dependencies(int_builtin nat_builtin)
add_dependencies(int_builtin basic_builtin)
add_theory("cast.lean")
# TODO(Leo): Remove the following dependencies after cleanup
add_dependencies(cast_builtin nat_builtin)
add_dependencies(cast_builtin int_builtin)

BIN
src/builtin/cast.olean
View file

Binary file not shown.

65
src/builtin/int.lean Normal file
View file

@ -0,0 +1,65 @@
Import basic.
Import nat.
Variable Int : Type.
Alias ℤ : Int.
Builtin Int::numeral.
Builtin Int::add : Int -> Int -> Int.
Infixl 65 + : Int::add.
Builtin Int::mul : Int -> Int -> Int.
Infixl 70 * : Int::mul.
Builtin Int::div : Int -> Int -> Int.
Infixl 70 div : Int::div.
Builtin Int::le : Int -> Int -> Bool.
Infix 50 <= : Int::le.
Infix 50 ≤ : Int::le.
Definition Int::ge (a b : Int) : Bool := b ≤ a.
Infix 50 >= : Int::ge.
Infix 50 ≥ : Int::ge.
Definition Int::lt (a b : Int) : Bool := ¬ (a ≥ b).
Infix 50 < : Int::lt.
Definition Int::gt (a b : Int) : Bool := ¬ (a ≤ b).
Infix 50 > : Int::gt.
Definition Int::sub (a b : Int) : Int := a + -1 * b.
Infixl 65 - : Int::sub.
Definition Int::neg (a : Int) : Int := -1 * a.
Notation 75 - _ : Int::neg.
Definition Int::mod (a b : Int) : Int := a - b * (a div b).
Infixl 70 mod : Int::mod.
Builtin nat_to_int : Nat -> Int.
Coercion nat_to_int.
Definition Int::divides (a b : Int) : Bool := (b mod a) = 0.
Infix 50 | : Int::divides.
Definition Int::abs (a : Int) : Int := if (0 ≤ a) a (- a).
Notation 55 | _ | : Int::abs.
Definition Nat::sub (a b : Nat) : Int := nat_to_int a - nat_to_int b.
Infixl 65 - : Nat::sub.
Definition Nat::neg (a : Nat) : Int := - (nat_to_int a).
Notation 75 - _ : Nat::neg.
SetOpaque Int::sub true.
SetOpaque Int::neg true.
SetOpaque Int::mod true.
SetOpaque Int::divides true.
SetOpaque Int::abs true.
SetOpaque Int::ge true.
SetOpaque Int::lt true.
SetOpaque Int::gt true.
SetOpaque Nat::sub true.
SetOpaque Nat::neg true.

BIN
src/builtin/int.olean Normal file
View file

Binary file not shown.

34
src/builtin/nat.lean Normal file
View file

@ -0,0 +1,34 @@
Import basic.
Variable Nat : Type.
Alias ℕ : Nat.
Builtin Nat::numeral.
Builtin Nat::add : Nat -> Nat -> Nat.
Infixl 65 + : Nat::add.
Builtin Nat::mul : Nat -> Nat -> Nat.
Infixl 70 * : Nat::mul.
Builtin Nat::le : Nat -> Nat -> Bool.
Infix 50 <= : Nat::le.
Infix 50 ≤ : Nat::le.
Definition Nat::ge (a b : Nat) := b ≤ a.
Infix 50 >= : Nat::ge.
Infix 50 ≥ : Nat::ge.
Definition Nat::lt (a b : Nat) := ¬ (a ≥ b).
Infix 50 < : Nat::lt.
Definition Nat::gt (a b : Nat) := ¬ (a ≤ b).
Infix 50 > : Nat::gt.
Definition Nat::id (a : Nat) := a.
Notation 55 | _ | : Nat::id.
SetOpaque Nat::ge true.
SetOpaque Nat::lt true.
SetOpaque Nat::gt true.
SetOpaque Nat::id true.

BIN
src/builtin/nat.olean Normal file
View file

Binary file not shown.

18
src/frontends/lean/frontend.cpp
View file

@ -597,14 +597,24 @@ void add_mixfixo(environment const & env, io_state const & ios, unsigned sz, nam
}
operator_info find_op_for(ro_environment const & env, expr const & n, bool unicode) {
operator_info r = to_ext(env).find_op_for(n, unicode);
if (r || !is_constant(n)) {
if (r) {
return r;
} else {
} else if (is_constant(n)) {
optional<object> obj = env->find_object(const_name(n));
if (obj && obj->is_builtin() && obj->get_name() == const_name(n))
if (obj && obj->is_builtin() && obj->get_name() == const_name(n)) {
// n is a constant that is referencing a builtin object.
// If the notation is associated with the builtin object, we should try it.
// TODO(Leo): Remark: in the new approach using .Lean files, the table is populated with constants.
// So, this branch is not really needed anymore.
return to_ext(env).find_op_for(obj->get_value(), unicode);
else
} else {
return r;
}
} else if (is_value(n)) {
// Check whether the notation was declared for a constant referencing this builtin object.
return to_ext(env).find_op_for(mk_constant(to_value(n).get_name()), unicode);
} else {
return r;
}
}
operator_info find_nud(ro_environment const & env, name const & n) {

31
src/frontends/lean/notation.cpp
View file

@ -19,39 +19,9 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
[&]() {
// mark_implicit_arguments(env, mk_if_fn(), 1);
if (kernel_only)
return;
add_alias(env, "ℕ", Nat);
add_infixl(env, ios, "+", 65, mk_nat_add_fn());
add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
add_infixl(env, ios, "*", 70, mk_nat_mul_fn());
add_infix(env, ios, "<=", 50, mk_nat_le_fn());
add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_nat_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_nat_lt_fn());
add_infix(env, ios, ">", 50, mk_nat_gt_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
add_alias(env, "ℤ", Int);
add_infixl(env, ios, "+", 65, mk_int_add_fn());
add_infixl(env, ios, "-", 65, mk_int_sub_fn());
add_prefix(env, ios, "-", 75, mk_int_neg_fn());
add_infixl(env, ios, "*", 70, mk_int_mul_fn());
add_infixl(env, ios, "div", 70, mk_int_div_fn());
add_infixl(env, ios, "mod", 70, mk_int_mod_fn());
add_infix(env, ios, "|", 50, mk_int_divides_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn());
add_infix(env, ios, "<=", 50, mk_int_le_fn());
add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_int_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_int_lt_fn());
add_infix(env, ios, ">", 50, mk_int_gt_fn());
add_alias(env, "ℝ", Real);
add_infixl(env, ios, "+", 65, mk_real_add_fn());
add_infixl(env, ios, "-", 65, mk_real_sub_fn());
@ -66,7 +36,6 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
add_infix(env, ios, "<", 50, mk_real_lt_fn());
add_infix(env, ios, ">", 50, mk_real_gt_fn());
add_coercion(env, mk_nat_to_int_fn());
add_coercion(env, mk_int_to_real_fn());
add_coercion(env, mk_nat_to_real_fn());
});

22
src/frontends/lean/parser.cpp
View file

@ -343,7 +343,7 @@ class parser::imp {
/** \brief Return true iff the current token is a '_" */
bool curr_is_placeholder() const { return curr() == scanner::token::Placeholder; }
/** \brief Return true iff the current token is a natural number */
bool curr_is_nat() const { return curr() == scanner::token::NatVal; }
bool curr_is_nat() const { return curr() == scanner::token::IntVal && m_scanner.get_num_val() >= 0; }
/** \brief Return true iff the current token is a '(' */
bool curr_is_lparen() const { return curr() == scanner::token::LeftParen; }
/** \brief Return true iff the current token is a '{' */
@ -615,6 +615,8 @@ class parser::imp {
auto p = pos();
mpz val = curr_num().get_numerator();
next();
if (val < 0)
throw parser_error("invalid level expression, value is negative", p);
if (!val.is_unsigned_int())
throw parser_error("invalid level expression, value does not fit in a machine integer", p);
return level() + val.get_unsigned_int();
@ -630,7 +632,7 @@ class parser::imp {
level parse_level_nud() {
switch (curr()) {
case scanner::token::Id: return parse_level_nud_id();
case scanner::token::NatVal: return parse_level_nud_int();
case scanner::token::IntVal: return parse_level_nud_int();
case scanner::token::LeftParen: return parse_level_lparen();
default:
throw parser_error("invalid level expression", pos());
@ -1468,10 +1470,12 @@ class parser::imp {
}
}
/** \brief Parse a natural number value. */
expr parse_nat() {
/** \brief Parse a natural/integer number value. */
expr parse_nat_int() {
auto p = pos();
expr r = save(mk_nat_value(m_scanner.get_num_val().get_numerator()), p);
mpz v = m_scanner.get_num_val().get_numerator();
expr r = v >= 0 ? mk_nat_value(v) : mk_int_value(v);
r = save(r, p);
next();
return r;
}
@ -1604,7 +1608,7 @@ class parser::imp {
case scanner::token::Forall: return parse_forall();
case scanner::token::Exists: return parse_exists();
case scanner::token::Let: return parse_let();
case scanner::token::NatVal: return parse_nat();
case scanner::token::IntVal: return parse_nat_int();
case scanner::token::DecimalVal: return parse_decimal();
case scanner::token::StringVal: return parse_string();
case scanner::token::Placeholder: return parse_placeholder();
@ -1636,7 +1640,7 @@ class parser::imp {
case scanner::token::Eq: return parse_eq(left);
case scanner::token::Arrow: return parse_arrow(left);
case scanner::token::LeftParen: return mk_app_left(left, parse_lparen());
case scanner::token::NatVal: return mk_app_left(left, parse_nat());
case scanner::token::IntVal: return mk_app_left(left, parse_nat_int());
case scanner::token::DecimalVal: return mk_app_left(left, parse_decimal());
case scanner::token::StringVal: return mk_app_left(left, parse_string());
case scanner::token::Placeholder: return mk_app_left(left, parse_placeholder());
@ -1665,7 +1669,7 @@ class parser::imp {
}
case scanner::token::Eq : return g_eq_precedence;
case scanner::token::Arrow : return g_arrow_precedence;
case scanner::token::LeftParen: case scanner::token::NatVal: case scanner::token::DecimalVal:
case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal:
case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder:
return g_app_precedence;
default:
@ -2382,7 +2386,7 @@ class parser::imp {
m_io_state.set_option(id, curr_string());
next();
break;
case scanner::token::NatVal:
case scanner::token::IntVal:
if (k != IntOption && k != UnsignedOption)
throw parser_error("invalid option value, given option is not an integer", pos());
m_io_state.set_option(id, parse_unsigned("invalid option value, value does not fit in a machine integer"));

34
src/frontends/lean/scanner.cpp
View file

@ -57,9 +57,10 @@ public:
set('_', 'a');
set('\'', 'a');
set('@', 'a');
set('-', '-');
// characters that can be used to create ids of group b
for (unsigned char b : {'=', '<', '>', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'})
for (unsigned char b : {'=', '<', '>', '^', '|', '&', '~', '+', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'})
set(b, 'b');
// punctuation
@ -241,13 +242,15 @@ scanner::token scanner::read_a_symbol() {
}
}
scanner::token scanner::read_b_symbol() {
lean_assert(normalize(curr()) == 'b');
scanner::token scanner::read_b_symbol(char prev) {
lean_assert(normalize(curr()) == 'b' || curr() == '-');
m_buffer.clear();
if (prev != 0)
m_buffer += prev;
m_buffer += curr();
next();
while (true) {
if (normalize(curr()) == 'b') {
if (normalize(curr()) == 'b' || curr() == '-') {
m_buffer += curr();
next();
} else {
@ -289,7 +292,7 @@ scanner::token scanner::read_c_symbol() {
}
}
scanner::token scanner::read_number() {
scanner::token scanner::read_number(bool pos) {
lean_assert('0' <= curr() && curr() <= '9');
mpq q(1);
m_num_val = curr() - '0';
@ -319,7 +322,9 @@ scanner::token scanner::read_number() {
}
if (is_decimal)
m_num_val /= q;
return is_decimal ? token::DecimalVal : token::NatVal;
if (!pos)
m_num_val.neg();
return is_decimal ? token::DecimalVal : token::IntVal;
}
scanner::token scanner::read_string() {
@ -426,9 +431,20 @@ scanner::token scanner::scan() {
case '{': next(); return token::LeftCurlyBracket;
case '}': next(); return token::RightCurlyBracket;
case 'a': return read_a_symbol();
case 'b': return read_b_symbol();
case 'b': return read_b_symbol(0);
case 'c': return read_c_symbol();
case '0': return read_number();
case '-':
next();
if (normalize(curr()) == '0') {
return read_number(false);
} else if (normalize(curr()) == 'b' || curr() == '-') {
return read_b_symbol('-');
} else {
m_name_val = name("-");
return token::Id;
}
break;
case '0': return read_number(true);
case '\"': return read_string();
case -1: return token::Eof;
default: lean_unreachable(); // LCOV_EXCL_LINE
@ -454,7 +470,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
case scanner::token::In: out << "in"; break;
case scanner::token::Id: out << "Id"; break;
case scanner::token::CommandId: out << "CId"; break;
case scanner::token::NatVal: out << "Nat"; break;
case scanner::token::IntVal: out << "Int"; break;
case scanner::token::DecimalVal: out << "Dec"; break;
case scanner::token::StringVal: out << "String"; break;
case scanner::token::Eq: out << "=="; break;

6
src/frontends/lean/scanner.h
View file

@ -20,7 +20,7 @@ class scanner {
public:
enum class token {
LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
Let, In, Forall, Exists, Id, CommandId, NatVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
Let, In, Forall, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
Show, By, ScriptBlock, Eof
};
protected:
@ -49,9 +49,9 @@ protected:
void read_comment();
name mk_name(name const & curr, std::string const & buf, bool only_digits);
token read_a_symbol();
token read_b_symbol();
token read_b_symbol(char prev);
token read_c_symbol();
token read_number();
token read_number(bool pos);
token read_string();
token read_script_block();
bool is_command(name const & n) const;

41
src/library/arith/int.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/environment.h"
#include "kernel/value.h"
#include "library/io_state.h"
#include "library/kernel_bindings.h"
#include "library/arith/int.h"
#include "library/arith/nat.h"
@ -35,7 +36,7 @@ public:
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)
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);
@ -51,6 +52,7 @@ expr mk_int_value(mpz const & v) {
}
expr read_int_value(deserializer & d) { return mk_int_value(read_mpz(d)); }
static value::register_deserializer_fn int_value_ds("int", read_int_value);
register_available_builtin_fn g_int_value(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;
@ -85,6 +87,7 @@ typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
MK_BUILTIN(int_add_fn, int_add_value);
expr read_int_add(deserializer & ) { return mk_int_add_fn(); }
static value::register_deserializer_fn int_add_ds("int_add", read_int_add);
register_available_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; }; };
@ -92,6 +95,7 @@ typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
MK_BUILTIN(int_mul_fn, int_mul_value);
expr read_int_mul(deserializer & ) { return mk_int_mul_fn(); }
static value::register_deserializer_fn int_mul_ds("int_mul", read_int_mul);
register_available_builtin_fn g_int_mul_value(name({"Int", "mul"}), []() { return mk_int_mul_fn(); });
constexpr char int_div_name[] = "div";
struct int_div_eval {
@ -106,6 +110,7 @@ typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
MK_BUILTIN(int_div_fn, int_div_value);
expr read_int_div(deserializer & ) { return mk_int_div_fn(); }
static value::register_deserializer_fn int_div_ds("int_div", read_int_div);
register_available_builtin_fn g_int_div_value(name({"Int", "div"}), []() { return mk_int_div_fn(); });
class int_le_value : public const_value {
public:
@ -122,6 +127,7 @@ public:
MK_BUILTIN(int_le_fn, int_le_value);
expr read_int_le(deserializer & ) { return mk_int_le_fn(); }
static value::register_deserializer_fn int_le_ds("int_le", read_int_le);
register_available_builtin_fn g_int_le_value(name({"Int", "le"}), []() { return mk_int_le_fn(); });
MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
@ -150,41 +156,14 @@ public:
MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
expr read_nat_to_int(deserializer & ) { return mk_nat_to_int_fn(); }
static value::register_deserializer_fn nat_to_int_ds("nat_to_int", read_nat_to_int);
register_available_builtin_fn g_n2i_value(name({"nat_to_int"}), []() { return mk_nat_to_int_fn(); });
MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
void import_int(environment const & env) {
env->import_builtin(
"int",
[&]() {
import_nat(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_var(Int_name, Type());
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_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
env->add_opaque_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
env->add_opaque_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
env->add_opaque_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
});
io_state ios;
env->import("int", ios);
}
static int mk_int_value(lua_State * L) {

24
src/library/arith/nat.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/value.h"
#include "library/kernel_bindings.h"
#include "library/io_state.h"
#include "library/arith/nat.h"
namespace lean {
@ -44,6 +45,7 @@ expr mk_nat_value(mpz const & v) {
}
expr read_nat_value(deserializer & d) { return mk_nat_value(read_mpz(d)); }
static value::register_deserializer_fn nat_value_ds("nat", read_nat_value);
register_available_builtin_fn g_nat_value(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;
@ -79,6 +81,7 @@ typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
MK_BUILTIN(nat_add_fn, nat_add_value);
expr read_nat_add(deserializer & ) { return mk_nat_add_fn(); }
static value::register_deserializer_fn nat_add_ds("nat_add", read_nat_add);
register_available_builtin_fn g_nat_add_value(name({"Nat", "add"}), []() { return mk_nat_add_fn(); });
constexpr char nat_mul_name[] = "mul";
/** \brief Evaluator for * : Nat -> Nat -> Nat */
@ -87,6 +90,7 @@ typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
MK_BUILTIN(nat_mul_fn, nat_mul_value);
expr read_nat_mul(deserializer & ) { return mk_nat_mul_fn(); }
static value::register_deserializer_fn nat_mul_ds("nat_mul", read_nat_mul);
register_available_builtin_fn g_nat_mul_value(name({"Nat", "mul"}), []() { return mk_nat_mul_fn(); });
/**
\brief Semantic attachment for less than or equal to operator with type
@ -107,6 +111,7 @@ public:
MK_BUILTIN(nat_le_fn, nat_le_value);
expr read_nat_le(deserializer & ) { return mk_nat_le_fn(); }
static value::register_deserializer_fn nat_le_ds("nat_le", read_nat_le);
register_available_builtin_fn g_nat_le_value(name({"Nat", "le"}), []() { return mk_nat_le_fn(); });
MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"}));
MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"}));
@ -114,23 +119,8 @@ MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
void import_nat(environment const & env) {
env->import_builtin(
"nat",
[&]() {
expr nn_b = Nat >> (Nat >> Bool);
expr x = Const("x");
expr y = Const("y");
env->add_var(Nat_name, Type());
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_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
});
io_state ios;
env->import("nat", ios);
}
static int mk_nat_value(lua_State * L) {

10
src/tests/frontends/lean/scanner.cpp
View file

@ -24,7 +24,7 @@ static void scan(char const * str, list<name> const & cmds = list<name>()) {
std::cout << t;
if (t == st::Id || t == st::CommandId)
std::cout << "[" << s.get_name_val() << "]";
else if (t == st::NatVal || t == st::DecimalVal)
else if (t == st::IntVal || t == st::DecimalVal)
std::cout << "[" << s.get_num_val() << "]";
else if (t == st::StringVal)
std::cout << "[\"" << escaped(s.get_str_val().c_str()) << "\"]";
@ -82,11 +82,11 @@ static void tst2() {
check("x+y", {st::Id, st::Id, st::Id});
check("(* testing *)", {});
check(" 2.31 ", {st::DecimalVal});
check(" 333 22", {st::NatVal, st::NatVal});
check(" 333 22", {st::IntVal, st::IntVal});
check("Int -> Int", {st::Id, st::Arrow, st::Id});
check("Int --> Int", {st::Id, st::Id, st::Id});
check("x := 10", {st::Id, st::Assign, st::NatVal});
check("(x+1):Int", {st::LeftParen, st::Id, st::Id, st::NatVal, st::RightParen, st::Colon, st::Id});
check("x := 10", {st::Id, st::Assign, st::IntVal});
check("(x+1):Int", {st::LeftParen, st::Id, st::Id, st::IntVal, st::RightParen, st::Colon, st::Id});
check("{x}", {st::LeftCurlyBracket, st::Id, st::RightCurlyBracket});
check("\u03BB \u03A0 \u2192", {st::Lambda, st::Pi, st::Arrow});
scan("++\u2295++x\u2296\u2296");
@ -95,7 +95,7 @@ static void tst2() {
check_name("x10", name("x10"));
check_name("x::10", name(name("x"), 10));
check_name("x::10::bla::0", name(name(name(name("x"), 10), "bla"), 0u));
check("0::1", {st::NatVal, st::Colon, st::Colon, st::NatVal});
check("0::1", {st::IntVal, st::Colon, st::Colon, st::IntVal});
check_name("\u2296\u2296", name("\u2296\u2296"));
scan_error("x::1000000000000000000");
scan("Theorem a : Bool Axiom b : Int", list<name>({"Theorem", "Axiom"}));

4
tests/lean/arith3.lean.expected.out
View file

@ -4,8 +4,8 @@
2
2
1
- 8 mod 3
-8 mod 3
Set: lean::pp::notation
Int::mod (Nat::neg 8) 3
Int::mod -8 3
-2
-8

2
tests/lean/elab4.lean.expected.out
View file

@ -6,6 +6,8 @@
Proved: R2
Set: lean::pp::implicit
Import "basic"
Import "nat"
Import "int"
Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
@eq Type A A'

2
tests/lean/elab5.lean.expected.out
View file

@ -6,6 +6,8 @@
Proved: R2
Set: lean::pp::implicit
Import "basic"
Import "nat"
Import "int"
Variable C {A B : Type} (H : @eq Type A B) (a : A) : B
Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (Π x : A, B x) (Π x : A', B' x)) :
@eq Type A A'

2
tests/lean/implicit6.lean.expected.out
View file

@ -8,4 +8,4 @@
Set: lean::pp::coercion
f ⊤ ⊥
Nat::add 10 20
Int::add (nat_to_int 10) (Nat::neg 20)
Int::add (nat_to_int 10) (Int::neg (nat_to_int 20))