feat(*): builtin support for uint functions
@kha The VM versions just throw exceptions. They are just stubs to make sure we can compile Lean. I implemented the uint functions in the new runtime, but there are a few missing cases marked with TODO. I needed these builtins to be able to compile the C++ generated code for corelib.
This commit is contained in:
Leonardo de Moura
parent
54f501594d
commit
0918a599ae
8 changed files with 438 additions and 79 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<bool> b{true};
|
||||
list<bool> bb{true, true};
|
||||
list<bool> 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() {
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
81
src/library/vm/vm_uint.cpp
Normal file
81
src/library/vm/vm_uint.cpp
Normal file
|
|
@ -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() {
|
||||
}
|
||||
}
|
||||
11
src/library/vm/vm_uint.h
Normal file
11
src/library/vm/vm_uint.h
Normal file
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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<uint8>(unbox(a)) : 0; }
|
||||
inline obj_res uint8_to_nat(uint8 a) { return mk_nat_obj(static_cast<unsigned>(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<uint16>(unbox(a)) : 0; }
|
||||
inline obj_res uint16_to_nat(uint16 a) { return mk_nat_obj(static_cast<unsigned>(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<unsigned>(a));
|
||||
else
|
||||
return mk_nat_obj(static_cast<uint64>(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); }
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue