feat(builtin): use namespaces when defining nat, int and real.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
d633622d90
commit
770145a361
9 changed files with 132 additions and 118 deletions
|
|
@ -2,63 +2,67 @@ 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.
|
||||
Namespace Int.
|
||||
Builtin numeral.
|
||||
|
||||
Definition Int::abs (a : Int) : Int := if (0 ≤ a) a (- a).
|
||||
Notation 55 | _ | : Int::abs.
|
||||
Builtin add : Int → Int → Int.
|
||||
Infixl 65 + : add.
|
||||
|
||||
Definition Nat::sub (a b : Nat) : Int := nat_to_int a - nat_to_int b.
|
||||
Infixl 65 - : Nat::sub.
|
||||
Builtin mul : Int → Int → Int.
|
||||
Infixl 70 * : mul.
|
||||
|
||||
Definition Nat::neg (a : Nat) : Int := - (nat_to_int a).
|
||||
Notation 75 - _ : Nat::neg.
|
||||
Builtin div : Int → Int → Int.
|
||||
Infixl 70 div : div.
|
||||
|
||||
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.
|
||||
Builtin le : Int → Int → Bool.
|
||||
Infix 50 <= : le.
|
||||
Infix 50 ≤ : le.
|
||||
|
||||
Definition ge (a b : Int) : Bool := b ≤ a.
|
||||
Infix 50 >= : ge.
|
||||
Infix 50 ≥ : ge.
|
||||
|
||||
Definition lt (a b : Int) : Bool := ¬ (a ≥ b).
|
||||
Infix 50 < : lt.
|
||||
|
||||
Definition gt (a b : Int) : Bool := ¬ (a ≤ b).
|
||||
Infix 50 > : gt.
|
||||
|
||||
Definition sub (a b : Int) : Int := a + -1 * b.
|
||||
Infixl 65 - : sub.
|
||||
|
||||
Definition neg (a : Int) : Int := -1 * a.
|
||||
Notation 75 - _ : neg.
|
||||
|
||||
Definition mod (a b : Int) : Int := a - b * (a div b).
|
||||
Infixl 70 mod : mod.
|
||||
|
||||
Definition divides (a b : Int) : Bool := (b mod a) = 0.
|
||||
Infix 50 | : divides.
|
||||
|
||||
Definition abs (a : Int) : Int := if (0 ≤ a) a (- a).
|
||||
Notation 55 | _ | : abs.
|
||||
|
||||
SetOpaque sub true.
|
||||
SetOpaque neg true.
|
||||
SetOpaque mod true.
|
||||
SetOpaque divides true.
|
||||
SetOpaque abs true.
|
||||
SetOpaque ge true.
|
||||
SetOpaque lt true.
|
||||
SetOpaque gt true.
|
||||
EndNamespace.
|
||||
|
||||
Namespace Nat.
|
||||
Definition sub (a b : Nat) : Int := nat_to_int a - nat_to_int b.
|
||||
Infixl 65 - : sub.
|
||||
|
||||
Definition neg (a : Nat) : Int := - (nat_to_int a).
|
||||
Notation 75 - _ : neg.
|
||||
|
||||
SetOpaque sub true.
|
||||
SetOpaque neg true.
|
||||
EndNamespace.
|
||||
|
|
@ -3,32 +3,36 @@ Import kernel.
|
|||
Variable Nat : Type.
|
||||
Alias ℕ : Nat.
|
||||
|
||||
Builtin Nat::numeral.
|
||||
Namespace Nat.
|
||||
|
||||
Builtin Nat::add : Nat → Nat → Nat.
|
||||
Infixl 65 + : Nat::add.
|
||||
Builtin numeral.
|
||||
|
||||
Builtin Nat::mul : Nat → Nat → Nat.
|
||||
Infixl 70 * : Nat::mul.
|
||||
Builtin add : Nat → Nat → Nat.
|
||||
Infixl 65 + : add.
|
||||
|
||||
Builtin Nat::le : Nat → Nat → Bool.
|
||||
Infix 50 <= : Nat::le.
|
||||
Infix 50 ≤ : Nat::le.
|
||||
Builtin mul : Nat → Nat → Nat.
|
||||
Infixl 70 * : mul.
|
||||
|
||||
Definition Nat::ge (a b : Nat) := b ≤ a.
|
||||
Infix 50 >= : Nat::ge.
|
||||
Infix 50 ≥ : Nat::ge.
|
||||
Builtin le : Nat → Nat → Bool.
|
||||
Infix 50 <= : le.
|
||||
Infix 50 ≤ : le.
|
||||
|
||||
Definition Nat::lt (a b : Nat) := ¬ (a ≥ b).
|
||||
Infix 50 < : Nat::lt.
|
||||
Definition ge (a b : Nat) := b ≤ a.
|
||||
Infix 50 >= : ge.
|
||||
Infix 50 ≥ : ge.
|
||||
|
||||
Definition Nat::gt (a b : Nat) := ¬ (a ≤ b).
|
||||
Infix 50 > : Nat::gt.
|
||||
Definition lt (a b : Nat) := ¬ (a ≥ b).
|
||||
Infix 50 < : lt.
|
||||
|
||||
Definition Nat::id (a : Nat) := a.
|
||||
Notation 55 | _ | : Nat::id.
|
||||
Definition gt (a b : Nat) := ¬ (a ≤ b).
|
||||
Infix 50 > : gt.
|
||||
|
||||
SetOpaque Nat::ge true.
|
||||
SetOpaque Nat::lt true.
|
||||
SetOpaque Nat::gt true.
|
||||
SetOpaque Nat::id true.
|
||||
Definition id (a : Nat) := a.
|
||||
Notation 55 | _ | : id.
|
||||
|
||||
SetOpaque ge true.
|
||||
SetOpaque lt true.
|
||||
SetOpaque gt true.
|
||||
SetOpaque id true.
|
||||
|
||||
EndNamespace.
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
|
|
@ -2,43 +2,43 @@ Import int.
|
|||
|
||||
Variable Real : Type.
|
||||
Alias ℝ : Real.
|
||||
|
||||
Builtin Real::numeral.
|
||||
|
||||
Builtin Real::add : Real → Real → Real.
|
||||
Infixl 65 + : Real::add.
|
||||
|
||||
Builtin Real::mul : Real → Real → Real.
|
||||
Infixl 70 * : Real::mul.
|
||||
|
||||
Builtin Real::div : Real → Real → Real.
|
||||
Infixl 70 / : Real::div.
|
||||
|
||||
Builtin Real::le : Real → Real → Bool.
|
||||
Infix 50 <= : Real::le.
|
||||
Infix 50 ≤ : Real::le.
|
||||
|
||||
Definition Real::ge (a b : Real) : Bool := b ≤ a.
|
||||
Infix 50 >= : Real::ge.
|
||||
Infix 50 ≥ : Real::ge.
|
||||
|
||||
Definition Real::lt (a b : Real) : Bool := ¬ (a ≥ b).
|
||||
Infix 50 < : Real::lt.
|
||||
|
||||
Definition Real::gt (a b : Real) : Bool := ¬ (a ≤ b).
|
||||
Infix 50 > : Real::gt.
|
||||
|
||||
Definition Real::sub (a b : Real) : Real := a + -1.0 * b.
|
||||
Infixl 65 - : Real::sub.
|
||||
|
||||
Definition Real::neg (a : Real) : Real := -1.0 * a.
|
||||
Notation 75 - _ : Real::neg.
|
||||
|
||||
Definition Real::abs (a : Real) : Real := if (0.0 ≤ a) a (- a).
|
||||
Notation 55 | _ | : Real::abs.
|
||||
|
||||
Builtin int_to_real : Int → Real.
|
||||
Coercion int_to_real.
|
||||
|
||||
Definition nat_to_real (a : Nat) : Real := int_to_real (nat_to_int a).
|
||||
Coercion nat_to_real.
|
||||
|
||||
Namespace Real.
|
||||
Builtin numeral.
|
||||
|
||||
Builtin add : Real → Real → Real.
|
||||
Infixl 65 + : add.
|
||||
|
||||
Builtin mul : Real → Real → Real.
|
||||
Infixl 70 * : mul.
|
||||
|
||||
Builtin div : Real → Real → Real.
|
||||
Infixl 70 / : div.
|
||||
|
||||
Builtin le : Real → Real → Bool.
|
||||
Infix 50 <= : le.
|
||||
Infix 50 ≤ : le.
|
||||
|
||||
Definition ge (a b : Real) : Bool := b ≤ a.
|
||||
Infix 50 >= : ge.
|
||||
Infix 50 ≥ : ge.
|
||||
|
||||
Definition lt (a b : Real) : Bool := ¬ (a ≥ b).
|
||||
Infix 50 < : lt.
|
||||
|
||||
Definition gt (a b : Real) : Bool := ¬ (a ≤ b).
|
||||
Infix 50 > : gt.
|
||||
|
||||
Definition sub (a b : Real) : Real := a + -1.0 * b.
|
||||
Infixl 65 - : sub.
|
||||
|
||||
Definition neg (a : Real) : Real := -1.0 * a.
|
||||
Notation 75 - _ : neg.
|
||||
|
||||
Definition abs (a : Real) : Real := if (0.0 ≤ a) a (- a).
|
||||
Notation 55 | _ | : abs.
|
||||
EndNamespace.
|
||||
|
|
|
|||
|
|
@ -914,8 +914,11 @@ class parser::imp {
|
|||
\brief Try to find an object (Definition or Postulate) named \c
|
||||
id in the frontend/environment. If there isn't one, then tries
|
||||
to check if \c id is a builtin symbol. If it is not throws an error.
|
||||
|
||||
If \c implicit_args is true, then we also parse explicit arguments until
|
||||
we have a placeholder forall implicit ones.
|
||||
*/
|
||||
expr get_name_ref(name const & id, pos_info const & p) {
|
||||
expr get_name_ref(name const & id, pos_info const & p, bool implicit_args = true) {
|
||||
lean_assert(!m_namespace_prefixes.empty());
|
||||
auto it = m_namespace_prefixes.end();
|
||||
auto begin = m_namespace_prefixes.begin();
|
||||
|
|
@ -926,7 +929,7 @@ class parser::imp {
|
|||
if (obj) {
|
||||
object_kind k = obj->kind();
|
||||
if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) {
|
||||
if (has_implicit_arguments(m_env, obj->get_name())) {
|
||||
if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) {
|
||||
std::vector<bool> const & imp_args = get_implicit_arguments(m_env, obj->get_name());
|
||||
buffer<expr> args;
|
||||
pos_info p = pos();
|
||||
|
|
@ -2278,8 +2281,9 @@ class parser::imp {
|
|||
unsigned prec = parse_precedence();
|
||||
name op_id = parse_op_id();
|
||||
check_colon_next("invalid operator definition, ':' expected");
|
||||
auto name_pos = pos();
|
||||
name name_id = check_identifier_next("invalid operator definition, identifier expected");
|
||||
expr d = mk_constant(name_id);
|
||||
expr d = get_name_ref(name_id, name_pos, false);
|
||||
switch (fx) {
|
||||
case fixity::Infix: add_infix(m_env, m_io_state, op_id, prec, d); break;
|
||||
case fixity::Infixl: add_infixl(m_env, m_io_state, op_id, prec, d); break;
|
||||
|
|
@ -2319,8 +2323,9 @@ class parser::imp {
|
|||
if (parts.size() == 0) {
|
||||
throw parser_error("invalid notation declaration, it must have at least one identifier", p);
|
||||
}
|
||||
auto id_pos = pos();
|
||||
name name_id = check_identifier_next("invalid notation declaration, identifier expected");
|
||||
expr d = mk_constant(name_id);
|
||||
expr d = get_name_ref(name_id, id_pos, false);
|
||||
if (parts.size() == 1) {
|
||||
if (first_placeholder && prev_placeholder) {
|
||||
// infix: _ ID _
|
||||
|
|
@ -2593,9 +2598,10 @@ class parser::imp {
|
|||
next();
|
||||
auto id_pos = pos();
|
||||
name id = check_identifier_next("invalid builtin declaration, identifier expected");
|
||||
auto d = get_builtin(id);
|
||||
name full_id = mk_full_name(id);
|
||||
auto d = get_builtin(full_id);
|
||||
if (!d)
|
||||
throw parser_error(sstream() << "unknown builtin '" << id << "'", id_pos);
|
||||
throw parser_error(sstream() << "unknown builtin '" << full_id << "'", id_pos);
|
||||
expr b = d->first;
|
||||
if (d->second) {
|
||||
m_env->add_builtin_set(b);
|
||||
|
|
@ -2623,8 +2629,8 @@ class parser::imp {
|
|||
}
|
||||
m_env->add_builtin(d->first);
|
||||
if (m_verbose)
|
||||
regular(m_io_state) << " Added: " << id << endl;
|
||||
register_implicit_arguments(id, bindings);
|
||||
regular(m_io_state) << " Added: " << full_id << endl;
|
||||
register_implicit_arguments(full_id, bindings);
|
||||
}
|
||||
|
||||
void parse_namespace() {
|
||||
|
|
|
|||
Loading…
Reference in a new issue