First batch of features

lib/vector.sail

@@ -289,6 +289,7 @@ val subrange_bits = pure {
   interpreter: "subrange",
   lem: "subrange_vec_dec",
   coq: "subrange_vec_dec",
+  lean: "Sail.BitVec.extractLsb",
   _: "vector_subrange"
 } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
   (bits('n), int('m), int('o)) -> bits('m - 'o + 1)
@@ -311,6 +312,7 @@ val update_subrange_bits = pure {
   interpreter: "update_subrange",
   lem: "update_subrange_vec_dec",
   coq: "update_subrange_vec_dec",
+  lean: "Sail.BitVec.update_subrange",
   _: "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

@@ -15,5 +15,11 @@ def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec 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/pretty_print_lean.ml

@@ -96,6 +96,7 @@ let string_of_typ_con (Typ_aux (t, _)) =
   | Typ_internal_unknown -> "Typ_internal_unknown"
   | Typ_id _ -> "Typ_id"
 
+
 let rec doc_typ (Typ_aux (t, _) as typ) =
   match t with
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
@@ -104,10 +105,17 @@ let rec doc_typ (Typ_aux (t, _) as typ) =
   | Typ_id (Id_aux (Id "bit", _)) -> parens (string "BitVec 1")
   | Typ_id (Id_aux (Id "nat", _)) -> string "Nat"
   | Typ_app (Id_aux (Id "bitvector", _), [A_aux (A_nexp m, _)]) -> string "BitVec " ^^ doc_nexp m
+  | Typ_app (Id_aux (Id "register", _), t_app) -> string "Register " ^^ separate_map comma doc_typ_app t_app
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) doc_typ ts)
   | Typ_id (Id_aux (Id id, _)) -> string id
   | _ -> failwith ("Type " ^ string_of_typ_con typ ^ " " ^ string_of_typ typ ^ " not translatable yet.")
 
+and doc_typ_app (A_aux (t, _) as typ) =
+  match t with
+  | A_typ t' -> doc_typ t'
+  | A_bool nc -> failwith ("Constraint " ^ string_of_n_constraint nc ^ "not translatable yet.")
+  | A_nexp m -> doc_nexp m
+
 let doc_typ_id (typ, fid) = concat [doc_id_ctor fid; space; colon; space; doc_typ typ; hardline]
 
 let doc_typ_quant tq =
@@ -181,8 +189,8 @@ let rec doc_exp (E_aux (e, (l, annot)) as full_exp) =
   | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *)
   | E_lit l -> doc_lit l
   | E_app (Id_aux (Id "internal_pick", _), _) ->
-      string "sorry" (* TODO replace by actual implementation of internal_pick *)
-  | E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *)
+      string "sorry /- internal_pick -/" (* TODO replace by actual implementation of internal_pick *)
+  | E_internal_plet _ -> string "sorry /- internal_plet -/" (* TODO replace by actual implementation of internal_plet *)
   | E_app (f, args) ->
       let d_id =
         if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") else doc_exp (E_aux (E_id f, (l, annot)))
@@ -200,8 +208,15 @@ let rec doc_exp (E_aux (e, (l, annot)) as full_exp) =
         | _ -> failwith "Let pattern not translatable yet."
       in
       nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp lexp]) ^^ hardline ^^ doc_exp e
+  | E_struct fexps -> let args = List.map doc_fexp fexps in
+    braces (separate comma args)
+  | E_field (exp, id) -> doc_exp exp ^^ dot ^^ doc_id_ctor id
+  | E_struct_update (exp, fexps) -> let args = List.map doc_fexp fexps in
+    braces (doc_exp exp ^^ string " with " ^^ separate comma args)
   | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")
 
+and doc_fexp (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp exp
+
 let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) =
   let env = env_of_tannot (snd annot) in
   let TypQ_aux (tq, l), typ = Env.get_val_spec_orig id env in

test/lean/bitfield.lean.expected

@@ -0,0 +1,69 @@
+import Sail.sail
+
+structure cr_type  where
+  bits : BitVec 8
+
+
+def undefined_cr_type (lit : Unit) : cr_type :=
+  sorry
+
+def Mk_cr_type (v : BitVec 8) : cr_type :=
+  {bits := v}
+
+def _get_cr_type_bits (v : cr_type) : BitVec 8 :=
+  (Sail.BitVec.extractLsb v.bits (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 _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit :=
+  sorry
+
+def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
+  (Sail.BitVec.extractLsb v.bits 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 _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit :=
+  sorry
+
+def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
+  (Sail.BitVec.extractLsb v.bits 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 _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit :=
+  sorry
+
+def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
+  (Sail.BitVec.extractLsb v.bits 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 _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit :=
+  sorry
+
+def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
+  (Sail.BitVec.extractLsb v.bits 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 _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit :=
+  sorry
+
+def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
+  (Sail.BitVec.extractLsb v.bits 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 _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit :=
+  sorry
+
+def initialize_registers : Unit :=
+  ()
+

test/lean/bitfield.sail

@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+bitfield cr_type : bits(8) = {
+  CR0 : 7 .. 4,
+  LT  : 7,
+  GT  : 6,
+  CR1 : 3 .. 2,
+  CR3 : 1 .. 0
+}