max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init): use extern when declarating nat primitives

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-12 18:12:29 -08:00
parent 532a51b152
commit 456ed23cc2
5 changed files with 26 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/core.lean
View file

@ -427,7 +427,8 @@ export has_insert (insert)
has_insert.insert a ∅
/- nat basic instances -/
protected def nat.add : nat → nat → nat
@[extern cpp "lean::nat_add"]
protected def nat.add : (@& nat) → (@& nat) → nat
| a nat.zero := a
| a (nat.succ b) := nat.succ (nat.add a b)

18
library/init/data/nat/basic.lean
View file

@ -10,6 +10,7 @@ notation `ℕ` := nat
namespace nat
@[extern cpp "lean::nat_dec_eq"]
def beq : nat → nat → bool
| zero zero := tt
| zero (succ m) := ff
@ -34,13 +35,15 @@ theorem ne_of_beq_eq_ff : ∀ {n m : nat}, beq n m = ff → n ≠ m
have n ≠ m, from ne_of_beq_eq_ff this,
nat.no_confusion h₂ (λ h₂, absurd h₂ this)
protected def dec_eq (n m : nat) : decidable (n = m) :=
@[extern cpp "lean::nat_dec_eq"]
protected def dec_eq (n m : @& nat) : decidable (n = m) :=
if h : beq n m = tt then is_true (eq_of_beq_eq_tt h)
else is_false (ne_of_beq_eq_ff (eq_ff_of_ne_tt h))
@[inline] instance : decidable_eq nat :=
{dec_eq := nat.dec_eq}
@[extern cpp "lean::nat_dec_le"]
def ble : nat → nat → bool
| zero zero := tt
| zero (succ m) := tt
@ -59,15 +62,18 @@ nat.le (succ n) m
instance : has_lt nat :=
⟨nat.lt⟩
@[extern cpp inline "lean::nat_sub(#1, lean::box(1))"]
def pred : nat → nat
| 0 := 0
| (a+1) := a
protected def sub : nat → nat → nat
@[extern cpp "lean::nat_sub"]
protected def sub : (@& nat) → (@& nat) → nat
| a 0 := a
| a (b+1) := pred (sub a b)
protected def mul : nat → nat → nat
@[extern cpp "lean::nat_mul"]
protected def mul : (@& nat) → (@& nat) → nat
| a 0 := 0
| a (b+1) := (mul a b) + a
@ -252,10 +258,12 @@ theorem pred_le_pred : ∀ {n m : nat}, n ≤ m → pred n ≤ pred m
theorem le_of_succ_le_succ {n m : nat} : succ n ≤ succ m → n ≤ m :=
pred_le_pred
instance dec_le (n m : nat) : decidable (n ≤ m) :=
@[extern cpp "lean::nat_dec_le"]
instance dec_le (n m : @& nat) : decidable (n ≤ m) :=
dec_eq (ble n m) tt
instance dec_lt (n m : nat) : decidable (n < m) :=
@[extern cpp "lean::nat_dec_lt"]
instance dec_lt (n m : @& nat) : decidable (n < m) :=
nat.dec_le (succ n) m
protected theorem eq_or_lt_of_le : ∀ {n m: nat}, n ≤ m → n = m ∨ n < m

8
library/init/data/nat/div.lean
View file

@ -13,7 +13,9 @@ private def div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x :=
private def div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y + 1 else zero
protected def div := well_founded.fix lt_wf div.F
@[extern cpp "lean::nat_div"]
protected def div (a b : @& nat) : nat :=
well_founded.fix lt_wf div.F a b
instance : has_div nat :=
⟨nat.div⟩
@ -43,7 +45,9 @@ well_founded.fix nat.lt_wf (div.induction.F C h₁ h₂) x y
private def mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
protected def mod := well_founded.fix lt_wf mod.F
@[extern cpp "lean::nat_mod"]
protected def mod (a b : @& nat) : nat :=
well_founded.fix lt_wf mod.F a b
instance : has_mod nat :=
⟨nat.mod⟩

78
src/library/compiler/builtin.cpp
View file

@ -146,84 +146,6 @@ bool get_native_borrowed_info(environment const & env, name const & c, buffer<bo
void initialize_builtin() {
g_initial_native_decls = new native_decl_map();
expr o = mk_enf_object_type();
expr u8 = mk_constant(get_uint8_name());
expr u16 = mk_constant(get_uint16_name());
expr u32 = mk_constant(get_uint32_name());
expr u64 = mk_constant(get_uint64_name());
expr us = mk_constant(get_usize_name());
expr o_o = mk_arrow(o, o);
expr o_o_o = mk_arrow(o, o_o);
expr o_o_o_o = mk_arrow(o, o_o_o);
expr o_o_o_o_o = mk_arrow(o, o_o_o_o);
expr o_u8 = mk_arrow(o, u8);
expr o_u8_u8_o_o = mk_arrow(o, mk_arrow(u8, mk_arrow(u8, o_o)));
expr u8_u8 = mk_arrow(u8, u8);
expr u8_u8_u8 = mk_arrow(u8, u8_u8);
expr u8_o_u8 = mk_arrow(u8, o_u8);
expr u8_o = mk_arrow(u8, o);
expr u8_u8_o = mk_arrow(u8, u8_o);
expr o_o_u8 = mk_arrow(o, o_u8);
expr o_u16 = mk_arrow(o, u16);
expr o_u16_u16_o_o = mk_arrow(o, mk_arrow(u16, mk_arrow(u16, o_o)));
expr u16_u16 = mk_arrow(u16, u16);
expr u16_u16_u16 = mk_arrow(u16, u16_u16);
expr u16_o_u16 = mk_arrow(u16, o_u16);
expr u16_o = mk_arrow(u16, o);
expr u16_u16_o = mk_arrow(u16, u16_o);
expr u16_u16_u8 = mk_arrow(u16, mk_arrow(u16, u8));
expr o_u32 = mk_arrow(o, u32);
expr o_u32_o = mk_arrow(o, mk_arrow(u32, o));
expr o_u32_u32_o_o = mk_arrow(o, mk_arrow(u32, mk_arrow(u32, o_o)));
expr u32_u32 = mk_arrow(u32, u32);
expr u32_u32_u32 = mk_arrow(u32, u32_u32);
expr u32_o_u32 = mk_arrow(u32, o_u32);
expr u32_o = mk_arrow(u32, o);
expr u32_u32_o = mk_arrow(u32, u32_o);
expr u32_u32_u8 = mk_arrow(u32, mk_arrow(u32, u8));
expr o_u64 = mk_arrow(o, u64);
expr o_u64_u64_o_o = mk_arrow(o, mk_arrow(u64, mk_arrow(u64, o_o)));
expr u64_u64 = mk_arrow(u64, u64);
expr u64_u64_u64 = mk_arrow(u64, u64_u64);
expr u64_o_u64 = mk_arrow(u64, o_u64);
expr u64_o = mk_arrow(u64, o);
expr u64_u64_o = mk_arrow(u64, u64_o);
expr u64_u64_u8 = mk_arrow(u64, mk_arrow(u64, u8));
expr o_us = mk_arrow(o, us);
expr o_us_us_o_o = mk_arrow(o, mk_arrow(us, mk_arrow(us, o_o)));
expr us_us = mk_arrow(us, us);
expr us_us_us = mk_arrow(us, us_us);
expr us_o_us = mk_arrow(us, o_us);
expr us_o = mk_arrow(us, o);
expr us_us_o = mk_arrow(us, us_o);
expr us_us_u8 = mk_arrow(us, mk_arrow(us, u8));
list<bool> b{true};
list<bool> bb{true, true};
list<bool> c{false};
list<bool> cc{false, false};
list<bool> cb{false, true};
list<bool> bc{true, false};
list<bool> bbb{true, true, true};
list<bool> bccc{true, false, false, false};
list<bool> bbcc{true, true, false, false};
/* nat builtin functions */
register_builtin(name({"nat", "add"}), o_o_o, "lean::nat_add", bb);
register_builtin(name({"nat", "sub"}), o_o_o, "lean::nat_sub", bb);
register_builtin(name({"nat", "mul"}), o_o_o, "lean::nat_mul", bb);
register_builtin(name({"nat", "div"}), o_o_o, "lean::nat_div", bb);
register_builtin(name({"nat", "mod"}), o_o_o, "lean::nat_mod", bb);
register_builtin(name({"nat", "dec_eq"}), o_o_u8, "lean::nat_dec_eq", bb);
register_builtin(name({"nat", "dec_lt"}), o_o_u8, "lean::nat_dec_lt", bb);
register_builtin(name({"nat", "dec_le"}), o_o_u8, "lean::nat_dec_le", bb);
g_ext = new native_decls_reg();
}

5
src/library/vm/vm_nat.cpp
View file

@ -127,6 +127,10 @@ vm_obj nat_sub(vm_obj const & a1, vm_obj const & a2) {
}
}
vm_obj nat_pred(vm_obj const & a) {
return nat_sub(a, mk_vm_simple(1));
}
vm_obj nat_div(vm_obj const & a1, vm_obj const & a2) {
if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
unsigned v1 = cidx(a1);
@ -191,6 +195,7 @@ void initialize_vm_nat() {
DECLARE_VM_BUILTIN(name({"nat", "add"}), nat_add);
DECLARE_VM_BUILTIN(name({"nat", "mul"}), nat_mul);
DECLARE_VM_BUILTIN(name({"nat", "sub"}), nat_sub);
DECLARE_VM_BUILTIN(name({"nat", "pred"}), nat_pred);
DECLARE_VM_BUILTIN(name({"nat", "div"}), nat_div);
DECLARE_VM_BUILTIN(name({"nat", "mod"}), nat_mod);
DECLARE_VM_BUILTIN(name({"nat", "dec_eq"}), nat_decidable_eq);