diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean index ba3f2ce472..a7497d471d 100644 --- a/library/init/data/uint.lean +++ b/library/init/data/uint.lean @@ -8,20 +8,20 @@ import init.data.fin.basic open nat -def uint8_sz : nat := 65536 +def uint8_sz : nat := 256 structure uint8 := (val : fin uint8_sz) def uint8.of_nat (n : nat) : uint8 := ⟨fin.of_nat n⟩ -def uint8.to_nat : uint8 → nat | ⟨a⟩ := a.val -def uint8.add : uint8 → uint8 → uint8 | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ -def uint8.sub : uint8 → uint8 → uint8 | ⟨a⟩ ⟨b⟩ := ⟨a - b⟩ -def uint8.mul : uint8 → uint8 → uint8 | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -def uint8.div : uint8 → uint8 → uint8 | ⟨a⟩ ⟨b⟩ := ⟨a / b⟩ -def uint8.mod : uint8 → uint8 → uint8 | ⟨a⟩ ⟨b⟩ := ⟨a % b⟩ -def uint8.modn : uint8 → nat → uint8 | ⟨a⟩ b := ⟨a %ₙ b⟩ -def uint8.lt : uint8 → uint8 → Prop | ⟨a⟩ ⟨b⟩ := a < b -def uint8.le : uint8 → uint8 → Prop | ⟨a⟩ ⟨b⟩ := a ≤ b +def uint8.to_nat (n : uint8) : nat := n.val.val +def uint8.add (a b : uint8) : uint8 := ⟨a.val + b.val⟩ +def uint8.sub (a b : uint8) : uint8 := ⟨a.val - b.val⟩ +def uint8.mul (a b : uint8) : uint8 := ⟨a.val * b.val⟩ +def uint8.div (a b : uint8) : uint8 := ⟨a.val / b.val⟩ +def uint8.mod (a b : uint8) : uint8 := ⟨a.val % b.val⟩ +def uint8.modn (a : uint8) (n : nat) : uint8 := ⟨a.val %ₙ n⟩ +def uint8.lt (a b : uint8) : Prop := a.val < b.val +def uint8.le (a b : uint8) : Prop := a.val ≤ b.val instance : has_zero uint8 := ⟨uint8.of_nat 0⟩ instance : has_one uint8 := ⟨uint8.of_nat 1⟩ @@ -35,14 +35,17 @@ instance : has_lt uint8 := ⟨uint8.lt⟩ instance : has_le uint8 := ⟨uint8.le⟩ instance : inhabited uint8 := ⟨0⟩ -def uint8.dec_eq : Π (a b : uint8), decidable (a = b) -| ⟨a⟩ ⟨b⟩ := if h : a = b then is_true (h ▸ rfl) else is_false (λ h', uint8.no_confusion h' (λ h', absurd h' h)) +def uint8.dec_eq (a b : uint8) : decidable (a = b) := +uint8.cases_on a $ λ n, uint8.cases_on b $ λ m, + if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint8.no_confusion h' (λ h', absurd h' h)) -def uint8.dec_lt : Π (a b : uint8), decidable (a < b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a < b)) +def uint8.dec_lt (a b : uint8) : decidable (a < b) := +uint8.cases_on a $ λ n, uint8.cases_on b $ λ m, + infer_instance_as (decidable (n < m)) -def uint8.dec_le : Π (a b : uint8), decidable (a ≤ b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a ≤ b)) +def uint8.dec_le (a b : uint8) : decidable (a ≤ b) := +uint8.cases_on a $ λ n, uint8.cases_on b $ λ m, + infer_instance_as (decidable (n <= m)) instance : decidable_eq uint8 := {dec_eq := uint8.dec_eq} instance uint8.has_decidable_lt (a b : uint8) : decidable (a < b) := uint8.dec_lt a b @@ -53,15 +56,15 @@ structure uint16 := (val : fin uint16_sz) def uint16.of_nat (n : nat) : uint16 := ⟨fin.of_nat n⟩ -def uint16.to_nat : uint16 → nat | ⟨a⟩ := a.val -def uint16.add : uint16 → uint16 → uint16 | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ -def uint16.sub : uint16 → uint16 → uint16 | ⟨a⟩ ⟨b⟩ := ⟨a - b⟩ -def uint16.mul : uint16 → uint16 → uint16 | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -def uint16.div : uint16 → uint16 → uint16 | ⟨a⟩ ⟨b⟩ := ⟨a / b⟩ -def uint16.mod : uint16 → uint16 → uint16 | ⟨a⟩ ⟨b⟩ := ⟨a % b⟩ -def uint16.modn : uint16 → nat → uint16 | ⟨a⟩ b := ⟨a %ₙ b⟩ -def uint16.lt : uint16 → uint16 → Prop | ⟨a⟩ ⟨b⟩ := a < b -def uint16.le : uint16 → uint16 → Prop | ⟨a⟩ ⟨b⟩ := a ≤ b +def uint16.to_nat (n : uint16) : nat := n.val.val +def uint16.add (a b : uint16) : uint16 := ⟨a.val + b.val⟩ +def uint16.sub (a b : uint16) : uint16 := ⟨a.val - b.val⟩ +def uint16.mul (a b : uint16) : uint16 := ⟨a.val * b.val⟩ +def uint16.div (a b : uint16) : uint16 := ⟨a.val / b.val⟩ +def uint16.mod (a b : uint16) : uint16 := ⟨a.val % b.val⟩ +def uint16.modn (a : uint16) (n : nat) : uint16 := ⟨a.val %ₙ n⟩ +def uint16.lt (a b : uint16) : Prop := a.val < b.val +def uint16.le (a b : uint16) : Prop := a.val ≤ b.val instance : has_zero uint16 := ⟨uint16.of_nat 0⟩ instance : has_one uint16 := ⟨uint16.of_nat 1⟩ @@ -75,14 +78,17 @@ instance : has_lt uint16 := ⟨uint16.lt⟩ instance : has_le uint16 := ⟨uint16.le⟩ instance : inhabited uint16 := ⟨0⟩ -def uint16.dec_eq : Π (a b : uint16), decidable (a = b) -| ⟨a⟩ ⟨b⟩ := if h : a = b then is_true (h ▸ rfl) else is_false (λ h', uint16.no_confusion h' (λ h', absurd h' h)) +def uint16.dec_eq (a b : uint16) : decidable (a = b) := +uint16.cases_on a $ λ n, uint16.cases_on b $ λ m, + if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint16.no_confusion h' (λ h', absurd h' h)) -def uint16.dec_lt : Π (a b : uint16), decidable (a < b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a < b)) +def uint16.dec_lt (a b : uint16) : decidable (a < b) := +uint16.cases_on a $ λ n, uint16.cases_on b $ λ m, + infer_instance_as (decidable (n < m)) -def uint16.dec_le : Π (a b : uint16), decidable (a ≤ b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a ≤ b)) +def uint16.dec_le (a b : uint16) : decidable (a ≤ b) := +uint16.cases_on a $ λ n, uint16.cases_on b $ λ m, + infer_instance_as (decidable (n <= m)) instance : decidable_eq uint16 := {dec_eq := uint16.dec_eq} instance uint16.has_decidable_lt (a b : uint16) : decidable (a < b) := uint16.dec_lt a b @@ -93,15 +99,15 @@ structure uint32 := (val : fin uint32_sz) def uint32.of_nat (n : nat) : uint32 := ⟨fin.of_nat n⟩ -def uint32.to_nat : uint32 → nat | ⟨a⟩ := a.val -def uint32.add : uint32 → uint32 → uint32 | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ -def uint32.sub : uint32 → uint32 → uint32 | ⟨a⟩ ⟨b⟩ := ⟨a - b⟩ -def uint32.mul : uint32 → uint32 → uint32 | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -def uint32.div : uint32 → uint32 → uint32 | ⟨a⟩ ⟨b⟩ := ⟨a / b⟩ -def uint32.mod : uint32 → uint32 → uint32 | ⟨a⟩ ⟨b⟩ := ⟨a % b⟩ -def uint32.modn : uint32 → nat → uint32 | ⟨a⟩ b := ⟨a %ₙ b⟩ -def uint32.lt : uint32 → uint32 → Prop | ⟨a⟩ ⟨b⟩ := a < b -def uint32.le : uint32 → uint32 → Prop | ⟨a⟩ ⟨b⟩ := a ≤ b +def uint32.to_nat (n : uint32) : nat := n.val.val +def uint32.add (a b : uint32) : uint32 := ⟨a.val + b.val⟩ +def uint32.sub (a b : uint32) : uint32 := ⟨a.val - b.val⟩ +def uint32.mul (a b : uint32) : uint32 := ⟨a.val * b.val⟩ +def uint32.div (a b : uint32) : uint32 := ⟨a.val / b.val⟩ +def uint32.mod (a b : uint32) : uint32 := ⟨a.val % b.val⟩ +def uint32.modn (a : uint32) (n : nat) : uint32 := ⟨a.val %ₙ n⟩ +def uint32.lt (a b : uint32) : Prop := a.val < b.val +def uint32.le (a b : uint32) : Prop := a.val ≤ b.val instance : has_zero uint32 := ⟨uint32.of_nat 0⟩ instance : has_one uint32 := ⟨uint32.of_nat 1⟩ @@ -115,14 +121,17 @@ instance : has_lt uint32 := ⟨uint32.lt⟩ instance : has_le uint32 := ⟨uint32.le⟩ instance : inhabited uint32 := ⟨0⟩ -def uint32.dec_eq : Π (a b : uint32), decidable (a = b) -| ⟨a⟩ ⟨b⟩ := if h : a = b then is_true (h ▸ rfl) else is_false (λ h', uint32.no_confusion h' (λ h', absurd h' h)) +def uint32.dec_eq (a b : uint32) : decidable (a = b) := +uint32.cases_on a $ λ n, uint32.cases_on b $ λ m, + if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint32.no_confusion h' (λ h', absurd h' h)) -def uint32.dec_lt : Π (a b : uint32), decidable (a < b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a < b)) +def uint32.dec_lt (a b : uint32) : decidable (a < b) := +uint32.cases_on a $ λ n, uint32.cases_on b $ λ m, + infer_instance_as (decidable (n < m)) -def uint32.dec_le : Π (a b : uint32), decidable (a ≤ b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a ≤ b)) +def uint32.dec_le (a b : uint32) : decidable (a ≤ b) := +uint32.cases_on a $ λ n, uint32.cases_on b $ λ m, + infer_instance_as (decidable (n <= m)) instance : decidable_eq uint32 := {dec_eq := uint32.dec_eq} instance uint32.has_decidable_lt (a b : uint32) : decidable (a < b) := uint32.dec_lt a b @@ -133,15 +142,15 @@ structure uint64 := (val : fin uint64_sz) def uint64.of_nat (n : nat) : uint64 := ⟨fin.of_nat n⟩ -def uint64.to_nat : uint64 → nat | ⟨a⟩ := a.val -def uint64.add : uint64 → uint64 → uint64 | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ -def uint64.sub : uint64 → uint64 → uint64 | ⟨a⟩ ⟨b⟩ := ⟨a - b⟩ -def uint64.mul : uint64 → uint64 → uint64 | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -def uint64.div : uint64 → uint64 → uint64 | ⟨a⟩ ⟨b⟩ := ⟨a / b⟩ -def uint64.mod : uint64 → uint64 → uint64 | ⟨a⟩ ⟨b⟩ := ⟨a % b⟩ -def uint64.modn : uint64 → nat → uint64 | ⟨a⟩ b := ⟨a %ₙ b⟩ -def uint64.lt : uint64 → uint64 → Prop | ⟨a⟩ ⟨b⟩ := a < b -def uint64.le : uint64 → uint64 → Prop | ⟨a⟩ ⟨b⟩ := a ≤ b +def uint64.to_nat (n : uint64) : nat := n.val.val +def uint64.add (a b : uint64) : uint64 := ⟨a.val + b.val⟩ +def uint64.sub (a b : uint64) : uint64 := ⟨a.val - b.val⟩ +def uint64.mul (a b : uint64) : uint64 := ⟨a.val * b.val⟩ +def uint64.div (a b : uint64) : uint64 := ⟨a.val / b.val⟩ +def uint64.mod (a b : uint64) : uint64 := ⟨a.val % b.val⟩ +def uint64.modn (a : uint64) (n : nat) : uint64 := ⟨a.val %ₙ n⟩ +def uint64.lt (a b : uint64) : Prop := a.val < b.val +def uint64.le (a b : uint64) : Prop := a.val ≤ b.val instance : has_zero uint64 := ⟨uint64.of_nat 0⟩ instance : has_one uint64 := ⟨uint64.of_nat 1⟩ @@ -155,14 +164,17 @@ instance : has_lt uint64 := ⟨uint64.lt⟩ instance : has_le uint64 := ⟨uint64.le⟩ instance : inhabited uint64 := ⟨0⟩ -def uint64.dec_eq : Π (a b : uint64), decidable (a = b) -| ⟨a⟩ ⟨b⟩ := if h : a = b then is_true (h ▸ rfl) else is_false (λ h', uint64.no_confusion h' (λ h', absurd h' h)) +def uint64.dec_eq (a b : uint64) : decidable (a = b) := +uint64.cases_on a $ λ n, uint64.cases_on b $ λ m, + if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint64.no_confusion h' (λ h', absurd h' h)) -def uint64.dec_lt : Π (a b : uint64), decidable (a < b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a < b)) +def uint64.dec_lt (a b : uint64) : decidable (a < b) := +uint64.cases_on a $ λ n, uint64.cases_on b $ λ m, + infer_instance_as (decidable (n < m)) -def uint64.dec_le : Π (a b : uint64), decidable (a ≤ b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a ≤ b)) +def uint64.dec_le (a b : uint64) : decidable (a ≤ b) := +uint64.cases_on a $ λ n, uint64.cases_on b $ λ m, + infer_instance_as (decidable (n <= m)) instance : decidable_eq uint64 := {dec_eq := uint64.dec_eq} instance uint64.has_decidable_lt (a b : uint64) : decidable (a < b) := uint64.dec_lt a b diff --git a/library/init/data/usize.lean b/library/init/data/usize.lean index 605ea85e38..7c0a2490d5 100644 --- a/library/init/data/usize.lean +++ b/library/init/data/usize.lean @@ -11,15 +11,15 @@ structure usize := (val : fin usize_sz) def usize.of_nat (n : nat) : usize := ⟨fin.of_nat n⟩ -def usize.to_nat : usize → nat | ⟨a⟩ := a.val -def usize.add : usize → usize → usize | ⟨a⟩ ⟨b⟩ := ⟨a + b⟩ -def usize.sub : usize → usize → usize | ⟨a⟩ ⟨b⟩ := ⟨a - b⟩ -def usize.mul : usize → usize → usize | ⟨a⟩ ⟨b⟩ := ⟨a * b⟩ -def usize.div : usize → usize → usize | ⟨a⟩ ⟨b⟩ := ⟨a / b⟩ -def usize.mod : usize → usize → usize | ⟨a⟩ ⟨b⟩ := ⟨a % b⟩ -def usize.modn : usize → nat → usize | ⟨a⟩ b := ⟨a %ₙ b⟩ -def usize.lt : usize → usize → Prop | ⟨a⟩ ⟨b⟩ := a < b -def usize.le : usize → usize → Prop | ⟨a⟩ ⟨b⟩ := a ≤ b +def usize.to_nat (n : usize) : nat := n.val.val +def usize.add (a b : usize) : usize := ⟨a.val + b.val⟩ +def usize.sub (a b : usize) : usize := ⟨a.val - b.val⟩ +def usize.mul (a b : usize) : usize := ⟨a.val * b.val⟩ +def usize.div (a b : usize) : usize := ⟨a.val / b.val⟩ +def usize.mod (a b : usize) : usize := ⟨a.val % b.val⟩ +def usize.modn (a : usize) (n : nat) : usize := ⟨a.val %ₙ n⟩ +def usize.lt (a b : usize) : Prop := a.val < b.val +def usize.le (a b : usize) : Prop := a.val ≤ b.val instance : has_zero usize := ⟨usize.of_nat 0⟩ instance : has_one usize := ⟨usize.of_nat 1⟩ @@ -33,14 +33,17 @@ instance : has_lt usize := ⟨usize.lt⟩ instance : has_le usize := ⟨usize.le⟩ instance : inhabited usize := ⟨0⟩ -def usize.dec_eq : Π (a b : usize), decidable (a = b) -| ⟨a⟩ ⟨b⟩ := if h : a = b then is_true (h ▸ rfl) else is_false (λ h', usize.no_confusion h' (λ h', absurd h' h)) +def usize.dec_eq (a b : usize) : decidable (a = b) := +usize.cases_on a $ λ n, usize.cases_on b $ λ m, + if h : n = m then is_true (h ▸ rfl) else is_false (λ h', usize.no_confusion h' (λ h', absurd h' h)) -def usize.dec_lt : Π (a b : usize), decidable (a < b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a < b)) +def usize.dec_lt (a b : usize) : decidable (a < b) := +usize.cases_on a $ λ n, usize.cases_on b $ λ m, + infer_instance_as (decidable (n < m)) -def usize.dec_le : Π (a b : usize), decidable (a ≤ b) -| ⟨a⟩ ⟨b⟩ := infer_instance_as (decidable (a ≤ b)) +def usize.dec_le (a b : usize) : decidable (a ≤ b) := +usize.cases_on a $ λ n, usize.cases_on b $ λ m, + infer_instance_as (decidable (n <= m)) instance : decidable_eq usize := {dec_eq := usize.dec_eq} instance usize.has_decidable_lt (a b : usize) : decidable (a < b) := usize.dec_lt a b diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp index 56c1ccfb88..608d2db3a6 100644 --- a/src/library/compiler/builtin.cpp +++ b/src/library/compiler/builtin.cpp @@ -91,14 +91,55 @@ void initialize_builtin() { 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_u32_o = mk_arrow(o, mk_arrow(u32, o)); - expr o_u32 = mk_arrow(o, u32); + 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_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 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 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 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); + list b{true}; list bb{true, true}; list c{false}; @@ -174,6 +215,71 @@ void initialize_builtin() { register_builtin(name({"lean", "environment", "empty"}), o, "lean_environment_empty"); register_builtin(name({"lean", "environment", "contains"}), o_o_o, "lean_environment_contains"); register_builtin(name({"lean", "elaborator", "elaborate_command"}), o_o_o_o, "lean_elaborator_elaborate_command"); + + /* uint8 builtin functions */ + register_builtin(name({"uint8", "of_nat"}), o_u8, "lean::uint8_of_nat", b); + register_builtin(name({"uint8", "to_nat"}), u8_o, "lean::uint8_to_nat"); + register_builtin(name({"uint8", "add"}), u8_u8_u8, "lean::uint8_add"); + register_builtin(name({"uint8", "sub"}), u8_u8_u8, "lean::uint8_sub"); + register_builtin(name({"uint8", "mul"}), u8_u8_u8, "lean::uint8_mul"); + register_builtin(name({"uint8", "div"}), u8_u8_u8, "lean::uint8_div"); + register_builtin(name({"uint8", "mod"}), u8_u8_u8, "lean::uint8_mod"); + register_builtin(name({"uint8", "modn"}), u8_o_u8, "lean::uint8_modn", cb); + register_builtin(name({"uint8", "dec_eq"}), u8_u8_o, "lean::uint8_dec_eq"); + register_builtin(name({"uint8", "dec_lt"}), u8_u8_o, "lean::uint8_dec_lt"); + register_builtin(name({"uint8", "dec_le"}), u8_u8_o, "lean::uint8_dec_le"); + + /* uint16 builtin functions */ + register_builtin(name({"uint16", "of_nat"}), o_u16, "lean::uint16_of_nat", b); + register_builtin(name({"uint16", "to_nat"}), u16_o, "lean::uint16_to_nat"); + register_builtin(name({"uint16", "add"}), u16_u16_u16, "lean::uint16_add"); + register_builtin(name({"uint16", "sub"}), u16_u16_u16, "lean::uint16_sub"); + register_builtin(name({"uint16", "mul"}), u16_u16_u16, "lean::uint16_mul"); + register_builtin(name({"uint16", "div"}), u16_u16_u16, "lean::uint16_div"); + register_builtin(name({"uint16", "mod"}), u16_u16_u16, "lean::uint16_mod"); + register_builtin(name({"uint16", "modn"}), u16_o_u16, "lean::uint16_modn", cb); + register_builtin(name({"uint16", "dec_eq"}), u16_u16_o, "lean::uint16_dec_eq"); + register_builtin(name({"uint16", "dec_lt"}), u16_u16_o, "lean::uint16_dec_lt"); + register_builtin(name({"uint16", "dec_le"}), u16_u16_o, "lean::uint16_dec_le"); + + /* uint32 builtin functions */ + register_builtin(name({"uint32", "of_nat"}), o_u32, "lean::uint32_of_nat", b); + register_builtin(name({"uint32", "to_nat"}), u32_o, "lean::uint32_to_nat"); + register_builtin(name({"uint32", "add"}), u32_u32_u32, "lean::uint32_add"); + register_builtin(name({"uint32", "sub"}), u32_u32_u32, "lean::uint32_sub"); + register_builtin(name({"uint32", "mul"}), u32_u32_u32, "lean::uint32_mul"); + register_builtin(name({"uint32", "div"}), u32_u32_u32, "lean::uint32_div"); + register_builtin(name({"uint32", "mod"}), u32_u32_u32, "lean::uint32_mod"); + register_builtin(name({"uint32", "modn"}), u32_o_u32, "lean::uint32_modn", cb); + register_builtin(name({"uint32", "dec_eq"}), u32_u32_o, "lean::uint32_dec_eq"); + register_builtin(name({"uint32", "dec_lt"}), u32_u32_o, "lean::uint32_dec_lt"); + register_builtin(name({"uint32", "dec_le"}), u32_u32_o, "lean::uint32_dec_le"); + + /* uint64 builtin functions */ + register_builtin(name({"uint64", "of_nat"}), o_u64, "lean::uint64_of_nat", b); + register_builtin(name({"uint64", "to_nat"}), u64_o, "lean::uint64_to_nat"); + register_builtin(name({"uint64", "add"}), u64_u64_u64, "lean::uint64_add"); + register_builtin(name({"uint64", "sub"}), u64_u64_u64, "lean::uint64_sub"); + register_builtin(name({"uint64", "mul"}), u64_u64_u64, "lean::uint64_mul"); + register_builtin(name({"uint64", "div"}), u64_u64_u64, "lean::uint64_div"); + register_builtin(name({"uint64", "mod"}), u64_u64_u64, "lean::uint64_mod"); + register_builtin(name({"uint64", "modn"}), u64_o_u64, "lean::uint64_modn", cb); + register_builtin(name({"uint64", "dec_eq"}), u64_u64_o, "lean::uint64_dec_eq"); + register_builtin(name({"uint64", "dec_lt"}), u64_u64_o, "lean::uint64_dec_lt"); + register_builtin(name({"uint64", "dec_le"}), u64_u64_o, "lean::uint64_dec_le"); + + /* usize builtin functions */ + register_builtin(name({"usize", "of_nat"}), o_us, "lean::usize_of_nat", b); + register_builtin(name({"usize", "to_nat"}), us_o, "lean::usize_to_nat"); + register_builtin(name({"usize", "add"}), us_us_us, "lean::usize_add"); + register_builtin(name({"usize", "sub"}), us_us_us, "lean::usize_sub"); + register_builtin(name({"usize", "mul"}), us_us_us, "lean::usize_mul"); + register_builtin(name({"usize", "div"}), us_us_us, "lean::usize_div"); + register_builtin(name({"usize", "mod"}), us_us_us, "lean::usize_mod"); + register_builtin(name({"usize", "modn"}), us_o_us, "lean::usize_modn", cb); + register_builtin(name({"usize", "dec_eq"}), us_us_o, "lean::usize_dec_eq"); + register_builtin(name({"usize", "dec_lt"}), us_us_o, "lean::usize_dec_lt"); + register_builtin(name({"usize", "dec_le"}), us_us_o, "lean::usize_dec_le"); } void finalize_builtin() { diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 5b2b869445..aab92fb7b8 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp - vm_int.cpp init_module.cpp) + vm_int.cpp vm_uint.cpp init_module.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 698ef2aa3e..84ecc2526e 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "library/vm/vm.h" #include "library/vm/vm_nat.h" #include "library/vm/vm_int.h" +#include "library/vm/vm_uint.h" #include "library/vm/vm_aux.h" #include "library/vm/vm_io.h" #include "library/vm/vm_string.h" @@ -19,9 +20,11 @@ void initialize_vm_core_module() { initialize_vm_aux(); initialize_vm_io(); initialize_vm_string(); + initialize_vm_uint(); } void finalize_vm_core_module() { + finalize_vm_uint(); finalize_vm_string(); finalize_vm_io(); finalize_vm_aux(); diff --git a/src/library/vm/vm_uint.cpp b/src/library/vm/vm_uint.cpp new file mode 100644 index 0000000000..d9f3264854 --- /dev/null +++ b/src/library/vm/vm_uint.cpp @@ -0,0 +1,81 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/vm/vm.h" +namespace lean { +vm_obj dummy_unary_op(vm_obj const &, vm_obj const &) { + throw exception("uint support has not been implemented in the old VM"); +} + +vm_obj dummy_binary_op(vm_obj const &, vm_obj const &) { + throw exception("uint support has not been implemented in the old VM"); +} + +void initialize_vm_uint() { + DECLARE_VM_BUILTIN(name({"uint8", "of_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint8", "to_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint8", "add"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "sub"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "mul"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "div"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "mod"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "modn"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "dec_eq"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "dec_lt"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint8", "dec_le"}), dummy_binary_op); + + DECLARE_VM_BUILTIN(name({"uint16", "of_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint16", "to_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint16", "add"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "sub"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "mul"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "div"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "mod"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "modn"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "dec_eq"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "dec_lt"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint16", "dec_le"}), dummy_binary_op); + + DECLARE_VM_BUILTIN(name({"uint32", "of_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint32", "to_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint32", "add"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "sub"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "mul"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "div"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "mod"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "modn"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "dec_eq"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "dec_lt"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint32", "dec_le"}), dummy_binary_op); + + DECLARE_VM_BUILTIN(name({"uint64", "of_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint64", "to_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"uint64", "add"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "sub"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "mul"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "div"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "mod"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "modn"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "dec_eq"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "dec_lt"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"uint64", "dec_le"}), dummy_binary_op); + + DECLARE_VM_BUILTIN(name({"usize", "of_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"usize", "to_nat"}), dummy_unary_op); + DECLARE_VM_BUILTIN(name({"usize", "add"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "sub"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "mul"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "div"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "mod"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "modn"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "dec_eq"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "dec_lt"}), dummy_binary_op); + DECLARE_VM_BUILTIN(name({"usize", "dec_le"}), dummy_binary_op); +} + +void finalize_vm_uint() { +} +} diff --git a/src/library/vm/vm_uint.h b/src/library/vm/vm_uint.h new file mode 100644 index 0000000000..46b4a28ed1 --- /dev/null +++ b/src/library/vm/vm_uint.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +void initialize_vm_uint(); +void finalize_vm_uint(); +} diff --git a/src/runtime/object.h b/src/runtime/object.h index ed4c5a120e..01456bae24 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -21,6 +21,7 @@ typedef unsigned char uint8; typedef unsigned short uint16; typedef unsigned uint32; typedef unsigned long long uint64; +typedef size_t usize; /* The primitives implemented in the runtime do not modify the RC of its arguments. @@ -1118,4 +1119,146 @@ bool string_eq(b_obj_arg s1, char const * s2); bool string_lt(b_obj_arg s1, b_obj_arg s2); inline obj_res string_dec_eq(b_obj_arg s1, b_obj_arg s2) { return box(string_eq(s1, s2)); } inline obj_res string_dec_lt(b_obj_arg s1, b_obj_arg s2) { return box(string_lt(s1, s2)); } + +// ======================================= +// uint8 +inline uint8 uint8_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast(unbox(a)) : 0; } +inline obj_res uint8_to_nat(uint8 a) { return mk_nat_obj(static_cast(a)); } +inline uint8 uint8_add(uint8 a1, uint8 a2) { return a1+a2; } +inline uint8 uint8_sub(uint8 a1, uint8 a2) { return a1-a2; } +inline uint8 uint8_mul(uint8 a1, uint8 a2) { return a1*a2; } +inline uint8 uint8_div(uint8 a1, uint8 a2) { return a2 == 0 ? 0 : a1/a2; } +inline uint8 uint8_mod(uint8 a1, uint8 a2) { return a2 == 0 ? 0 : a1%a2; } +inline uint8 uint8_modn(uint8 a1, b_obj_arg a2) { + if (LEAN_LIKELY(is_scalar(a2))) { + unsigned n2 = unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return a1; + } +} +inline obj_res uint8_dec_eq(uint8 a1, uint8 a2) { return box(a1 == a2); } +inline obj_res uint8_dec_lt(uint8 a1, uint8 a2) { return box(a1 < a2); } +inline obj_res uint8_dec_le(uint8 a1, uint8 a2) { return box(a1 <= a2); } + +// ======================================= +// uint16 +inline uint16 uint16_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast(unbox(a)) : 0; } +inline obj_res uint16_to_nat(uint16 a) { return mk_nat_obj(static_cast(a)); } +inline uint16 uint16_add(uint16 a1, uint16 a2) { return a1+a2; } +inline uint16 uint16_sub(uint16 a1, uint16 a2) { return a1-a2; } +inline uint16 uint16_mul(uint16 a1, uint16 a2) { return a1*a2; } +inline uint16 uint16_div(uint16 a1, uint16 a2) { return a2 == 0 ? 0 : a1/a2; } +inline uint16 uint16_mod(uint16 a1, uint16 a2) { return a2 == 0 ? 0 : a1%a2; } +inline uint16 uint16_modn(uint16 a1, b_obj_arg a2) { + if (LEAN_LIKELY(is_scalar(a2))) { + unsigned n2 = unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return a1; + } +} +inline obj_res uint16_dec_eq(uint16 a1, uint16 a2) { return box(a1 == a2); } +inline obj_res uint16_dec_lt(uint16 a1, uint16 a2) { return box(a1 < a2); } +inline obj_res uint16_dec_le(uint16 a1, uint16 a2) { return box(a1 <= a2); } + +// ======================================= +// uint32 +inline uint32 uint32_of_nat(b_obj_arg a) { + if (is_scalar(a)) { + return unbox(a); + } else if (sizeof(void*) == 4) { + // 32-bit + mpz const & m = mpz_value(a); + return m.is_unsigned_int() ? mpz_value(a).get_unsigned_int() : 0; + } else { + // 64-bit + return 0; + } +} +inline obj_res uint32_to_nat(uint32 a) { return mk_nat_obj(a); } +inline uint32 uint32_add(uint32 a1, uint32 a2) { return a1+a2; } +inline uint32 uint32_sub(uint32 a1, uint32 a2) { return a1-a2; } +inline uint32 uint32_mul(uint32 a1, uint32 a2) { return a1*a2; } +inline uint32 uint32_div(uint32 a1, uint32 a2) { return a2 == 0 ? 0 : a1/a2; } +inline uint32 uint32_mod(uint32 a1, uint32 a2) { return a2 == 0 ? 0 : a1%a2; } +inline uint32 uint32_modn(uint32 a1, b_obj_arg a2) { + if (LEAN_LIKELY(is_scalar(a2))) { + unsigned n2 = unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else if (sizeof(void*) == 4) { + // 32-bit + mpz const & m = mpz_value(a2); + return m.is_unsigned_int() ? a1 % m.get_unsigned_int() : a1; + } else { + // 64-bit + return a1; + } +} +inline obj_res uint32_dec_eq(uint32 a1, uint32 a2) { return box(a1 == a2); } +inline obj_res uint32_dec_lt(uint32 a1, uint32 a2) { return box(a1 < a2); } +inline obj_res uint32_dec_le(uint32 a1, uint32 a2) { return box(a1 <= a2); } + +// ======================================= +// uint64 +inline uint64 uint64_of_nat(b_obj_arg a) { + if (is_scalar(a)) { + return unbox(a); + } else { + // TODO(Leo): + return 0; + } +} +inline obj_res uint64_to_nat(uint64 a) { return mk_nat_obj(a); } +inline uint64 uint64_add(uint64 a1, uint64 a2) { return a1+a2; } +inline uint64 uint64_sub(uint64 a1, uint64 a2) { return a1-a2; } +inline uint64 uint64_mul(uint64 a1, uint64 a2) { return a1*a2; } +inline uint64 uint64_div(uint64 a1, uint64 a2) { return a2 == 0 ? 0 : a1/a2; } +inline uint64 uint64_mod(uint64 a1, uint64 a2) { return a2 == 0 ? 0 : a1%a2; } +inline uint64 uint64_modn(uint64 a1, b_obj_arg a2) { + if (LEAN_LIKELY(is_scalar(a2))) { + unsigned n2 = unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + // TODO(Leo) + return a1; + } +} +inline obj_res uint64_dec_eq(uint64 a1, uint64 a2) { return box(a1 == a2); } +inline obj_res uint64_dec_lt(uint64 a1, uint64 a2) { return box(a1 < a2); } +inline obj_res uint64_dec_le(uint64 a1, uint64 a2) { return box(a1 <= a2); } + +// ======================================= +// usize +inline usize usize_of_nat(b_obj_arg a) { + if (is_scalar(a)) { + return unbox(a); + } else { + // TODO(Leo): + return 0; + } +} +inline obj_res usize_to_nat(usize a) { + if (sizeof(void*) == 4) + return mk_nat_obj(static_cast(a)); + else + return mk_nat_obj(static_cast(a)); +} +inline usize usize_add(usize a1, usize a2) { return a1+a2; } +inline usize usize_sub(usize a1, usize a2) { return a1-a2; } +inline usize usize_mul(usize a1, usize a2) { return a1*a2; } +inline usize usize_div(usize a1, usize a2) { return a2 == 0 ? 0 : a1/a2; } +inline usize usize_mod(usize a1, usize a2) { return a2 == 0 ? 0 : a1%a2; } +inline usize usize_modn(usize a1, b_obj_arg a2) { + if (LEAN_LIKELY(is_scalar(a2))) { + unsigned n2 = unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + // TODO(Leo) + return a1; + } +} +inline obj_res usize_dec_eq(usize a1, usize a2) { return box(a1 == a2); } +inline obj_res usize_dec_lt(usize a1, usize a2) { return box(a1 < a2); } +inline obj_res usize_dec_le(usize a1, usize a2) { return box(a1 <= a2); } }