Adding features

lib/arith.sail

@@ -51,26 +51,27 @@ $include <flow.sail>
 
 // ***** Addition *****
 
-val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : forall 'n 'm.
+val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 
-val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add",  _: "add_int"} : (int, int) -> int
+val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd",  _: "add_int"} : (int, int) -> int
 
 overload operator + = {add_atom, add_int}
 
 // ***** Subtraction *****
 
-val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : forall 'n 'm.
+val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "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: "Int.sub", _: "sub_int"} : (int, int) -> int
+val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "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: "HSub.hSub",
   _: "sub_nat"
 } : (nat, nat) -> nat
 

src/bin/dune

@@ -242,4 +242,10 @@
    src/gen_lib/sail2_values.lem)
   (%{workspace_root}/src/sail_lean_backend/Sail/sail.lean
    as
-   src/sail_lean_backend/Sail/sail.lean)))
+   src/sail_lean_backend/Sail/sail.lean)
+   (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean
+   as
+   src/sail_lean_backend/Sail/bitvec.lean)
+   (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean
+   as
+   src/sail_lean_backend/Sail/registers.lean)))

src/sail_lean_backend/Sail/bitvec.lean

@@ -0,0 +1,25 @@
+namespace Sail
+namespace BitVec
+
+def length {w: Nat} (_: BitVec w): Nat := w
+
+def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.signExtend w'
+
+def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.zeroExtend w'
+
+def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.truncate w'
+
+def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.extractLsb' 0 w'
+
+def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
+  x.extractLsb hi lo
+
+def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
+  sorry
+
+end BitVec
+end Sail

src/sail_lean_backend/Sail/registers.lean

@@ -0,0 +1,29 @@
+
+inductive register where
+  | Register : String → /- name -/
+               Nat → /- length -/
+               Nat → /- start index -/
+               Bool → /- is increasing -/
+               List register_field_index
+               → register
+  | UndefinedRegister : Nat → register /- length -/
+  | RegisterPair : register → register → register
+
+structure register_ref (regstate regval a: Type) where
+  name: String
+  read_from: regstate -> a
+  write_to: a -> regstate -> regstate
+  of_regval: regval -> Option a
+  regval_of: a -> regval
+
+def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e :=
+  let k v :=
+    match reg.of_regval v with
+      | some v => some v
+      | none => none
+  Read_reg reg.(name) k.
+
+def reg_deref {s rv a e} := @read_reg s rv a e.
+
+def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e :=
+ Write_reg reg.(name) (reg.(regval_of) v) (Done tt).

src/sail_lean_backend/Sail/sail.lean

@@ -1,25 +1,2 @@
-namespace Sail
-namespace BitVec
-
-def length {w: Nat} (_: BitVec w): Nat := w
-
-def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.signExtend w'
-
-def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.zeroExtend w'
-
-def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.truncate w'
-
-def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.extractLsb' 0 w'
-
-def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
-  x.extractLsb hi lo
-
-def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
-  sorry
-
-end BitVec
-end Sail
+import Sail.bitvec
+import Sail.registers