Merge branch 'lean-record-features' into lean-register

lib/vector.sail

@@ -322,7 +322,7 @@ val update_subrange_bits = pure {
   interpreter: "update_subrange",
   lem: "update_subrange_vec_dec",
   coq: "update_subrange_vec_dec",
-  lean: "Sail.BitVec.update_subrange",
+  lean: "Sail.BitVec.updateSubrange",
   _: "vector_update_subrange"
 } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n)
 $else

src/sail_lean_backend/Sail/Sail.lean

@@ -19,25 +19,32 @@ def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
 def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.extractLsb' (w - w') w'
 
-def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
+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) (start len: Nat) (y: BitVec len) : BitVec w :=
+def updateSubrange' {w : Nat} (x : BitVec w) (start len : Nat) (y : BitVec len) : BitVec w :=
   let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start)
   let y' := mask ||| ((y.zeroExtend w) <<< start)
   x &&& y'
 
-def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
-  update_subrange' x lo _ y
+def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + 1)) : BitVec w :=
+  updateSubrange' x lo _ y
 
 end BitVec
 end Sail
 
-def undefined_bitvector (n: Nat) : BitVec n :=
-  0#n
+structure RegisterRef (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 undefined_int (lit: Unit) : Int :=
+def undefined_bitvector (w : Nat) : BitVec w :=
   0
 
-def undefined_bit (lit: Unit) : BitVec 1 :=
+def undefined_int (_ : Unit) : Int :=
+  0
+
+def undefined_bit (_ : Unit) : BitVec 1 :=
   undefined_bitvector 1

src/sail_lean_backend/pretty_print_lean.ml

@@ -156,8 +156,8 @@ let rec doc_typ ctxt (Typ_aux (t, _) as typ) =
   | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) ->
       string "Int" (* TODO This probably has to be generalized *)
   | Typ_app (Id_aux (Id "register", _), t_app) ->
-      string "register_ref Unit Unit " (* TODO: Replace units with real types. *)
-      ^^ separate_map comma (doc_typ_app ctxt) t_app
+      string "RegisterRef Unit Unit "
+      (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctxt) t_app
   | Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) ->
       underscore (* TODO check if the type of implicit arguments can really be always inferred *)
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctxt) ts)
@@ -420,11 +420,11 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
       nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e
   | E_struct fexps ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (separate comma args)
+      braces (space ^^ nest 2 (separate hardline args) ^^ space)
   | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor ctxt id
   | E_struct_update (exp, fexps) ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args)
+      braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space)
   | E_assign ((LE_aux (le_act, tannot) as le), e) -> string "set_" ^^ doc_lexp_deref ctxt le ^^ space ^^ doc_exp ctxt e
   | E_internal_return e -> nest 2 (flow (break 1) [string "return"; doc_exp ctxt e])
   | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")

test/lean/bitfield.expected.lean

@@ -1,68 +1,68 @@
 import Out.Sail.Sail
 
-structure cr_type where
-  bits : BitVec 8
+open Sail
 
+def cr_type := (BitVec 8)
 
-def undefined_cr_type (lit : Unit) : cr_type :=
-  sorry
+def undefined_cr_type (lit : Unit) : SailM (BitVec 8) :=
+  return ((undefined_bitvector 8) : (BitVec 8))
 
-def Mk_cr_type (v : BitVec 8) : cr_type :=
-  {bits := v}
+def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) :=
+  v
 
-def _get_cr_type_bits (v : cr_type) : BitVec 8 :=
-  (Sail.BitVec.extractLsb v.bits (HSub.hSub 8 1) 0)
+def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) :=
+  (Sail.BitVec.extractLsb v (HSub.hSub 8 1) 0)
 
-def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)}
+def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x)
 
-def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit :=
-  sorry
+def _set_cr_type_bits (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : SailM Unit :=
+  return sorry
 
-def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
-  (Sail.BitVec.extractLsb v.bits 7 4)
+def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) :=
+  (Sail.BitVec.extractLsb v 7 4)
 
-def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)}
+def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v 7 4 x)
 
-def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit :=
-  sorry
+def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : SailM Unit :=
+  return sorry
 
-def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
-  (Sail.BitVec.extractLsb v.bits 3 2)
+def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) :=
+  (Sail.BitVec.extractLsb v 3 2)
 
-def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)}
+def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v 3 2 x)
 
-def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
-  sorry
+def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit :=
+  return sorry
 
-def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
-  (Sail.BitVec.extractLsb v.bits 1 0)
+def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) :=
+  (Sail.BitVec.extractLsb v 1 0)
 
-def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)}
+def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v 1 0 x)
 
-def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
-  sorry
+def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit :=
+  return sorry
 
-def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
-  (Sail.BitVec.extractLsb v.bits 6 6)
+def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) :=
+  (Sail.BitVec.extractLsb v 6 6)
 
-def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)}
+def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v 6 6 x)
 
-def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
-  sorry
+def _set_cr_type_GT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit :=
+  return sorry
 
-def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
-  (Sail.BitVec.extractLsb v.bits 7 7)
+def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) :=
+  (Sail.BitVec.extractLsb v 7 7)
 
-def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type :=
-  {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)}
+def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
+  (Sail.BitVec.updateSubrange v 7 7 x)
 
-def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
-  sorry
+def _set_cr_type_LT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit :=
+  return sorry
 
 def initialize_registers : Unit :=
   ()

test/lean/struct.expected.lean

@@ -18,6 +18,21 @@ def struct_field2 (s : My_struct) : (BitVec 1) :=
 def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
   {s with field2 := b}
 
+def struct_field2 (s : My_struct) : (BitVec 1) :=
+  s.field2
+
+def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
+  { s with field2 := b }
+
+/-- Type quantifiers: i : Int -/
+def struct_update_both_fields (s : My_struct) (i : Int) (b : (BitVec 1)) : My_struct :=
+  { s with field1 := i, field2 := b }
+
+/-- Type quantifiers: i : Int -/
+def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
+  { field1 := i
+    field2 := b }
+
 def initialize_registers : Unit :=
   ()
 

test/lean/struct.sail

@@ -15,4 +15,17 @@ function struct_field2(s) = {
 val struct_update_field2 : (My_struct, bit) -> My_struct
 function struct_update_field2(s, b) = {
   { s with field2 = b }
+}
+
+val struct_update_both_fields : (My_struct, int, bit) -> My_struct
+function struct_update_both_fields(s, i, b) = {
+  { s with field1 = i, field2 = b }
+}
+
+val mk_struct : (int, bit) -> My_struct
+function mk_struct(i, b) = {
+  struct { 
+    field1 = i,
+    field2 = b
+  }
 }