Skip to content

Commit

Permalink
disable inline notation for subtraction
Browse files Browse the repository at this point in the history
  • Loading branch information
@javra @Alasdair
javra authored and Alasdair committed Feb 27, 2025
1 parent df4102b commit f3f367a
Show file tree
Hide file tree
Showing 27 changed files with 95 additions and 89 deletions.
6 changes: 3 additions & 3 deletions lib/arith.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,18 +60,18 @@ overload operator + = {add_atom, add_int}

// ***** Subtraction *****

val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "_lean_sub", _: "sub_int"} : forall 'n 'm.
val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "_lean_subi", _: "sub_int"} : forall 'n 'm.
(int('n), int('m)) -> int('n - 'm)

val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "_lean_sub", _: "sub_int"} : (int, int) -> int
val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "_lean_subi", _: "sub_int"} : (int, int) -> int

overload operator - = {sub_atom, sub_int}

val sub_nat = pure {
ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
lem: "integerMinus",
coq: "Z.sub",
lean: "_lean_sub",
lean: "_lean_subi",
_: "sub_nat"
} : (nat, nat) -> nat

Expand Down
9 changes: 7 additions & 2 deletions src/sail_lean_backend/Sail/Sail.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,10 @@ def parse_hex_bits (n : Nat) (str : String) : BitVec n :=
def valid_hex_bits (n : Nat) (str : String) : Bool := str.length = n ∧ str.all fun x =>
x.toLower ∈ ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f']

def shift_bits_left (bv : BitVec n) (sh : BitVec m) : BitVec n :=
def shift_bits_left (bv : BitVec n) (sh : BitVec m) : BitVec n :=
bv <<< sh

def shift_bits_right (bv : BitVec n) (sh : BitVec m) : BitVec n :=
def shift_bits_right (bv : BitVec n) (sh : BitVec m) : BitVec n :=
bv >>> sh

def shiftl (bv : BitVec n) (m : Nat) : BitVec n :=
Expand Down Expand Up @@ -543,3 +543,8 @@ instance : HPow Nat Int Nat where

instance : HPow Int Int Int where
hPow x n := x ^ n.toNat

instance : HSub Nat Nat Int where
hSub m n := (m : Int) - (n : Int)

infixl:65 " -i " => HSub.hSub (γ := Int)
1 change: 1 addition & 0 deletions src/sail_lean_backend/pretty_print_lean.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -528,6 +528,7 @@ let op_of_id id =
match id with
| Some "_lean_add" -> `Binop "+"
| Some "_lean_sub" -> `Binop "-"
| Some "_lean_subi" -> `Binop "-i"
| Some "_lean_mul" -> `Binop "*"
| Some "_lean_div" -> `Binop "/"
| Some "_lean_app" -> `Binop "++"
Expand Down
18 changes: 9 additions & 9 deletions test/lean/SailTinyArm.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -616,14 +616,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down Expand Up @@ -652,26 +652,26 @@ def Mk_MAIRType (v : (BitVec 64)) : (BitVec 64) :=
v

def _get_MAIRType_bits (v : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.extractLsb v (64 - 1) 0)
(Sail.BitVec.extractLsb v (64 -i 1) 0)

def _update_MAIRType_bits (v : (BitVec 64)) (x : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.updateSubrange v (64 - 1) 0 x)
(Sail.BitVec.updateSubrange v (64 -i 1) 0 x)

def _update_S1PIRType_bits (v : (BitVec 64)) (x : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.updateSubrange v (64 - 1) 0 x)
(Sail.BitVec.updateSubrange v (64 -i 1) 0 x)

def _update_S2PIRType_bits (v : (BitVec 64)) (x : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.updateSubrange v (64 - 1) 0 x)
(Sail.BitVec.updateSubrange v (64 -i 1) 0 x)

def _set_MAIRType_bits (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 64)) : SailM Unit := do
let r ← do (reg_deref r_ref)
writeRegRef r_ref (_update_MAIRType_bits r v)

def _get_S1PIRType_bits (v : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.extractLsb v (64 - 1) 0)
(Sail.BitVec.extractLsb v (64 -i 1) 0)

def _get_S2PIRType_bits (v : (BitVec 64)) : (BitVec 64) :=
(Sail.BitVec.extractLsb v (64 - 1) 0)
(Sail.BitVec.extractLsb v (64 -i 1) 0)

def _set_S1PIRType_bits (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 64)) : SailM Unit := do
let r ← do (reg_deref r_ref)
Expand Down
6 changes: 3 additions & 3 deletions test/lean/append.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
10 changes: 5 additions & 5 deletions test/lean/bitfield.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,14 +94,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down Expand Up @@ -130,10 +130,10 @@ def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) :=
v

def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) :=
(Sail.BitVec.extractLsb v (8 - 1) 0)
(Sail.BitVec.extractLsb v (8 -i 1) 0)

def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) :=
(Sail.BitVec.updateSubrange v (8 - 1) 0 x)
(Sail.BitVec.updateSubrange v (8 -i 1) 0 x)

def _set_cr_type_bits (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 8)) : SailM Unit := do
let r ← do (reg_deref r_ref)
Expand Down
6 changes: 3 additions & 3 deletions test/lean/bitvec_operation.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/enum.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,14 +87,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/errors.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
10 changes: 5 additions & 5 deletions test/lean/extern.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down Expand Up @@ -169,10 +169,10 @@ def extern_add (_ : Unit) : Int :=
(5 + 4)

def extern_sub (_ : Unit) : Int :=
(5 - (-4))
(5 -i (-4))

def extern_sub_nat (_ : Unit) : Nat :=
(5 - 4)
(5 -i 4)

def extern_negate (_ : Unit) : Int :=
(Neg.neg 5)
Expand Down
6 changes: 3 additions & 3 deletions test/lean/extern_bitvec.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/implicit.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/ite.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,14 +96,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/let.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/loop.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/mapping.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,14 +87,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/match.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,14 +102,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/match_bv.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
6 changes: 3 additions & 3 deletions test/lean/option.expected.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then ((Int.tdiv (n + 1) m) - 1)
then ((Int.tdiv (n + 1) m) -i 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then ((Int.tdiv (n - 1) m) - 1)
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m)

/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n - (m * (fdiv_int n m)))
(n -i (m * (fdiv_int n m)))

/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
Expand Down
Loading

0 comments on commit f3f367a

Please sign in to comment.