feat: un-inline float intrinsics into runtime. (#694)
* outline all intrinsics into the runtime. This is necessary to support backends such as LLVM which do not emit C. * fix style
This commit is contained in:
Siddharth
GitHub
parent
4cc9072ec3
commit
da4ad465d0
4 changed files with 180 additions and 100 deletions
|
|
@ -32,11 +32,11 @@ structure Float where
|
|||
instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
|
||||
|
||||
@[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float
|
||||
@[extern c inline "#1 + #2"] constant Float.add : Float → Float → Float
|
||||
@[extern c inline "#1 - #2"] constant Float.sub : Float → Float → Float
|
||||
@[extern c inline "#1 * #2"] constant Float.mul : Float → Float → Float
|
||||
@[extern c inline "#1 / #2"] constant Float.div : Float → Float → Float
|
||||
@[extern c inline "(- #1)"] constant Float.neg : Float → Float
|
||||
@[extern "lean_float_add"] constant Float.add : Float → Float → Float
|
||||
@[extern "lean_float_sub"] constant Float.sub : Float → Float → Float
|
||||
@[extern "lean_float_mul"] constant Float.mul : Float → Float → Float
|
||||
@[extern "lean_float_div"] constant Float.div : Float → Float → Float
|
||||
@[extern "lean_float_negate"] constant Float.neg : Float → Float
|
||||
|
||||
def Float.ofInt : Int → Float
|
||||
| Int.ofNat n => Float.ofNat n
|
||||
|
|
@ -59,15 +59,15 @@ instance : Neg Float := ⟨Float.neg⟩
|
|||
instance : LT Float := ⟨Float.lt⟩
|
||||
instance : LE Float := ⟨Float.le⟩
|
||||
|
||||
@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool
|
||||
@[extern "lean_float_beq"] constant Float.beq (a b : Float) : Bool
|
||||
|
||||
instance : BEq Float := ⟨Float.beq⟩
|
||||
|
||||
@[extern c inline "#1 < #2"] constant Float.decLt (a b : Float) : Decidable (a < b) :=
|
||||
@[extern "lean_float_decLt"] constant Float.decLt (a b : Float) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
|
||||
|
||||
@[extern c inline "#1 <= #2"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
|
||||
@[extern "lean_float_decLe"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
|
||||
|
||||
|
|
@ -76,11 +76,11 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
|
|||
|
||||
@[extern "lean_float_to_string"] constant Float.toString : Float → String
|
||||
|
||||
@[extern c inline "(uint8_t)#1"] constant Float.toUInt8 : Float → UInt8
|
||||
@[extern c inline "(uint16_t)#1"] constant Float.toUInt16 : Float → UInt16
|
||||
@[extern c inline "(uint32_t)#1"] constant Float.toUInt32 : Float → UInt32
|
||||
@[extern c inline "(uint64_t)#1"] constant Float.toUInt64 : Float → UInt64
|
||||
@[extern c inline "(size_t)#1"] constant Float.toUSize : Float → USize
|
||||
@[extern "lean_float_to_uint8"] constant Float.toUInt8 : Float → UInt8
|
||||
@[extern "lean_float_to_uint16"] constant Float.toUInt16 : Float → UInt16
|
||||
@[extern "lean_float_to_uint32"] constant Float.toUInt32 : Float → UInt32
|
||||
@[extern "lean_float_to_uint64"] constant Float.toUInt64 : Float → UInt64
|
||||
@[extern "lean_float_to_usize"] constant Float.toUSize : Float → USize
|
||||
|
||||
instance : ToString Float where
|
||||
toString := Float.toString
|
||||
|
|
|
|||
|
|
@ -14,27 +14,27 @@ def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
|
|||
abbrev Nat.toUInt8 := UInt8.ofNat
|
||||
@[extern "lean_uint8_to_nat"]
|
||||
def UInt8.toNat (n : UInt8) : Nat := n.val.val
|
||||
@[extern c inline "#1 + #2"]
|
||||
@[extern "lean_uint8_add"]
|
||||
def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
|
||||
@[extern c inline "#1 - #2"]
|
||||
@[extern "lean_uint8_sub"]
|
||||
def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
|
||||
@[extern c inline "#1 * #2"]
|
||||
@[extern "lean_uint8_mul"]
|
||||
def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
|
||||
@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
|
||||
@[extern "lean_uint8_div"]
|
||||
def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
|
||||
@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
|
||||
@[extern "lean_uint8_mod"]
|
||||
def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint8_modn"]
|
||||
def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨a.val % n⟩
|
||||
@[extern c inline "#1 & #2"]
|
||||
@[extern "lean_uint8_land"]
|
||||
def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
|
||||
@[extern c inline "#1 | #2"]
|
||||
@[extern "lean_uint8_lor"]
|
||||
def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
|
||||
@[extern c inline "#1 ^ #2"]
|
||||
@[extern "lean_uint8_xor"]
|
||||
def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
|
||||
@[extern c inline "#1 << #2 % 8"]
|
||||
@[extern "lean_uint8_shift_left"]
|
||||
def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
|
||||
@[extern c inline "#1 >> #2 % 8"]
|
||||
@[extern "lean_uint8_shift_right"]
|
||||
def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
|
||||
def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
|
||||
def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
|
||||
|
|
@ -49,7 +49,7 @@ instance : Div UInt8 := ⟨UInt8.div⟩
|
|||
instance : LT UInt8 := ⟨UInt8.lt⟩
|
||||
instance : LE UInt8 := ⟨UInt8.le⟩
|
||||
|
||||
@[extern c inline "~ #1"]
|
||||
@[extern "lean_uint8_complement"]
|
||||
def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
|
||||
|
||||
instance : Complement UInt8 := ⟨UInt8.complement⟩
|
||||
|
|
@ -60,13 +60,13 @@ instance : ShiftLeft UInt8 := ⟨UInt8.shiftLeft⟩
|
|||
instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
@[extern "lean_uint8_dec_lt"]
|
||||
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
@[extern "lean_uint8_dec_le"]
|
||||
def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
|
@ -79,31 +79,31 @@ def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
|
|||
abbrev Nat.toUInt16 := UInt16.ofNat
|
||||
@[extern "lean_uint16_to_nat"]
|
||||
def UInt16.toNat (n : UInt16) : Nat := n.val.val
|
||||
@[extern c inline "#1 + #2"]
|
||||
@[extern "lean_uint16_add"]
|
||||
def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
|
||||
@[extern c inline "#1 - #2"]
|
||||
@[extern "lean_uint16_sub"]
|
||||
def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
|
||||
@[extern c inline "#1 * #2"]
|
||||
@[extern "lean_uint16_mul"]
|
||||
def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
|
||||
@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
|
||||
@[extern "lean_uint16_div"]
|
||||
def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
|
||||
@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
|
||||
@[extern "lean_uint16_mod"]
|
||||
def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint16_modn"]
|
||||
def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨a.val % n⟩
|
||||
@[extern c inline "#1 & #2"]
|
||||
@[extern "lean_uint16_land"]
|
||||
def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
|
||||
@[extern c inline "#1 | #2"]
|
||||
@[extern "lean_uint16_lor"]
|
||||
def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
|
||||
@[extern c inline "#1 ^ #2"]
|
||||
@[extern "lean_uint16_xor"]
|
||||
def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
|
||||
@[extern c inline "#1 << #2 % 16"]
|
||||
@[extern "lean_uint16_shift_left"]
|
||||
def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
|
||||
@[extern c inline "((uint8_t)#1)"]
|
||||
@[extern "lean_uint16_to_uint8"]
|
||||
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
|
||||
@[extern c inline "((uint16_t)#1)"]
|
||||
@[extern "lean_uint8_to_uint16"]
|
||||
def UInt8.toUInt16 (a : UInt8) : UInt16 := a.toNat.toUInt16
|
||||
@[extern c inline "#1 >> #2 % 16"]
|
||||
@[extern "lean_uint16_shift_right"]
|
||||
def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
|
||||
def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
|
||||
def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
|
||||
|
|
@ -119,7 +119,7 @@ instance : Div UInt16 := ⟨UInt16.div⟩
|
|||
instance : LT UInt16 := ⟨UInt16.lt⟩
|
||||
instance : LE UInt16 := ⟨UInt16.le⟩
|
||||
|
||||
@[extern c inline "~ #1"]
|
||||
@[extern "lean_uint16_complement"]
|
||||
def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
|
||||
|
||||
instance : Complement UInt16 := ⟨UInt16.complement⟩
|
||||
|
|
@ -130,13 +130,13 @@ instance : ShiftLeft UInt16 := ⟨UInt16.shiftLeft⟩
|
|||
instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
@[extern "lean_uint16_dec_lt"]
|
||||
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
@[extern "lean_uint16_dec_le"]
|
||||
def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
|
@ -149,35 +149,35 @@ def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
|
|||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
|
||||
abbrev Nat.toUInt32 := UInt32.ofNat
|
||||
@[extern c inline "#1 + #2"]
|
||||
@[extern "lean_uint32_add"]
|
||||
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
|
||||
@[extern c inline "#1 - #2"]
|
||||
@[extern "lean_uint32_sub"]
|
||||
def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
|
||||
@[extern c inline "#1 * #2"]
|
||||
@[extern "lean_uint32_mul"]
|
||||
def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
|
||||
@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
|
||||
@[extern "lean_uint32_div"]
|
||||
def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
|
||||
@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
|
||||
@[extern "lean_uint32_mod"]
|
||||
def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint32_modn"]
|
||||
def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨a.val % n⟩
|
||||
@[extern c inline "#1 & #2"]
|
||||
@[extern "lean_uint32_land"]
|
||||
def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
|
||||
@[extern c inline "#1 | #2"]
|
||||
@[extern "lean_uint32_lor"]
|
||||
def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
|
||||
@[extern c inline "#1 ^ #2"]
|
||||
@[extern "lean_uint32_xor"]
|
||||
def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
|
||||
@[extern c inline "#1 << #2 % 32"]
|
||||
@[extern "lean_uint32_shift_left"]
|
||||
def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
|
||||
@[extern c inline "#1 >> #2 % 32"]
|
||||
@[extern "lean_uint32_shift_right"]
|
||||
def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
|
||||
@[extern c inline "((uint8_t)#1)"]
|
||||
@[extern "lean_uint32_to_uint8"]
|
||||
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
|
||||
@[extern c inline "((uint16_t)#1)"]
|
||||
@[extern "lean_uint32_to_uint16"]
|
||||
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
|
||||
@[extern c inline "((uint32_t)#1)"]
|
||||
@[extern "lean_uint8_to_uint32"]
|
||||
def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
|
||||
@[extern c inline "((uint32_t)#1)"]
|
||||
@[extern "lean_uint16_to_uint32"]
|
||||
def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat.toUInt32
|
||||
|
||||
instance : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
|
||||
|
|
@ -188,7 +188,7 @@ instance : Mod UInt32 := ⟨UInt32.mod⟩
|
|||
instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
|
||||
instance : Div UInt32 := ⟨UInt32.div⟩
|
||||
|
||||
@[extern c inline "~ #1"]
|
||||
@[extern "lean_uint32_complement"]
|
||||
def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
|
||||
|
||||
instance : Complement UInt32 := ⟨UInt32.complement⟩
|
||||
|
|
@ -203,41 +203,41 @@ def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
|
|||
abbrev Nat.toUInt64 := UInt64.ofNat
|
||||
@[extern "lean_uint64_to_nat"]
|
||||
def UInt64.toNat (n : UInt64) : Nat := n.val.val
|
||||
@[extern c inline "#1 + #2"]
|
||||
@[extern "lean_uint64_add"]
|
||||
def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
|
||||
@[extern c inline "#1 - #2"]
|
||||
@[extern "lean_uint64_sub"]
|
||||
def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
|
||||
@[extern c inline "#1 * #2"]
|
||||
@[extern "lean_uint64_mul"]
|
||||
def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
|
||||
@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
|
||||
@[extern "lean_uint64_div"]
|
||||
def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
|
||||
@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
|
||||
@[extern "lean_uint64_mod"]
|
||||
def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
|
||||
@[extern "lean_uint64_modn"]
|
||||
def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨a.val % n⟩
|
||||
@[extern c inline "#1 & #2"]
|
||||
@[extern "lean_uint64_land"]
|
||||
def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
|
||||
@[extern c inline "#1 | #2"]
|
||||
@[extern "lean_uint64_lor"]
|
||||
def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
|
||||
@[extern c inline "#1 ^ #2"]
|
||||
@[extern "lean_uint64_xor"]
|
||||
def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
|
||||
@[extern c inline "#1 << #2 % 64"]
|
||||
@[extern "lean_uint64_shift_left"]
|
||||
def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
|
||||
@[extern c inline "#1 >> #2 % 64"]
|
||||
@[extern "lean_uint64_shift_right"]
|
||||
def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
|
||||
def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
|
||||
def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
|
||||
@[extern c inline "((uint8_t)#1)"]
|
||||
@[extern "lean_uint64_to_uint8"]
|
||||
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
|
||||
@[extern c inline "((uint16_t)#1)"]
|
||||
@[extern "lean_uint64_to_uint16"]
|
||||
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
|
||||
@[extern c inline "((uint32_t)#1)"]
|
||||
@[extern "lean_uint64_to_uint32"]
|
||||
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
|
||||
@[extern c inline "((uint64_t)#1)"]
|
||||
@[extern "lean_uint8_to_uint64"]
|
||||
def UInt8.toUInt64 (a : UInt8) : UInt64 := a.toNat.toUInt64
|
||||
@[extern c inline "((uint64_t)#1)"]
|
||||
@[extern "lean_uint16_to_uint64"]
|
||||
def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat.toUInt64
|
||||
@[extern c inline "((uint64_t)#1)"]
|
||||
@[extern "lean_uint32_to_uint64"]
|
||||
def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
|
||||
|
||||
instance : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
|
||||
|
|
@ -250,7 +250,7 @@ instance : Div UInt64 := ⟨UInt64.div⟩
|
|||
instance : LT UInt64 := ⟨UInt64.lt⟩
|
||||
instance : LE UInt64 := ⟨UInt64.le⟩
|
||||
|
||||
@[extern c inline "~ #1"]
|
||||
@[extern "lean_uint64_complement"]
|
||||
def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
|
||||
|
||||
instance : Complement UInt64 := ⟨UInt64.complement⟩
|
||||
|
|
@ -260,17 +260,17 @@ instance : Xor UInt64 := ⟨UInt64.xor⟩
|
|||
instance : ShiftLeft UInt64 := ⟨UInt64.shiftLeft⟩
|
||||
instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
|
||||
|
||||
@[extern c inline "(uint64_t)#1"]
|
||||
@[extern "lean_bool_to_uint64"]
|
||||
def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
@[extern "lean_uint64_dec_lt"]
|
||||
def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
@[extern "lean_uint64_dec_le"]
|
||||
def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
|
@ -286,31 +286,31 @@ def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usize_size_gt_zero⟩
|
|||
abbrev Nat.toUSize := USize.ofNat
|
||||
@[extern "lean_usize_to_nat"]
|
||||
def USize.toNat (n : USize) : Nat := n.val.val
|
||||
@[extern c inline "#1 + #2"]
|
||||
@[extern "lean_usize_add"]
|
||||
def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
|
||||
@[extern c inline "#1 - #2"]
|
||||
@[extern "lean_usize_sub"]
|
||||
def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
|
||||
@[extern c inline "#1 * #2"]
|
||||
@[extern "lean_usize_mul"]
|
||||
def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
|
||||
@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
|
||||
@[extern "lean_usize_div"]
|
||||
def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
|
||||
@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
|
||||
@[extern "lean_usize_mod"]
|
||||
def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
|
||||
@[extern "lean_usize_modn"]
|
||||
def USize.modn (a : USize) (n : @& Nat) : USize := ⟨a.val % n⟩
|
||||
@[extern c inline "#1 & #2"]
|
||||
@[extern "lean_usize_land"]
|
||||
def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
|
||||
@[extern c inline "#1 | #2"]
|
||||
@[extern "lean_usize_lor"]
|
||||
def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
|
||||
@[extern c inline "#1 ^ #2"]
|
||||
@[extern "lean_usize_xor"]
|
||||
def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
|
||||
@[extern c inline "#1 << #2 % (sizeof(size_t) * 8)"]
|
||||
@[extern "lean_usize_shift_left"]
|
||||
def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
|
||||
@[extern c inline "#1 >> #2 % (sizeof(size_t) * 8)"]
|
||||
@[extern "lean_usize_shift_right"]
|
||||
def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
|
||||
@[extern c inline "#1"]
|
||||
@[extern "lean_uint32_to_usize"]
|
||||
def UInt32.toUSize (a : UInt32) : USize := a.toNat.toUSize
|
||||
@[extern c inline "(uint32_t)#1"]
|
||||
@[extern "lean_usize_to_uint32"]
|
||||
def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
|
||||
|
||||
def USize.lt (a b : USize) : Prop := a.val < b.val
|
||||
|
|
@ -326,7 +326,7 @@ instance : Div USize := ⟨USize.div⟩
|
|||
instance : LT USize := ⟨USize.lt⟩
|
||||
instance : LE USize := ⟨USize.le⟩
|
||||
|
||||
@[extern c inline "~ #1"]
|
||||
@[extern "lean_usize_complement"]
|
||||
def USize.complement (a:USize) : USize := 0-(a+1)
|
||||
|
||||
instance : Complement USize := ⟨USize.complement⟩
|
||||
|
|
@ -337,13 +337,13 @@ instance : ShiftLeft USize := ⟨USize.shiftLeft⟩
|
|||
instance : ShiftRight USize := ⟨USize.shiftRight⟩
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
@[extern "lean_usize_dec_lt"]
|
||||
def USize.decLt (a b : USize) : Decidable (a < b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
@[extern "lean_usize_dec_le"]
|
||||
def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
|
|
|||
|
|
@ -811,7 +811,7 @@ def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 := {
|
|||
}
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
@[extern "lean_uint8_dec_eq"]
|
||||
def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
|
|
@ -835,7 +835,7 @@ def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 := {
|
|||
}
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
@[extern "lean_uint16_dec_eq"]
|
||||
def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
|
|
@ -862,7 +862,7 @@ def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 := {
|
|||
def UInt32.toNat (n : UInt32) : Nat := n.val.val
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
@[extern "lean_uint32_dec_eq"]
|
||||
def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
|
|
@ -880,13 +880,13 @@ instance : LE UInt32 where
|
|||
le a b := LE.le a.val b.val
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
@[extern "lean_uint32_dec_lt"]
|
||||
def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
@[extern "lean_uint32_dec_le"]
|
||||
def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
|
||||
|
|
@ -907,7 +907,7 @@ def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 := {
|
|||
}
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
@[extern c "lean_uint64_dec_eq"]
|
||||
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
|
|
@ -938,7 +938,7 @@ def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
|
|||
}
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
@[extern c "lean_usize_dec_eq"]
|
||||
def USize.decEq (a b : USize) : Decidable (Eq a b) :=
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ =>
|
||||
|
|
@ -1644,10 +1644,10 @@ class Hashable (α : Sort u) where
|
|||
|
||||
export Hashable (hash)
|
||||
|
||||
@[extern c inline "(size_t)#1"]
|
||||
@[extern c "lean_uint64_to_usize"]
|
||||
constant UInt64.toUSize (u : UInt64) : USize
|
||||
|
||||
@[extern c inline "(uint64_t)#1"]
|
||||
@[extern c "lean_usize_to_uint64"]
|
||||
constant USize.toUInt64 (u : USize) : UInt64
|
||||
|
||||
@[extern "lean_uint64_mix_hash"]
|
||||
|
|
|
|||
|
|
@ -1476,6 +1476,10 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
|
|||
return lean_int_big_nonneg(a);
|
||||
}
|
||||
|
||||
/* Bool */
|
||||
|
||||
static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
|
||||
|
||||
|
||||
/* UInt8 */
|
||||
|
||||
|
|
@ -1489,6 +1493,12 @@ static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; }
|
|||
static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return a1*a2; }
|
||||
static inline uint8_t lean_uint8_div(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint8_t lean_uint8_mod(uint8_t a1, uint8_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
static inline uint8_t lean_uint8_land(uint8_t a, uint8_t b) { return a & b; }
|
||||
static inline uint8_t lean_uint8_lor(uint8_t a, uint8_t b) { return a | b; }
|
||||
static inline uint8_t lean_uint8_xor(uint8_t a, uint8_t b) { return a ^ b; }
|
||||
static inline uint8_t lean_uint8_shift_left(uint8_t a, uint8_t b) { return a << (b % 8); }
|
||||
static inline uint8_t lean_uint8_shift_right(uint8_t a, uint8_t b) { return a >> (b % 8); }
|
||||
static inline uint8_t lean_uint8_complement(uint8_t a) { return ~a; }
|
||||
static inline uint8_t lean_uint8_modn(uint8_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
unsigned n2 = lean_unbox(a2);
|
||||
|
|
@ -1501,6 +1511,12 @@ static inline uint8_t lean_uint8_dec_eq(uint8_t a1, uint8_t a2) { return a1 == a
|
|||
static inline uint8_t lean_uint8_dec_lt(uint8_t a1, uint8_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a2; }
|
||||
|
||||
|
||||
/* Unit8 -> other */
|
||||
static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
|
||||
static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
|
||||
static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
|
||||
|
||||
/* UInt16 */
|
||||
|
||||
LEAN_SHARED uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
|
||||
|
|
@ -1513,6 +1529,12 @@ static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2;
|
|||
static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; }
|
||||
static inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
static inline uint16_t lean_uint16_land(uint16_t a, uint16_t b) { return a & b; }
|
||||
static inline uint16_t lean_uint16_lor(uint16_t a, uint16_t b) { return a | b; }
|
||||
static inline uint16_t lean_uint16_xor(uint16_t a, uint16_t b) { return a ^ b; }
|
||||
static inline uint16_t lean_uint16_shift_left(uint16_t a, uint16_t b) { return a << (b % 16); }
|
||||
static inline uint16_t lean_uint16_shift_right(uint16_t a, uint16_t b) { return a >> (b % 16); }
|
||||
static inline uint16_t lean_uint16_complement(uint16_t a) { return ~a; }
|
||||
static inline uint16_t lean_uint16_modn(uint16_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
unsigned n2 = lean_unbox(a2);
|
||||
|
|
@ -1525,6 +1547,11 @@ static inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 =
|
|||
static inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; }
|
||||
|
||||
/*uint16 -> other */
|
||||
static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
|
||||
static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
|
||||
static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
|
||||
|
||||
/* UInt32 */
|
||||
|
||||
LEAN_SHARED uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
|
||||
|
|
@ -1537,6 +1564,12 @@ static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2;
|
|||
static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; }
|
||||
static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
static inline uint32_t lean_uint32_land(uint32_t a, uint32_t b) { return a & b; }
|
||||
static inline uint32_t lean_uint32_lor(uint32_t a, uint32_t b) { return a | b; }
|
||||
static inline uint32_t lean_uint32_xor(uint32_t a, uint32_t b) { return a ^ b; }
|
||||
static inline uint32_t lean_uint32_shift_left(uint32_t a, uint32_t b) { return a << (b % 32); }
|
||||
static inline uint32_t lean_uint32_shift_right(uint32_t a, uint32_t b) { return a >> (b % 32); }
|
||||
static inline uint32_t lean_uint32_complement(uint32_t a) { return ~a; }
|
||||
LEAN_SHARED uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
|
||||
static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
|
|
@ -1554,6 +1587,13 @@ static inline uint8_t lean_uint32_dec_eq(uint32_t a1, uint32_t a2) { return a1 =
|
|||
static inline uint8_t lean_uint32_dec_lt(uint32_t a1, uint32_t a2) { return a1 < a2; }
|
||||
static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <= a2; }
|
||||
|
||||
/* uint32 -> other */
|
||||
static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
|
||||
static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
|
||||
static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
|
||||
static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
|
||||
|
||||
|
||||
/* UInt64 */
|
||||
|
||||
LEAN_SHARED uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
|
||||
|
|
@ -1565,6 +1605,12 @@ static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2;
|
|||
static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; }
|
||||
static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
static inline uint64_t lean_uint64_land(uint64_t a, uint64_t b) { return a & b; }
|
||||
static inline uint64_t lean_uint64_lor(uint64_t a, uint64_t b) { return a | b; }
|
||||
static inline uint64_t lean_uint64_xor(uint64_t a, uint64_t b) { return a ^ b; }
|
||||
static inline uint64_t lean_uint64_shift_left(uint64_t a, uint64_t b) { return a << (b % 64); }
|
||||
static inline uint64_t lean_uint64_shift_right(uint64_t a, uint64_t b) { return a >> (b % 64); }
|
||||
static inline uint64_t lean_uint64_complement(uint64_t a) { return ~a; }
|
||||
LEAN_SHARED uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
|
||||
static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
|
|
@ -1579,6 +1625,13 @@ static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 <
|
|||
static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; }
|
||||
LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
|
||||
|
||||
|
||||
/* uint64 -> other */
|
||||
static inline uint8_t lean_uint64_to_uint8(uint64_t a) { return ((uint8_t)a); }
|
||||
static inline uint16_t lean_uint64_to_uint16(uint64_t a) { return ((uint16_t)a); }
|
||||
static inline uint32_t lean_uint64_to_uint32(uint64_t a) { return ((uint32_t)a); }
|
||||
static inline size_t lean_uint64_to_usize(uint64_t a) { return ((size_t)a); }
|
||||
|
||||
/* USize */
|
||||
|
||||
LEAN_SHARED size_t lean_usize_of_big_nat(b_lean_obj_arg a);
|
||||
|
|
@ -1590,6 +1643,12 @@ static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; }
|
|||
static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; }
|
||||
static inline size_t lean_usize_div(size_t a1, size_t a2) { return a2 == 0 ? 0 : a1/a2; }
|
||||
static inline size_t lean_usize_mod(size_t a1, size_t a2) { return a2 == 0 ? a1 : a1%a2; }
|
||||
static inline size_t lean_usize_land(size_t a, size_t b) { return a & b; }
|
||||
static inline size_t lean_usize_lor(size_t a, size_t b) { return a | b; }
|
||||
static inline size_t lean_usize_xor(size_t a, size_t b) { return a ^ b; }
|
||||
static inline size_t lean_usize_shift_left(size_t a, size_t b) { return a << (b % (sizeof(size_t) * 8)); }
|
||||
static inline size_t lean_usize_shift_right(size_t a, size_t b) { return a >> (b % (sizeof(size_t) * 8)); }
|
||||
static inline size_t lean_usize_complement(size_t a) { return ~a; }
|
||||
LEAN_SHARED size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
|
||||
static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
|
||||
if (LEAN_LIKELY(lean_is_scalar(a2))) {
|
||||
|
|
@ -1604,6 +1663,12 @@ static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2;
|
|||
static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
|
||||
LEAN_SHARED size_t lean_usize_mix_hash(size_t a1, size_t a2);
|
||||
|
||||
|
||||
|
||||
/* usize -> other */
|
||||
static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
|
||||
static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
|
||||
|
||||
/* Float */
|
||||
|
||||
LEAN_SHARED double lean_float_of_nat(b_lean_obj_arg a);
|
||||
|
|
@ -1745,6 +1810,21 @@ static inline uint64_t lean_name_hash(b_lean_obj_arg n) {
|
|||
return lean_name_hash_ptr(n);
|
||||
}
|
||||
|
||||
/* float primitives */
|
||||
static inline uint8_t lean_float_to_uint8(double a) { return (uint8_t)a; }
|
||||
static inline uint16_t lean_float_to_uint16(double a) { return (uint16_t)a; }
|
||||
static inline uint32_t lean_float_to_uint32(double a) { return (uint32_t)a; }
|
||||
static inline uint64_t lean_float_to_uint64(double a) { return (uint64_t)a; }
|
||||
static inline size_t lean_float_to_usize(double a) { return (size_t)a; }
|
||||
static inline double lean_float_add(double a, double b) { return a + b; }
|
||||
static inline double lean_float_sub(double a, double b) { return a - b; }
|
||||
static inline double lean_float_mul(double a, double b) { return a * b; }
|
||||
static inline double lean_float_div(double a, double b) { return a / b; }
|
||||
static inline double lean_float_negate(double a) { return -a; }
|
||||
static inline uint8_t lean_float_beq(double a, double b) { return a == b; }
|
||||
static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
|
||||
static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue