From dbf9caafc5642686e390d8ee41b66867b2109929 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Fri, 17 Jan 2025 15:18:31 +0000 Subject: [PATCH 01/23] Working registers and tests --- src/lib/state.ml | 26 ++++++ src/sail_lean_backend/pretty_print_lean.ml | 94 ++++++++++++++++++++-- test/lean/bitfield.expected.lean | 20 +++-- test/lean/reg.expected.lean | 16 ++++ test/lean/reg.sail | 5 ++ test/lean/struct.expected.lean | 5 +- 6 files changed, 153 insertions(+), 13 deletions(-) create mode 100644 test/lean/reg.expected.lean create mode 100644 test/lean/reg.sail diff --git a/src/lib/state.ml b/src/lib/state.ml index a5b958aaf..855050b5a 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -835,6 +835,32 @@ let register_refs_coq doc_id coq_record_update env registers = in separate hardline [generic_convs; refs; getters_setters] +let register_refs_lean doc_id doc_typ registers = + let generic_convs = separate_map hardline string [""; "variable [MonadReg]"; ""; "open MonadReg"; ""] in + let register_ref (typ, id, _) = + let idd = doc_id id in + let typp = doc_typ typ in + concat + [ + string " set_"; + idd; + colon; + space; + typp; + string " -> SailM Unit"; + hardline; + string " get_"; + idd; + colon; + space; + string "SailM ("; + typp; + string ")"; + ] + in + let refs = separate_map hardline register_ref registers in + separate hardline [string "class MonadReg where"; refs; generic_convs] + let generate_regstate_defs ctx env ast = let defs = ast.defs in let registers = find_registers defs in diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 06a22684b..9c499a0d8 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -264,6 +264,60 @@ let string_of_exp_con (E_aux (e, _)) = | E_vector _ -> "E_vector" | E_let _ -> "E_let" +let string_of_pat_con (P_aux (p, _)) = + match p with + | P_app _ -> "P_app" + | P_wild -> "P_wild" + | P_lit _ -> "P_lit" + | P_or _ -> "P_or" + | P_not _ -> "P_not" + | P_as _ -> "P_as" + | P_typ _ -> "P_typ" + | P_id _ -> "P_id" + | P_var _ -> "P_var" + | P_vector _ -> "P_vector" + | P_vector_concat _ -> "P_vector_concat" + | P_vector_subrange _ -> "P_vector_subrange" + | P_tuple _ -> "P_tuple" + | P_list _ -> "P_list" + | P_cons _ -> "P_cons" + | P_string_append _ -> "P_string_append" + | P_struct _ -> "P_struct" + +let rec doc_pat ctxt apat_needed (P_aux (p, (l, annot)) as pat) = + let env = env_of_annot (l, annot) in + let typ = Env.expand_synonyms env (typ_of_annot (l, annot)) in + match p with + | P_typ (ptyp, p) -> + let doc_p = doc_pat ctxt true p in + doc_p + | P_id id -> doc_id_ctor id + | _ -> failwith ("Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.") + +(* Copied from the Coq PP *) +let rebind_cast_pattern_vars pat typ exp = + let rec aux pat typ = + match (pat, typ) with + | P_aux (P_typ (target_typ, P_aux (P_id id, (l, ann))), _), source_typ when not (is_enum (env_of exp) id) -> + if Typ.compare target_typ source_typ == 0 then [] + else ( + let l = Parse_ast.Generated l in + let cast_annot = Type_check.replace_typ source_typ ann in + let e_annot = Type_check.mk_tannot (env_of exp) source_typ in + [LB_aux (LB_val (pat, E_aux (E_id id, (l, e_annot))), (l, ann))] + ) + | P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs) + | _ -> [] + in + let add_lb (E_aux (_, ann) as exp) lb = E_aux (E_let (lb, exp), ann) in + (* Don't introduce new bindings at the top-level, we'd just go into a loop. *) + let lbs = + match (pat, typ) with + | P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs) + | _ -> [] + in + List.fold_left add_lb exp lbs + let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = let env = env_of_tannot annot in match e with @@ -271,7 +325,21 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = | 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 *) + | E_internal_plet (pat, e1, e2) -> + (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *) + let e0 = doc_pat ctx false pat in + let e1_pp = doc_exp ctx e1 in + let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in + let e2_pp = doc_exp ctx e2' in + (* infix 0 1 middle e1_pp e2_pp *) + let e0_pp = + begin + match pat with + | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" + | _ -> separate space [string "let"; e0; string ":="] ^^ space + end + in + e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") @@ -280,7 +348,13 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = let d_args = List.map (doc_exp ctx) args in nest 2 (parens (flow (break 1) (d_id :: d_args))) | E_vector vals -> failwith "vector found" - | E_typ (typ, e) -> parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ]) + | E_typ (typ, e) -> ( + match e with + | E_aux (E_assign _, _) -> doc_exp ctx e + | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> + string "return " ^^ nest 7 (parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ])) + | _ -> parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ]) + ) | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctx) es) | E_let (LB_aux (LB_val (lpat, lexp), _), e) -> let id = @@ -297,6 +371,13 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = | E_struct_update (exp, fexps) -> let args = List.map (doc_fexp ctx) fexps in braces (space ^^ doc_exp ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space) + | E_assign ((LE_aux (le_act, tannot) as le), e) -> ( + match le_act with + | LE_id id | LE_typ (_, id) -> string "set_" ^^ doc_id_ctor id ^^ space ^^ doc_exp ctx e + | LE_deref e -> string "sorry /- deref -/" + | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") + ) + | E_internal_return e -> nest 2 (string "return" ^^ space ^^ nest 5 (doc_exp ctx e)) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp ctx (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctx exp @@ -363,8 +444,7 @@ let doc_funcl_body (FCL_aux (FCL_funcl (id, pexp), annot)) = let env = env_of_tannot (snd annot) in let ctx = initial_context env in let _, _, exp, _ = destruct_pexp pexp in - let is_monadic = effectful (effect_of exp) in - if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctx exp]) else doc_exp ctx exp + doc_exp (initial_context env) exp let doc_funcl ctx funcl = let comment, signature, env = doc_funcl_init funcl in @@ -425,6 +505,10 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in + let regs = State.find_registers defs in + let register_refs = + match regs with [] -> empty | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline + in let output : document = separate_map empty (doc_def (initial_context env)) defs in - print o output; + print o (register_refs ^^ output); () diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index b100161a8..1c7b11aae 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -5,7 +5,7 @@ open Sail def cr_type := (BitVec 8) def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := - return ((undefined_bitvector 8) : (BitVec 8)) + ((undefined_bitvector 8) : (BitVec 8)) def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) := v @@ -17,7 +17,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := (Sail.BitVec.extractLsb v 7 4) @@ -26,7 +27,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 3 2) @@ -35,7 +37,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 1 0) @@ -44,7 +47,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 6 6) @@ -53,7 +57,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 7 7) @@ -62,7 +67,8 @@ 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := - return sorry + let r := (reg_deref r_ref) + sorry /- deref -/ def initialize_registers : Unit := () diff --git a/test/lean/reg.expected.lean b/test/lean/reg.expected.lean new file mode 100644 index 000000000..00e105040 --- /dev/null +++ b/test/lean/reg.expected.lean @@ -0,0 +1,16 @@ +import Out.Sail.Sail + +open Sail + +class MonadReg where + set_R0: (BitVec 64) -> SailM Unit + get_R0: SailM ((BitVec 64)) + +variable [MonadReg] + +open MonadReg + +def initialize_registers : SailM Unit := + let w__0 := (undefined_bitvector 64) + set_R0 w__0 + diff --git a/test/lean/reg.sail b/test/lean/reg.sail new file mode 100644 index 000000000..0b2a367ab --- /dev/null +++ b/test/lean/reg.sail @@ -0,0 +1,5 @@ +default Order dec + +$include + +register R0 : bits(64) \ No newline at end of file diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 60424c7cc..714309b0a 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -7,7 +7,10 @@ structure My_struct where field2 : (BitVec 1) def undefined_My_struct (lit : Unit) : SailM My_struct := - return sorry + let w__0 := (undefined_int ()) + let w__1 := (undefined_bit ()) + return { field1 := w__0 + field2 := w__1 } def struct_field2 (s : My_struct) : (BitVec 1) := s.field2 From df046cece0e8160e1b5cc714889769d2dc9d7845 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 20 Jan 2025 13:16:41 +0000 Subject: [PATCH 02/23] Fix lean style in state.ml --- src/lib/state.ml | 5 +++-- test/lean/{reg.expected.lean => registers.expected.lean} | 4 ++-- test/lean/{reg.sail => registers.sail} | 0 3 files changed, 5 insertions(+), 4 deletions(-) rename test/lean/{reg.expected.lean => registers.expected.lean} (73%) rename test/lean/{reg.sail => registers.sail} (100%) diff --git a/src/lib/state.ml b/src/lib/state.ml index 855050b5a..1e24dd927 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -844,6 +844,7 @@ let register_refs_lean doc_id doc_typ registers = [ string " set_"; idd; + space; colon; space; typp; @@ -851,11 +852,11 @@ let register_refs_lean doc_id doc_typ registers = hardline; string " get_"; idd; + space; colon; space; - string "SailM ("; + string "SailM "; typp; - string ")"; ] in let refs = separate_map hardline register_ref registers in diff --git a/test/lean/reg.expected.lean b/test/lean/registers.expected.lean similarity index 73% rename from test/lean/reg.expected.lean rename to test/lean/registers.expected.lean index 00e105040..88f30150e 100644 --- a/test/lean/reg.expected.lean +++ b/test/lean/registers.expected.lean @@ -3,8 +3,8 @@ import Out.Sail.Sail open Sail class MonadReg where - set_R0: (BitVec 64) -> SailM Unit - get_R0: SailM ((BitVec 64)) + set_R0 : (BitVec 64) -> SailM Unit + get_R0 : SailM (BitVec 64) variable [MonadReg] diff --git a/test/lean/reg.sail b/test/lean/registers.sail similarity index 100% rename from test/lean/reg.sail rename to test/lean/registers.sail From 6840387c005983ef9eaddaef4e7809ae00f0231e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 21 Jan 2025 11:03:53 +0000 Subject: [PATCH 03/23] pretty printing fixes --- src/sail_lean_backend/pretty_print_lean.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 9c499a0d8..00db91ba8 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -336,10 +336,10 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = begin match pat with | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" - | _ -> separate space [string "let"; e0; string ":="] ^^ space + | _ -> flow (break 1) [string "let"; e0; string ":="] ^^ space end in - e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp + nest 2 (e0_pp ^^ e1_pp) ^^ hardline ^^ e2_pp | E_app (f, args) -> let d_id = if Env.is_extern f env "lean" then string (Env.get_extern f env "lean") @@ -352,8 +352,8 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = match e with | E_aux (E_assign _, _) -> doc_exp ctx e | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> - string "return " ^^ nest 7 (parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ])) - | _ -> parens (separate space [doc_exp ctx e; colon; doc_typ ctx typ]) + string "return " ^^ nest 7 (parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ])) + | _ -> parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ]) ) | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctx) es) | E_let (LB_aux (LB_val (lpat, lexp), _), e) -> From bce92f1408b8dedf16da89fc30f55e77a3edab74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 21 Jan 2025 11:07:05 +0000 Subject: [PATCH 04/23] formatting --- src/sail_lean_backend/pretty_print_lean.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 00db91ba8..f5fbc1b1e 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -507,7 +507,9 @@ let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check. let defs = remove_imports defs 0 in let regs = State.find_registers defs in let register_refs = - match regs with [] -> empty | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline + match regs with + | [] -> empty + | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline in let output : document = separate_map empty (doc_def (initial_context env)) defs in print o (register_refs ^^ output); From 7966840d333aa3cdb72cd0593521499da6790cb2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 21 Jan 2025 13:35:23 +0000 Subject: [PATCH 05/23] New monad definition --- src/lib/state.ml | 15 +++------------ src/sail_lean_backend/Sail/Sail.lean | 2 +- src/sail_lean_backend/pretty_print_lean.ml | 1 + 3 files changed, 5 insertions(+), 13 deletions(-) diff --git a/src/lib/state.ml b/src/lib/state.ml index 1e24dd927..64430eb75 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -836,31 +836,22 @@ let register_refs_coq doc_id coq_record_update env registers = separate hardline [generic_convs; refs; getters_setters] let register_refs_lean doc_id doc_typ registers = - let generic_convs = separate_map hardline string [""; "variable [MonadReg]"; ""; "open MonadReg"; ""] in + let generic_convs = separate_map hardline string [""; "abbrev SailM := StateM SailReg"; ""] in let register_ref (typ, id, _) = let idd = doc_id id in let typp = doc_typ typ in concat [ - string " set_"; + string " "; idd; space; colon; space; typp; - string " -> SailM Unit"; - hardline; - string " get_"; - idd; - space; - colon; - space; - string "SailM "; - typp; ] in let refs = separate_map hardline register_ref registers in - separate hardline [string "class MonadReg where"; refs; generic_convs] + separate hardline [string "structure SailReg where"; refs; generic_convs] let generate_regstate_defs ctx env ast = let defs = ast.defs in diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index dc3dc9f92..697b858d7 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -1,7 +1,7 @@ namespace Sail /- Placeholder for a future implementation of the state monad some Sail functions use. -/ -abbrev SailM := StateM Unit +-- abbrev SailM := StateM Unit namespace BitVec diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index f5fbc1b1e..2edd728b8 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -292,6 +292,7 @@ let rec doc_pat ctxt apat_needed (P_aux (p, (l, annot)) as pat) = let doc_p = doc_pat ctxt true p in doc_p | P_id id -> doc_id_ctor id + | P_wild -> underscore | _ -> failwith ("Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.") (* Copied from the Coq PP *) From ad58fe9c69f767847f8d24d6dfc4af32faa0f9b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 21 Jan 2025 17:28:09 +0000 Subject: [PATCH 06/23] Registers in the state monad --- src/lib/state.ml | 18 --- src/sail_lean_backend/Sail/Sail.lean | 32 +++-- src/sail_lean_backend/pretty_print_lean.ml | 144 ++++++++++++++++++++- test/lean/registers.expected.lean | 86 +++++++++++- test/lean/registers.sail | 7 +- 5 files changed, 252 insertions(+), 35 deletions(-) diff --git a/src/lib/state.ml b/src/lib/state.ml index 64430eb75..a5b958aaf 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -835,24 +835,6 @@ let register_refs_coq doc_id coq_record_update env registers = in separate hardline [generic_convs; refs; getters_setters] -let register_refs_lean doc_id doc_typ registers = - let generic_convs = separate_map hardline string [""; "abbrev SailM := StateM SailReg"; ""] in - let register_ref (typ, id, _) = - let idd = doc_id id in - let typp = doc_typ typ in - concat - [ - string " "; - idd; - space; - colon; - space; - typp; - ] - in - let refs = separate_map hardline register_ref registers in - separate hardline [string "structure SailReg where"; refs; generic_convs] - let generate_regstate_defs ctx env ast = let defs = ast.defs in let registers = find_registers defs in diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 697b858d7..a2305e91d 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -1,7 +1,23 @@ namespace Sail -/- Placeholder for a future implementation of the state monad some Sail functions use. -/ --- abbrev SailM := StateM Unit +/- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ +abbrev Error := Unit + +structure SequentialSate ( Regs : Type ) where + regs : Regs + mem : Unit + tags : Unit + +abbrev PreSailM ( Regs: Type ) := EStateM Error (SequentialSate Regs) + +def read_reg {Register : Type -> Type} (register_lookup : ∀ T, Register T -> Regstate -> T) (reg : Register S) : PreSailM Regstate S := do + let r ← get + return register_lookup _ reg r.regs + +def write_reg {Register : Type -> Type} (register_set : ∀ T, Register T -> T -> Regstate -> Regstate) (reg : Register S) (s : S) : PreSailM Regstate Unit := do + let r ← get + set { r with regs := register_set _ reg s r.regs } + return () namespace BitVec @@ -33,12 +49,12 @@ def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + end BitVec end Sail -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 +-- 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_bitvector (w : Nat) : BitVec w := 0 diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 2edd728b8..1a49f194f 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -504,13 +504,151 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en | DEF_aux (DEF_pragma ("include_end", _, _), _) :: ds -> remove_imports ds (depth - 1) | d :: ds -> if depth > 0 then remove_imports ds depth else d :: remove_imports ds depth +let opt_cons v = function None -> Some [v] | Some t -> Some (v :: t) + +let reg_type_name typ_id = prepend_id "register_" typ_id +let reg_case_name typ_id = prepend_id "R_" typ_id +let state_field_name typ_id = append_id typ_id "_s" +let ref_name reg = append_id reg "_ref" +let add_reg_typ env (typ_map, regs_map) (typ, id, has_init) = + let typ_id = State.id_of_regtyp IdSet.empty typ in + (Bindings.add typ_id typ typ_map, Bindings.update typ_id (opt_cons id) regs_map) + +let per_type_register_enum ctxt typ_id registers = + let reg_type_id = reg_type_name typ_id in + let reg_type_pp = doc_id_ctor reg_type_id in + separate hardline + [ + string "inductive " ^^ reg_type_pp ^^ string " where"; + separate_map hardline (fun r -> string " | " ^^ doc_id_ctor r) registers; + string "deriving DecidableEq"; + string "open " ^^ reg_type_pp; + empty; + empty; + ] + +let type_enum ctxt env type_map = + separate hardline + [ + string "inductive Register : Type -> Type where"; + separate_map hardline + (fun (typ_id, typ) -> + string " | " + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ space ^^ colon ^^ space + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ string " -> Register " ^^ doc_typ ctxt typ + ) + type_map; + empty; + separate_map hardline + (fun (typ_id, typ) -> + string "instance : Coe " + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ space + ^^ parens (string "Register " ^^ doc_typ ctxt typ) + ^^ string " where" ^^ hardline ^^ string " coe r := Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r" + ) + type_map; + empty; + ] + +let regstate ctxt env type_map = + separate hardline + [ + string "structure Regstate where"; + separate_map hardline + (fun (typ_id, typ) -> + string " " + ^^ doc_id_ctor (state_field_name typ_id) + ^^ string " : " + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ string " -> " ^^ doc_typ ctxt typ + ) + type_map; + string ""; + (* doc_field_updates ctxt (mk_typquant []) (mk_id "regstate") + (List.map (fun (typ_id, typ) -> (typ, state_field_name typ_id)) type_map); *) + empty; + (* A record literal can cause problems with record type inference (e.g., if there are no registers) *) + (* string "Definition init_regstate : regstate := Build_regstate"; + separate_map hardline (fun _ -> string " inhabitant") type_map; + string "."; + empty; *) + ] + +let reg_accessors ctxt env type_map = + separate hardline + [ + string "def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :="; + string " match reg with"; + separate_map hardline + (fun (typ_id, _typ) -> + string " | Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r => rs." + ^^ doc_id_ctor (state_field_name typ_id) + ^^ string " r" + ) + type_map; + empty; + string "def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :="; + string " match reg with"; + separate_map hardline + (fun (typ_id, _typ) -> + string " | Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r => fun v rs => " + ^^ + let field = doc_id_ctor (state_field_name typ_id) in + let fexp = + string " rs with " ^^ field ^^ string " := fun r' => if r' = r then v else rs." ^^ field ^^ string " r' " + in + implicit_parens fexp + ) + type_map; + empty; + empty; + ] + +let doc_reg_info env registers = + let bare_ctxt = initial_context env in + let type_map, type_regs_map = List.fold_left (add_reg_typ env) (Bindings.empty, Bindings.empty) registers in + let type_map = Bindings.bindings type_map in + let type_regs_map = Bindings.bindings type_regs_map in + + let reg_enums = List.fold_left (fun pp (t, rs) -> pp ^^ per_type_register_enum bare_ctxt t rs) empty type_regs_map in + separate hardline + [ + reg_enums; + type_enum bare_ctxt env type_map; + (* register_refs bare_ctxt env type_regs_map; + empty; + string "(* Definitions to support the lifting to the sequential monad *)"; *) + regstate bare_ctxt env type_map; + reg_accessors bare_ctxt env type_map; + string "abbrev SailM := PreSailM Regstate"; + string "def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup"; + string "def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set"; + empty; + empty; + (* string + + "Definition register_accessors : register_accessors regstate register := (@register_lookup, @register_set)."; + empty; + empty; *) + ] + let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in let regs = State.find_registers defs in let register_refs = - match regs with - | [] -> empty - | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline + doc_reg_info env regs + (* match regs with + | [] -> empty + | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline *) in let output : document = separate_map empty (doc_def (initial_context env)) defs in print o (register_refs ^^ output); diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index 88f30150e..37b6616f1 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -2,15 +2,91 @@ import Out.Sail.Sail open Sail -class MonadReg where - set_R0 : (BitVec 64) -> SailM Unit - get_R0 : SailM (BitVec 64) +inductive register_bit where + | BIT +deriving DecidableEq +open register_bit -variable [MonadReg] +inductive register_bitvector_64 where + | R0 + | R1 +deriving DecidableEq +open register_bitvector_64 -open MonadReg +inductive register_bool where + | BOOL +deriving DecidableEq +open register_bool + +inductive register_int where + | INT +deriving DecidableEq +open register_int + +inductive register_nat where + | NAT +deriving DecidableEq +open register_nat + + +inductive Register : Type -> Type where + | R_bit : register_bit -> Register (BitVec 1) + | R_bitvector_64 : register_bitvector_64 -> Register (BitVec 64) + | R_bool : register_bool -> Register Bool + | R_int : register_int -> Register Int + | R_nat : register_nat -> Register Nat + +instance : Coe register_bit (Register (BitVec 1)) where + coe r := Register.R_bit r +instance : Coe register_bitvector_64 (Register (BitVec 64)) where + coe r := Register.R_bitvector_64 r +instance : Coe register_bool (Register Bool) where + coe r := Register.R_bool r +instance : Coe register_int (Register Int) where + coe r := Register.R_int r +instance : Coe register_nat (Register Nat) where + coe r := Register.R_nat r + +structure Regstate where + bit_s : register_bit -> (BitVec 1) + bitvector_64_s : register_bitvector_64 -> (BitVec 64) + bool_s : register_bool -> Bool + int_s : register_int -> Int + nat_s : register_nat -> Nat + + +def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T := + match reg with + | Register.R_bit r => rs.bit_s r + | Register.R_bitvector_64 r => rs.bitvector_64_s r + | Register.R_bool r => rs.bool_s r + | Register.R_int r => rs.int_s r + | Register.R_nat r => rs.nat_s r + +def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate := + match reg with + | Register.R_bit r => fun v rs => { rs with bit_s := fun r' => if r' = r then v else rs.bit_s r' } + | Register.R_bitvector_64 r => fun v rs => { rs with bitvector_64_s := fun r' => if r' = r then v else rs.bitvector_64_s r' } + | Register.R_bool r => fun v rs => { rs with bool_s := fun r' => if r' = r then v else rs.bool_s r' } + | Register.R_int r => fun v rs => { rs with int_s := fun r' => if r' = r then v else rs.int_s r' } + | Register.R_nat r => fun v rs => { rs with nat_s := fun r' => if r' = r then v else rs.nat_s r' } + + +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set def initialize_registers : SailM Unit := let w__0 := (undefined_bitvector 64) set_R0 w__0 + let w__1 := (undefined_bitvector 64) + set_R1 w__1 + let w__2 := (undefined_int ()) + set_INT w__2 + let w__3 := (undefined_bool ()) + set_BOOL w__3 + let w__4 := (undefined_nat ()) + set_NAT w__4 + let w__5 := (undefined_bit ()) + set_BIT w__5 diff --git a/test/lean/registers.sail b/test/lean/registers.sail index 0b2a367ab..43175ccb3 100644 --- a/test/lean/registers.sail +++ b/test/lean/registers.sail @@ -2,4 +2,9 @@ default Order dec $include -register R0 : bits(64) \ No newline at end of file +register R0 : bits(64) +register R1 : bits(64) +register INT : int +register BOOL : bool +register NAT : nat +register BIT : bit \ No newline at end of file From cf57e2082af28426ce73dd1ee9c76257692a1eba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 22 Jan 2025 12:35:08 +0000 Subject: [PATCH 07/23] fixing read/write reg output --- src/sail_lean_backend/pretty_print_lean.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 1a49f194f..38c2cad9d 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -322,7 +322,9 @@ let rebind_cast_pattern_vars pat typ exp = let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = let env = env_of_tannot annot in match e with - | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *) + | E_id id -> + if Env.is_register id env then string "read_reg " ^^ doc_id_ctor id + else string (string_of_id id) | E_lit l -> doc_lit l | E_app (Id_aux (Id "internal_pick", _), _) -> string "sorry" (* TODO replace by actual implementation of internal_pick *) @@ -354,6 +356,7 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = | E_aux (E_assign _, _) -> doc_exp ctx e | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> string "return " ^^ nest 7 (parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ])) + | E_aux (E_id id, _) when Env.is_register id (env_of e) -> doc_exp ctx e | _ -> parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ]) ) | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctx) es) @@ -374,7 +377,7 @@ let rec doc_exp ctx (E_aux (e, (l, annot)) as full_exp) = braces (space ^^ doc_exp ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space) | E_assign ((LE_aux (le_act, tannot) as le), e) -> ( match le_act with - | LE_id id | LE_typ (_, id) -> string "set_" ^^ doc_id_ctor id ^^ space ^^ doc_exp ctx e + | LE_id id | LE_typ (_, id) -> string "write_reg " ^^ doc_id_ctor id ^^ space ^^ doc_exp ctx e | LE_deref e -> string "sorry /- deref -/" | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") ) From fa92534bb82598206b7d0a6bbffaa1cbdf5ea0aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 22 Jan 2025 14:00:25 +0000 Subject: [PATCH 08/23] Fixing registers and bitfield --- src/sail_lean_backend/Sail/Sail.lean | 16 +- src/sail_lean_backend/pretty_print_lean.ml | 199 +++++++++++---------- test/lean/bitfield.expected.lean | 40 +++-- test/lean/registers.expected.lean | 23 +-- 4 files changed, 149 insertions(+), 129 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index a2305e91d..15d05a377 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -10,6 +10,9 @@ structure SequentialSate ( Regs : Type ) where abbrev PreSailM ( Regs: Type ) := EStateM Error (SequentialSate Regs) +structure RegisterRef (Register : Type -> Type) (T : Type) where + reg : Register T + def read_reg {Register : Type -> Type} (register_lookup : ∀ T, Register T -> Regstate -> T) (reg : Register S) : PreSailM Regstate S := do let r ← get return register_lookup _ reg r.regs @@ -19,6 +22,9 @@ def write_reg {Register : Type -> Type} (register_set : ∀ T, Register T -> T - set { r with regs := register_set _ reg s r.regs } return () +def reg_deref {Register : Type → Type} (read_reg : ∀ T, Register T → PreSailM Regstate T) (reg_ref : RegisterRef Register T) : PreSailM Regstate T := do + read_reg _ reg_ref.reg + namespace BitVec def length {w : Nat} (_ : BitVec w) : Nat := w @@ -48,13 +54,3 @@ def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + end BitVec end Sail - --- 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_bitvector (w : Nat) : BitVec w := - 0 diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index f0a141dec..1c8ee2a41 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -151,9 +151,7 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) = -> parens (string "BitVec " ^^ doc_nexp ctx m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int" - | Typ_app (Id_aux (Id "register", _), t_app) -> - string "RegisterRef Unit Unit " - (* TODO: Replace units with real types. *) ^^ separate_map comma (doc_typ_app ctx) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) 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 ctx) ts) @@ -344,6 +342,9 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = let field_monadic = effectful (effect_of e) in doc_fexp field_monadic ctx fexp in + (* string (string_of_exp_con full_exp) + ^^ space + ^^ *) match e with | E_id id -> if Env.is_register id env then string "read_reg " ^^ doc_id_ctor id @@ -352,6 +353,8 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = | E_app (Id_aux (Id "undefined_int", _), _) (* TODO remove when we handle imports *) | E_app (Id_aux (Id "undefined_bit", _), _) (* TODO remove when we handle imports *) | E_app (Id_aux (Id "undefined_bitvector", _), _) (* TODO remove when we handle imports *) + | E_app (Id_aux (Id "undefined_bool", _), _) (* TODO remove when we handle imports *) + | E_app (Id_aux (Id "undefined_nat", _), _) (* TODO remove when we handle imports *) | E_app (Id_aux (Id "internal_pick", _), _) -> (* TODO replace by actual implementation of internal_pick *) string "sorry" @@ -366,7 +369,7 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = begin match pat with | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string "" - | _ -> flow (break 1) [string "let"; e0; string ":="] ^^ space + | _ -> flow (break 1) [string "let"; e0; string "←"] ^^ space end in nest 2 (e0_pp ^^ e1_pp) ^^ hardline ^^ e2_pp @@ -571,90 +574,106 @@ let per_type_register_enum ctxt typ_id registers = ] let type_enum ctxt env type_map = - separate hardline - [ - string "inductive Register : Type -> Type where"; - separate_map hardline - (fun (typ_id, typ) -> - string " | " - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ space ^^ colon ^^ space - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " -> Register " ^^ doc_typ ctxt typ - ) - type_map; - empty; - separate_map hardline - (fun (typ_id, typ) -> - string "instance : Coe " - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ space - ^^ parens (string "Register " ^^ doc_typ ctxt typ) - ^^ string " where" ^^ hardline ^^ string " coe r := Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r" - ) - type_map; - empty; - ] + match type_map with + | [] -> string "def Register (T : Type) := T" + | _ -> + separate hardline + [ + string "inductive Register : Type -> Type where"; + separate_map hardline + (fun (typ_id, typ) -> + string " | " + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ space ^^ colon ^^ space + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ string " -> Register " ^^ doc_typ ctxt typ + ) + type_map; + empty; + separate_map hardline + (fun (typ_id, typ) -> + string "instance : Coe " + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ space + ^^ parens (string "Register " ^^ doc_typ ctxt typ) + ^^ string " where" ^^ hardline ^^ string " coe r := Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r" + ) + type_map; + empty; + ] let regstate ctxt env type_map = - separate hardline - [ - string "structure Regstate where"; - separate_map hardline - (fun (typ_id, typ) -> - string " " - ^^ doc_id_ctor (state_field_name typ_id) - ^^ string " : " - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " -> " ^^ doc_typ ctxt typ - ) - type_map; - string ""; - (* doc_field_updates ctxt (mk_typquant []) (mk_id "regstate") - (List.map (fun (typ_id, typ) -> (typ, state_field_name typ_id)) type_map); *) - empty; - (* A record literal can cause problems with record type inference (e.g., if there are no registers) *) - (* string "Definition init_regstate : regstate := Build_regstate"; - separate_map hardline (fun _ -> string " inhabitant") type_map; - string "."; - empty; *) - ] + match type_map with + | [] -> string "abbrev Regstate := Unit" + | _ -> + separate hardline + [ + string "structure Regstate where"; + separate_map hardline + (fun (typ_id, typ) -> + string " " + ^^ doc_id_ctor (state_field_name typ_id) + ^^ string " : " + ^^ doc_id_ctor (reg_type_name typ_id) + ^^ string " -> " ^^ doc_typ ctxt typ + ) + type_map; + string ""; + (* doc_field_updates ctxt (mk_typquant []) (mk_id "regstate") + (List.map (fun (typ_id, typ) -> (typ, state_field_name typ_id)) type_map); *) + empty; + (* A record literal can cause problems with record type inference (e.g., if there are no registers) *) + (* string "Definition init_regstate : regstate := Build_regstate"; + separate_map hardline (fun _ -> string " inhabitant") type_map; + string "."; + empty; *) + ] let reg_accessors ctxt env type_map = - separate hardline - [ - string "def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :="; - string " match reg with"; - separate_map hardline - (fun (typ_id, _typ) -> - string " | Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r => rs." - ^^ doc_id_ctor (state_field_name typ_id) - ^^ string " r" - ) - type_map; - empty; - string "def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :="; - string " match reg with"; - separate_map hardline - (fun (typ_id, _typ) -> - string " | Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r => fun v rs => " - ^^ - let field = doc_id_ctor (state_field_name typ_id) in - let fexp = - string " rs with " ^^ field ^^ string " := fun r' => if r' = r then v else rs." ^^ field ^^ string " r' " - in - implicit_parens fexp - ) - type_map; - empty; - empty; - ] + match type_map with + | [] -> + separate hardline + [ + string "def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg"; + string "def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()"; + ] + | _ -> + separate hardline + [ + string "def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :="; + string " match reg with"; + separate_map hardline + (fun (typ_id, _typ) -> + string " | Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r => rs." + ^^ doc_id_ctor (state_field_name typ_id) + ^^ string " r" + ) + type_map; + empty; + string "def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :="; + string " match reg with"; + separate_map hardline + (fun (typ_id, _typ) -> + string " | Register." + ^^ doc_id_ctor (reg_case_name typ_id) + ^^ string " r => fun v rs => " + ^^ + let field = doc_id_ctor (state_field_name typ_id) in + let fexp = + string " rs with " ^^ field + ^^ string " := fun r' => if r' = r then v else rs." + ^^ field ^^ string " r' " + in + implicit_parens fexp + ) + type_map; + empty; + empty; + ] let doc_reg_info env registers = let bare_ctxt = initial_context env in @@ -675,8 +694,7 @@ let doc_reg_info env registers = string "abbrev SailM := PreSailM Regstate"; string "def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup"; string "def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set"; - empty; - empty; + string "def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg"; (* string "Definition register_accessors : register_accessors regstate register := (@register_lookup, @register_set)."; @@ -687,12 +705,7 @@ let doc_reg_info env registers = let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in let regs = State.find_registers defs in - let register_refs = - doc_reg_info env regs - (* match regs with - | [] -> empty - | _ -> State.register_refs_lean doc_id_ctor (doc_typ (initial_context env)) regs ^^ hardline *) - in + let register_refs = doc_reg_info env regs in let output : document = separate_map empty (doc_def (initial_context env)) defs in - print o (register_refs ^^ output); + print o (register_refs ^^ hardline ^^ hardline ^^ output); () diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 72d994159..2d10181f7 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def cr_type := (BitVec 8) def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do @@ -16,8 +26,9 @@ def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : SailM Unit := do - sorry +def _set_cr_type_bits (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 8)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := (Sail.BitVec.extractLsb v 7 4) @@ -25,8 +36,9 @@ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : SailM Unit := do - sorry +def _set_cr_type_CR0 (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 4)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 3 2) @@ -34,8 +46,9 @@ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do - sorry +def _set_cr_type_CR1 (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 1 0) @@ -43,8 +56,9 @@ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do - sorry +def _set_cr_type_CR3 (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 6 6) @@ -52,8 +66,9 @@ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do - sorry +def _set_cr_type_GT (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 7 7) @@ -61,8 +76,9 @@ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do - sorry +def _set_cr_type_LT (r_ref : RegisterRef Register (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do + let r ← (reg_deref r_ref) + sorry /- deref -/ def initialize_registers : Unit := () diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index 37b6616f1..b5c587149 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -75,18 +75,13 @@ def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate := abbrev SailM := PreSailM Regstate def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set - -def initialize_registers : SailM Unit := - let w__0 := (undefined_bitvector 64) - set_R0 w__0 - let w__1 := (undefined_bitvector 64) - set_R1 w__1 - let w__2 := (undefined_int ()) - set_INT w__2 - let w__3 := (undefined_bool ()) - set_BOOL w__3 - let w__4 := (undefined_nat ()) - set_NAT w__4 - let w__5 := (undefined_bit ()) - set_BIT w__5 +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + +def initialize_registers : SailM Unit := do + write_reg R0 sorry + write_reg R1 sorry + write_reg INT sorry + write_reg BOOL sorry + write_reg NAT sorry + write_reg BIT sorry From 03c29dc3180387aa9474cec22cfb61c2e8c1e38a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 22 Jan 2025 14:31:29 +0000 Subject: [PATCH 09/23] Fixing tests --- src/sail_lean_backend/pretty_print_lean.ml | 24 ++++++++++++++-------- test/lean/bitfield.expected.lean | 4 ++-- test/lean/bitvec_operation.expected.lean | 10 +++++++++ test/lean/enum.expected.lean | 10 +++++++++ test/lean/extern.expected.lean | 10 +++++++++ test/lean/extern_bitvec.expected.lean | 10 +++++++++ test/lean/let.expected.lean | 10 +++++++++ test/lean/range.expected.lean | 10 +++++++++ test/lean/struct.expected.lean | 10 +++++++++ test/lean/trivial.expected.lean | 10 +++++++++ test/lean/tuples.expected.lean | 10 +++++++++ test/lean/typedef.expected.lean | 10 +++++++++ test/lean/typquant.expected.lean | 10 +++++++++ 13 files changed, 128 insertions(+), 10 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 1c8ee2a41..8da876f63 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -151,7 +151,8 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) = -> parens (string "BitVec " ^^ doc_nexp ctx m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int" - | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> + string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) 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 ctx) ts) @@ -536,11 +537,16 @@ let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) = nest 2 (flow (break 1) [string "def"; string id; colon; string "Int"; coloneq; doc_nexp ctx ne]) | _ -> failwith ("Type definition " ^ string_of_type_def_con full_typdef ^ " not translatable yet.") -let doc_def ctx (DEF_aux (aux, def_annot) as def) = - match aux with - | DEF_fundef fdef -> group (doc_fundef ctx fdef) ^/^ hardline - | DEF_type tdef -> group (doc_typdef ctx tdef) ^/^ hardline - | _ -> empty +let rec doc_defs_aux ctx defs types fundefs = + match defs with + | [] -> (types, fundefs) + | DEF_aux (DEF_fundef fdef, _) :: defs' -> + doc_defs_aux ctx defs' types (fundefs ^^ group (doc_fundef ctx fdef) ^/^ hardline) + | DEF_aux (DEF_type tdef, _) :: defs' -> + doc_defs_aux ctx defs' (types ^^ group (doc_typdef ctx tdef) ^/^ hardline) fundefs + | _ :: defs' -> doc_defs_aux ctx defs' types fundefs + +let doc_defs ctx defs = doc_defs_aux ctx defs empty empty (* Remove all imports for now, they will be printed in other files. Probably just for testing. *) let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.env) def list) depth = @@ -706,6 +712,8 @@ let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check. let defs = remove_imports defs 0 in let regs = State.find_registers defs in let register_refs = doc_reg_info env regs in - let output : document = separate_map empty (doc_def (initial_context env)) defs in - print o (register_refs ^^ hardline ^^ hardline ^^ output); + let types, fundefs = doc_defs (initial_context env) defs in + (* let types = separate empty types in + let fundefs = separate empty fundefs in *) + print o (types ^^ register_refs ^^ hardline ^^ hardline ^^ fundefs); () diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 2d10181f7..5c653ba1c 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -2,6 +2,8 @@ import Out.Sail.Sail open Sail +def cr_type := (BitVec 8) + def Register (T : Type) := T abbrev Regstate := Unit @@ -12,8 +14,6 @@ def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @registe def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg -def cr_type := (BitVec 8) - def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do sorry diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index 8f1f7ca93..6bfc9b812 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool := (Eq x y) diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index 637d9c28d..137703592 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -5,6 +5,16 @@ open Sail inductive E where | A | B | C deriving Inhabited + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def undefined_E : SailM E := do sorry diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index a67f1c206..63d959bd6 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def extern_add : Int := (Int.add 5 4) diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean index af4bdb0f9..8a56386f5 100644 --- a/test/lean/extern_bitvec.expected.lean +++ b/test/lean/extern_bitvec.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def extern_const : (BitVec 64) := (0xFFFF000012340000 : (BitVec 64)) diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index b2eb331d0..99ae3c6ac 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def foo : (BitVec 16) := let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16))) (HAnd.hAnd (0x0000 : (BitVec 16)) z) diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean index 6b9b23e3b..21d175436 100644 --- a/test/lean/range.expected.lean +++ b/test/lean/range.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + /-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/ def f_int (x : Nat) : Int := 0 diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index f4703e14c..392403157 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -6,6 +6,16 @@ structure My_struct where field1 : Int field2 : (BitVec 1) + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def undefined_My_struct (lit : Unit) : SailM My_struct := do (pure { field1 := (← sorry) field2 := (← sorry) }) diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean index 3bbf4f93c..65e7a393c 100644 --- a/test/lean/trivial.expected.lean +++ b/test/lean/trivial.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def foo (y : Unit) : Unit := y diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean index 8e040c490..b7dc4dcd0 100644 --- a/test/lean/tuples.expected.lean +++ b/test/lean/tuples.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + def tuple1 : (Int × Int × ((BitVec 2) × Unit)) := (3, 5, ((0b10 : (BitVec 2)), ())) diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean index 6ca3a901c..ea21d16d0 100644 --- a/test/lean/typedef.expected.lean +++ b/test/lean/typedef.expected.lean @@ -8,6 +8,16 @@ def xlen_bytes : Int := 8 def xlenbits := (BitVec 64) + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) := (Sail.BitVec.zeroExtend v m) diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index a89c720bd..6c7baf1fd 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -2,6 +2,16 @@ import Out.Sail.Sail open Sail + +def Register (T : Type) := T +abbrev Regstate := Unit +def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg +def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +abbrev SailM := PreSailM Regstate +def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + /-- Type quantifiers: n : Int -/ def foo (n : Int) : (BitVec 4) := (0xF : (BitVec 4)) From 5e1c0181e549f671a5a68c07bf7aa9ab3def1472 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 22 Jan 2025 14:44:50 +0000 Subject: [PATCH 10/23] fixing lean arrows --- src/sail_lean_backend/Sail/Sail.lean | 8 +++---- src/sail_lean_backend/pretty_print_lean.ml | 14 +++++------ test/lean/bitfield.expected.lean | 6 ++--- test/lean/bitvec_operation.expected.lean | 6 ++--- test/lean/enum.expected.lean | 6 ++--- test/lean/extern.expected.lean | 6 ++--- test/lean/extern_bitvec.expected.lean | 6 ++--- test/lean/let.expected.lean | 6 ++--- test/lean/range.expected.lean | 6 ++--- test/lean/registers.expected.lean | 28 +++++++++++----------- test/lean/struct.expected.lean | 6 ++--- test/lean/trivial.expected.lean | 6 ++--- test/lean/tuples.expected.lean | 6 ++--- test/lean/typedef.expected.lean | 6 ++--- test/lean/typquant.expected.lean | 6 ++--- 15 files changed, 61 insertions(+), 61 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 15d05a377..06b9c5700 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -10,16 +10,16 @@ structure SequentialSate ( Regs : Type ) where abbrev PreSailM ( Regs: Type ) := EStateM Error (SequentialSate Regs) -structure RegisterRef (Register : Type -> Type) (T : Type) where +structure RegisterRef (Register : Type → Type) (T : Type) where reg : Register T -def read_reg {Register : Type -> Type} (register_lookup : ∀ T, Register T -> Regstate -> T) (reg : Register S) : PreSailM Regstate S := do +def read_reg {Register : Type → Type} (register_lookup : ∀ T, Register T → Regstate → T) (reg : Register T) : PreSailM Regstate T := do let r ← get return register_lookup _ reg r.regs -def write_reg {Register : Type -> Type} (register_set : ∀ T, Register T -> T -> Regstate -> Regstate) (reg : Register S) (s : S) : PreSailM Regstate Unit := do +def write_reg {Register : Type → Type} (register_set : ∀ T, Register T → T → Regstate → Regstate) (reg : Register T) (t : T) : PreSailM Regstate Unit := do let r ← get - set { r with regs := register_set _ reg s r.regs } + set { r with regs := register_set _ reg t r.regs } return () def reg_deref {Register : Type → Type} (read_reg : ∀ T, Register T → PreSailM Regstate T) (reg_ref : RegisterRef Register T) : PreSailM Regstate T := do diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 8da876f63..af66b375a 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -585,14 +585,14 @@ let type_enum ctxt env type_map = | _ -> separate hardline [ - string "inductive Register : Type -> Type where"; + string "inductive Register : Type → Type where"; separate_map hardline (fun (typ_id, typ) -> string " | " ^^ doc_id_ctor (reg_case_name typ_id) ^^ space ^^ colon ^^ space ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " -> Register " ^^ doc_typ ctxt typ + ^^ string " → Register " ^^ doc_typ ctxt typ ) type_map; empty; @@ -623,7 +623,7 @@ let regstate ctxt env type_map = ^^ doc_id_ctor (state_field_name typ_id) ^^ string " : " ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " -> " ^^ doc_typ ctxt typ + ^^ string " → " ^^ doc_typ ctxt typ ) type_map; string ""; @@ -643,7 +643,7 @@ let reg_accessors ctxt env type_map = separate hardline [ string "def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg"; - string "def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()"; + string "def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => ()"; ] | _ -> separate hardline @@ -660,7 +660,7 @@ let reg_accessors ctxt env type_map = ) type_map; empty; - string "def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :="; + string "def register_set {T : Type} (reg : Register T) : T → Regstate → Regstate :="; string " match reg with"; separate_map hardline (fun (typ_id, _typ) -> @@ -698,8 +698,8 @@ let doc_reg_info env registers = regstate bare_ctxt env type_map; reg_accessors bare_ctxt env type_map; string "abbrev SailM := PreSailM Regstate"; - string "def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup"; - string "def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set"; + string "def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup"; + string "def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set"; string "def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg"; (* string diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 5c653ba1c..717ce8681 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -8,10 +8,10 @@ def cr_type := (BitVec 8) def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index 6bfc9b812..0261bbb37 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool := diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index 137703592..3f5ae48ee 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -9,10 +9,10 @@ inductive E where | A | B | C def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def undefined_E : SailM E := do diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index 63d959bd6..ab3938e86 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def extern_add : Int := diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean index 8a56386f5..2b962161f 100644 --- a/test/lean/extern_bitvec.expected.lean +++ b/test/lean/extern_bitvec.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def extern_const : (BitVec 64) := diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index 99ae3c6ac..5b92d5749 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def foo : (BitVec 16) := diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean index 21d175436..66acdd77e 100644 --- a/test/lean/range.expected.lean +++ b/test/lean/range.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg /-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/ diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index b5c587149..fa8d169aa 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -29,12 +29,12 @@ deriving DecidableEq open register_nat -inductive Register : Type -> Type where - | R_bit : register_bit -> Register (BitVec 1) - | R_bitvector_64 : register_bitvector_64 -> Register (BitVec 64) - | R_bool : register_bool -> Register Bool - | R_int : register_int -> Register Int - | R_nat : register_nat -> Register Nat +inductive Register : Type → Type where + | R_bit : register_bit → Register (BitVec 1) + | R_bitvector_64 : register_bitvector_64 → Register (BitVec 64) + | R_bool : register_bool → Register Bool + | R_int : register_int → Register Int + | R_nat : register_nat → Register Nat instance : Coe register_bit (Register (BitVec 1)) where coe r := Register.R_bit r @@ -48,11 +48,11 @@ instance : Coe register_nat (Register Nat) where coe r := Register.R_nat r structure Regstate where - bit_s : register_bit -> (BitVec 1) - bitvector_64_s : register_bitvector_64 -> (BitVec 64) - bool_s : register_bool -> Bool - int_s : register_int -> Int - nat_s : register_nat -> Nat + bit_s : register_bit → (BitVec 1) + bitvector_64_s : register_bitvector_64 → (BitVec 64) + bool_s : register_bool → Bool + int_s : register_int → Int + nat_s : register_nat → Nat def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T := @@ -63,7 +63,7 @@ def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T := | Register.R_int r => rs.int_s r | Register.R_nat r => rs.nat_s r -def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate := +def register_set {T : Type} (reg : Register T) : T → Regstate → Regstate := match reg with | Register.R_bit r => fun v rs => { rs with bit_s := fun r' => if r' = r then v else rs.bit_s r' } | Register.R_bitvector_64 r => fun v rs => { rs with bitvector_64_s := fun r' => if r' = r then v else rs.bitvector_64_s r' } @@ -73,8 +73,8 @@ def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate := abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def initialize_registers : SailM Unit := do diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 392403157..73af4f8c3 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -10,10 +10,10 @@ structure My_struct where def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def undefined_My_struct (lit : Unit) : SailM My_struct := do diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean index 65e7a393c..abe3a7b56 100644 --- a/test/lean/trivial.expected.lean +++ b/test/lean/trivial.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def foo (y : Unit) : Unit := diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean index b7dc4dcd0..cadd6ccbd 100644 --- a/test/lean/tuples.expected.lean +++ b/test/lean/tuples.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg def tuple1 : (Int × Int × ((BitVec 2) × Unit)) := diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean index ea21d16d0..a69ee58d7 100644 --- a/test/lean/typedef.expected.lean +++ b/test/lean/typedef.expected.lean @@ -12,10 +12,10 @@ def xlenbits := (BitVec 64) def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/ diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index 6c7baf1fd..4af931f2b 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -6,10 +6,10 @@ open Sail def Register (T : Type) := T abbrev Regstate := Unit def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => () +def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set +def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup +def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg /-- Type quantifiers: n : Int -/ From 8a6f18160f7480ce363654bb68c162c425af5957 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Wed, 22 Jan 2025 15:38:22 +0000 Subject: [PATCH 11/23] small style fix --- src/sail_lean_backend/Sail/Sail.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 06b9c5700..19303130a 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -3,12 +3,12 @@ namespace Sail /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ abbrev Error := Unit -structure SequentialSate ( Regs : Type ) where +structure SequentialSate (Regs : Type) where regs : Regs mem : Unit tags : Unit -abbrev PreSailM ( Regs: Type ) := EStateM Error (SequentialSate Regs) +abbrev PreSailM (Regs : Type) := EStateM Error (SequentialSate Regs) structure RegisterRef (Register : Type → Type) (T : Type) where reg : Register T @@ -19,7 +19,7 @@ def read_reg {Register : Type → Type} (register_lookup : ∀ T, Register T → def write_reg {Register : Type → Type} (register_set : ∀ T, Register T → T → Regstate → Regstate) (reg : Register T) (t : T) : PreSailM Regstate Unit := do let r ← get - set { r with regs := register_set _ reg t r.regs } + set {r with regs := register_set _ reg t r.regs} return () def reg_deref {Register : Type → Type} (read_reg : ∀ T, Register T → PreSailM Regstate T) (reg_ref : RegisterRef Register T) : PreSailM Regstate T := do From 7147adbe9973a6bccd3dc39843e8e45d0378da51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 11:19:00 +0000 Subject: [PATCH 12/23] Changed registers to grouped in a hashmap --- src/sail_lean_backend/Sail/Sail.lean | 28 ++--- src/sail_lean_backend/pretty_print_lean.ml | 128 +++------------------ 2 files changed, 31 insertions(+), 125 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 19303130a..10c0cdaad 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -1,29 +1,29 @@ +import Std.Data.DHashMap namespace Sail /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ abbrev Error := Unit -structure SequentialSate (Regs : Type) where - regs : Regs +structure SequentialSate (Register : Type) (RegisterType : Register → Type) [BEq Register] [Hashable Register] where + regs : Std.DHashMap Register RegisterType mem : Unit tags : Unit -abbrev PreSailM (Regs : Type) := EStateM Error (SequentialSate Regs) +structure RegisterRef (Register : Type) (RegisterType : Register → Type) where + reg : Register -structure RegisterRef (Register : Type → Type) (T : Type) where - reg : Register T +abbrev PreSailM (Register : Type) (RegisterType : Register → Type) [BEq Register] [Hashable Register] := EStateM Error (SequentialSate Register RegisterType) -def read_reg {Register : Type → Type} (register_lookup : ∀ T, Register T → Regstate → T) (reg : Register T) : PreSailM Regstate T := do - let r ← get - return register_lookup _ reg r.regs +def write_reg {RegisterType : Register → Type} [BEq Register] [Hashable Register] (r : Register) (v : RegisterType r) : PreSailM Register RegisterType Unit := + modify fun s => { s with regs := s.regs.insert r v } -def write_reg {Register : Type → Type} (register_set : ∀ T, Register T → T → Regstate → Regstate) (reg : Register T) (t : T) : PreSailM Regstate Unit := do - let r ← get - set {r with regs := register_set _ reg t r.regs} - return () +def read_reg {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] (r : Register) : PreSailM Register RegisterType (RegisterType r) := do + let .some s := (← get).regs.get? r + | throw () + pure s -def reg_deref {Register : Type → Type} (read_reg : ∀ T, Register T → PreSailM Regstate T) (reg_ref : RegisterRef Register T) : PreSailM Regstate T := do - read_reg _ reg_ref.reg +def reg_deref {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] (reg_ref : RegisterRef Register RegisterType) : PreSailM Register RegisterType (RegisterType reg_ref.reg) := do + read_reg reg_ref.reg namespace BitVec diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index af66b375a..728d355d6 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -579,133 +579,39 @@ let per_type_register_enum ctxt typ_id registers = empty; ] -let type_enum ctxt env type_map = - match type_map with - | [] -> string "def Register (T : Type) := T" +let register_enums ctx registers = + match registers with + | [] -> string "abbrev Register := Unit" | _ -> separate hardline [ - string "inductive Register : Type → Type where"; - separate_map hardline - (fun (typ_id, typ) -> - string " | " - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ space ^^ colon ^^ space - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " → Register " ^^ doc_typ ctxt typ - ) - type_map; - empty; - separate_map hardline - (fun (typ_id, typ) -> - string "instance : Coe " - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ space - ^^ parens (string "Register " ^^ doc_typ ctxt typ) - ^^ string " where" ^^ hardline ^^ string " coe r := Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r" - ) - type_map; + string "inductive Register : Type where"; + separate_map hardline (fun (_, id, _) -> string " | " ^^ doc_id_ctor id) registers; + string " deriving DecidableEq, Hashable"; + string "open Register"; empty; ] -let regstate ctxt env type_map = - match type_map with - | [] -> string "abbrev Regstate := Unit" +let type_enum ctx registers = + match registers with + | [] -> string "abbrev RegisterType : Register → Type := fun _ => Unit" | _ -> separate hardline [ - string "structure Regstate where"; + string "abbrev RegisterType : Register → Type"; separate_map hardline - (fun (typ_id, typ) -> - string " " - ^^ doc_id_ctor (state_field_name typ_id) - ^^ string " : " - ^^ doc_id_ctor (reg_type_name typ_id) - ^^ string " → " ^^ doc_typ ctxt typ - ) - type_map; - string ""; - (* doc_field_updates ctxt (mk_typquant []) (mk_id "regstate") - (List.map (fun (typ_id, typ) -> (typ, state_field_name typ_id)) type_map); *) - empty; - (* A record literal can cause problems with record type inference (e.g., if there are no registers) *) - (* string "Definition init_regstate : regstate := Build_regstate"; - separate_map hardline (fun _ -> string " inhabitant") type_map; - string "."; - empty; *) - ] - -let reg_accessors ctxt env type_map = - match type_map with - | [] -> - separate hardline - [ - string "def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg"; - string "def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => ()"; - ] - | _ -> - separate hardline - [ - string "def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :="; - string " match reg with"; - separate_map hardline - (fun (typ_id, _typ) -> - string " | Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r => rs." - ^^ doc_id_ctor (state_field_name typ_id) - ^^ string " r" - ) - type_map; - empty; - string "def register_set {T : Type} (reg : Register T) : T → Regstate → Regstate :="; - string " match reg with"; - separate_map hardline - (fun (typ_id, _typ) -> - string " | Register." - ^^ doc_id_ctor (reg_case_name typ_id) - ^^ string " r => fun v rs => " - ^^ - let field = doc_id_ctor (state_field_name typ_id) in - let fexp = - string " rs with " ^^ field - ^^ string " := fun r' => if r' = r then v else rs." - ^^ field ^^ string " r' " - in - implicit_parens fexp - ) - type_map; - empty; + (fun (typ, id, _) -> string " | ." ^^ doc_id_ctor id ^^ string " => " ^^ doc_typ ctx typ) + registers; empty; ] let doc_reg_info env registers = - let bare_ctxt = initial_context env in - let type_map, type_regs_map = List.fold_left (add_reg_typ env) (Bindings.empty, Bindings.empty) registers in - let type_map = Bindings.bindings type_map in - let type_regs_map = Bindings.bindings type_regs_map in - - let reg_enums = List.fold_left (fun pp (t, rs) -> pp ^^ per_type_register_enum bare_ctxt t rs) empty type_regs_map in + let bare_ctx = initial_context env in separate hardline [ - reg_enums; - type_enum bare_ctxt env type_map; - (* register_refs bare_ctxt env type_regs_map; - empty; - string "(* Definitions to support the lifting to the sequential monad *)"; *) - regstate bare_ctxt env type_map; - reg_accessors bare_ctxt env type_map; - string "abbrev SailM := PreSailM Regstate"; - string "def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup"; - string "def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set"; - string "def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg"; - (* string - - "Definition register_accessors : register_accessors regstate register := (@register_lookup, @register_set)."; - empty; - empty; *) + register_enums bare_ctx registers; + type_enum bare_ctx registers; + string "abbrev SailM := PreSailM Register RegisterType"; ] let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = From e26c834dc9028b4787f2ab189238d782365ea804 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 11:31:59 +0000 Subject: [PATCH 13/23] updated tests --- src/sail_lean_backend/pretty_print_lean.ml | 56 +++++--------- test/lean/bitfield.expected.lean | 32 ++++---- test/lean/bitfield.sail | 2 + test/lean/bitvec_operation.expected.lean | 10 --- test/lean/enum.expected.lean | 10 --- test/lean/extern.expected.lean | 10 --- test/lean/extern_bitvec.expected.lean | 10 --- test/lean/let.expected.lean | 10 --- test/lean/range.expected.lean | 10 --- test/lean/registers.expected.lean | 87 ++++------------------ test/lean/struct.expected.lean | 10 --- test/lean/trivial.expected.lean | 10 --- test/lean/tuples.expected.lean | 10 --- test/lean/typedef.expected.lean | 10 --- test/lean/typquant.expected.lean | 10 --- 15 files changed, 53 insertions(+), 234 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 728d355d6..1b550bebf 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -151,8 +151,7 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) = -> parens (string "BitVec " ^^ doc_nexp ctx m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int" - | Typ_app (Id_aux (Id "register", _), t_app) -> - string "RegisterRef Register " ^^ separate_map comma (doc_typ_app ctx) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef Register RegisterType" | 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 ctx) ts) @@ -566,60 +565,43 @@ let add_reg_typ env (typ_map, regs_map) (typ, id, has_init) = let typ_id = State.id_of_regtyp IdSet.empty typ in (Bindings.add typ_id typ typ_map, Bindings.update typ_id (opt_cons id) regs_map) -let per_type_register_enum ctxt typ_id registers = - let reg_type_id = reg_type_name typ_id in - let reg_type_pp = doc_id_ctor reg_type_id in +let register_enums registers = separate hardline [ - string "inductive " ^^ reg_type_pp ^^ string " where"; - separate_map hardline (fun r -> string " | " ^^ doc_id_ctor r) registers; - string "deriving DecidableEq"; - string "open " ^^ reg_type_pp; - empty; + string "inductive Register : Type where"; + separate_map hardline (fun (_, id, _) -> string " | " ^^ doc_id_ctor id) registers; + string " deriving DecidableEq, Hashable"; + string "open Register"; empty; ] -let register_enums ctx registers = - match registers with - | [] -> string "abbrev Register := Unit" - | _ -> - separate hardline - [ - string "inductive Register : Type where"; - separate_map hardline (fun (_, id, _) -> string " | " ^^ doc_id_ctor id) registers; - string " deriving DecidableEq, Hashable"; - string "open Register"; - empty; - ] - let type_enum ctx registers = - match registers with - | [] -> string "abbrev RegisterType : Register → Type := fun _ => Unit" - | _ -> - separate hardline - [ - string "abbrev RegisterType : Register → Type"; - separate_map hardline - (fun (typ, id, _) -> string " | ." ^^ doc_id_ctor id ^^ string " => " ^^ doc_typ ctx typ) - registers; - empty; - ] + separate hardline + [ + string "abbrev RegisterType : Register → Type"; + separate_map hardline + (fun (typ, id, _) -> string " | ." ^^ doc_id_ctor id ^^ string " => " ^^ doc_typ ctx typ) + registers; + empty; + ] let doc_reg_info env registers = let bare_ctx = initial_context env in separate hardline [ - register_enums bare_ctx registers; + register_enums registers; type_enum bare_ctx registers; string "abbrev SailM := PreSailM Register RegisterType"; + empty; + empty; ] let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in let regs = State.find_registers defs in - let register_refs = doc_reg_info env regs in + let register_refs = match regs with [] -> empty | _ -> doc_reg_info env regs in let types, fundefs = doc_defs (initial_context env) defs in (* let types = separate empty types in let fundefs = separate empty fundefs in *) - print o (types ^^ register_refs ^^ hardline ^^ hardline ^^ fundefs); + print o (types ^^ register_refs ^^ fundefs); () diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index 717ce8681..df1c4ad5f 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -4,15 +4,15 @@ open Sail def cr_type := (BitVec 8) +inductive Register : Type where + | R + deriving DecidableEq, Hashable +open Register -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg +abbrev RegisterType : Register → Type + | .R => (BitVec 8) + +abbrev SailM := PreSailM Register RegisterType def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do sorry @@ -26,7 +26,7 @@ def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 8)) : SailM Unit := do +def _set_cr_type_bits (r_ref : RegisterRef Register RegisterType) (v : (BitVec 8)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ @@ -36,7 +36,7 @@ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 4)) : SailM Unit := do +def _set_cr_type_CR0 (r_ref : RegisterRef Register RegisterType) (v : (BitVec 4)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ @@ -46,7 +46,7 @@ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do +def _set_cr_type_CR1 (r_ref : RegisterRef Register RegisterType) (v : (BitVec 2)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ @@ -56,7 +56,7 @@ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do +def _set_cr_type_CR3 (r_ref : RegisterRef Register RegisterType) (v : (BitVec 2)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ @@ -66,7 +66,7 @@ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do +def _set_cr_type_GT (r_ref : RegisterRef Register RegisterType) (v : (BitVec 1)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ @@ -76,10 +76,10 @@ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Register (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do +def _set_cr_type_LT (r_ref : RegisterRef Register RegisterType) (v : (BitVec 1)) : SailM Unit := do let r ← (reg_deref r_ref) sorry /- deref -/ -def initialize_registers : Unit := - () +def initialize_registers : SailM Unit := do + write_reg R (undefined_cr_type ()) diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail index 2969f5927..53dd33086 100644 --- a/test/lean/bitfield.sail +++ b/test/lean/bitfield.sail @@ -9,3 +9,5 @@ bitfield cr_type : bits(8) = { CR1 : 3 .. 2, CR3 : 1 .. 0 } + +register R : cr_type \ No newline at end of file diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean index 0261bbb37..8f1f7ca93 100644 --- a/test/lean/bitvec_operation.expected.lean +++ b/test/lean/bitvec_operation.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool := (Eq x y) diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean index 3f5ae48ee..637d9c28d 100644 --- a/test/lean/enum.expected.lean +++ b/test/lean/enum.expected.lean @@ -5,16 +5,6 @@ open Sail inductive E where | A | B | C deriving Inhabited - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def undefined_E : SailM E := do sorry diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean index ab3938e86..a67f1c206 100644 --- a/test/lean/extern.expected.lean +++ b/test/lean/extern.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def extern_add : Int := (Int.add 5 4) diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean index 2b962161f..af4bdb0f9 100644 --- a/test/lean/extern_bitvec.expected.lean +++ b/test/lean/extern_bitvec.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def extern_const : (BitVec 64) := (0xFFFF000012340000 : (BitVec 64)) diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean index 5b92d5749..b2eb331d0 100644 --- a/test/lean/let.expected.lean +++ b/test/lean/let.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def foo : (BitVec 16) := let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16))) (HAnd.hAnd (0x0000 : (BitVec 16)) z) diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean index 66acdd77e..6b9b23e3b 100644 --- a/test/lean/range.expected.lean +++ b/test/lean/range.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - /-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/ def f_int (x : Nat) : Int := 0 diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index fa8d169aa..0ac66b78c 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -2,80 +2,25 @@ import Out.Sail.Sail open Sail -inductive register_bit where +inductive Register : Type where | BIT -deriving DecidableEq -open register_bit - -inductive register_bitvector_64 where - | R0 - | R1 -deriving DecidableEq -open register_bitvector_64 - -inductive register_bool where + | NAT | BOOL -deriving DecidableEq -open register_bool - -inductive register_int where | INT -deriving DecidableEq -open register_int - -inductive register_nat where - | NAT -deriving DecidableEq -open register_nat - - -inductive Register : Type → Type where - | R_bit : register_bit → Register (BitVec 1) - | R_bitvector_64 : register_bitvector_64 → Register (BitVec 64) - | R_bool : register_bool → Register Bool - | R_int : register_int → Register Int - | R_nat : register_nat → Register Nat - -instance : Coe register_bit (Register (BitVec 1)) where - coe r := Register.R_bit r -instance : Coe register_bitvector_64 (Register (BitVec 64)) where - coe r := Register.R_bitvector_64 r -instance : Coe register_bool (Register Bool) where - coe r := Register.R_bool r -instance : Coe register_int (Register Int) where - coe r := Register.R_int r -instance : Coe register_nat (Register Nat) where - coe r := Register.R_nat r - -structure Regstate where - bit_s : register_bit → (BitVec 1) - bitvector_64_s : register_bitvector_64 → (BitVec 64) - bool_s : register_bool → Bool - int_s : register_int → Int - nat_s : register_nat → Nat - - -def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T := - match reg with - | Register.R_bit r => rs.bit_s r - | Register.R_bitvector_64 r => rs.bitvector_64_s r - | Register.R_bool r => rs.bool_s r - | Register.R_int r => rs.int_s r - | Register.R_nat r => rs.nat_s r - -def register_set {T : Type} (reg : Register T) : T → Regstate → Regstate := - match reg with - | Register.R_bit r => fun v rs => { rs with bit_s := fun r' => if r' = r then v else rs.bit_s r' } - | Register.R_bitvector_64 r => fun v rs => { rs with bitvector_64_s := fun r' => if r' = r then v else rs.bitvector_64_s r' } - | Register.R_bool r => fun v rs => { rs with bool_s := fun r' => if r' = r then v else rs.bool_s r' } - | Register.R_int r => fun v rs => { rs with int_s := fun r' => if r' = r then v else rs.int_s r' } - | Register.R_nat r => fun v rs => { rs with nat_s := fun r' => if r' = r then v else rs.nat_s r' } - - -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg + | R1 + | R0 + deriving DecidableEq, Hashable +open Register + +abbrev RegisterType : Register → Type + | .BIT => (BitVec 1) + | .NAT => Nat + | .BOOL => Bool + | .INT => Int + | .R1 => (BitVec 64) + | .R0 => (BitVec 64) + +abbrev SailM := PreSailM Register RegisterType def initialize_registers : SailM Unit := do write_reg R0 sorry diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 73af4f8c3..f4703e14c 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -6,16 +6,6 @@ structure My_struct where field1 : Int field2 : (BitVec 1) - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def undefined_My_struct (lit : Unit) : SailM My_struct := do (pure { field1 := (← sorry) field2 := (← sorry) }) diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean index abe3a7b56..3bbf4f93c 100644 --- a/test/lean/trivial.expected.lean +++ b/test/lean/trivial.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def foo (y : Unit) : Unit := y diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean index cadd6ccbd..8e040c490 100644 --- a/test/lean/tuples.expected.lean +++ b/test/lean/tuples.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - def tuple1 : (Int × Int × ((BitVec 2) × Unit)) := (3, 5, ((0b10 : (BitVec 2)), ())) diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean index a69ee58d7..6ca3a901c 100644 --- a/test/lean/typedef.expected.lean +++ b/test/lean/typedef.expected.lean @@ -8,16 +8,6 @@ def xlen_bytes : Int := 8 def xlenbits := (BitVec 64) - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) := (Sail.BitVec.zeroExtend v m) diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean index 4af931f2b..a89c720bd 100644 --- a/test/lean/typquant.expected.lean +++ b/test/lean/typquant.expected.lean @@ -2,16 +2,6 @@ import Out.Sail.Sail open Sail - -def Register (T : Type) := T -abbrev Regstate := Unit -def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg -def register_set {T : Type} (_ : Register T) : T → Regstate → Regstate := fun _ _ => () -abbrev SailM := PreSailM Regstate -def read_reg {T : Type} : Register T → SailM T := @Sail.read_reg _ T _ @register_lookup -def write_reg {T : Type} : Register T → T → SailM Unit := @Sail.write_reg _ T _ @register_set -def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg - /-- Type quantifiers: n : Int -/ def foo (n : Int) : (BitVec 4) := (0xF : (BitVec 4)) From 44f78d8b80b803d86167f42852712ffe4fba02d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 13:16:13 +0000 Subject: [PATCH 14/23] adding section, camelCase function names, regRef functions --- src/sail_lean_backend/Sail/Sail.lean | 27 +++++++++++++++------- src/sail_lean_backend/pretty_print_lean.ml | 6 ++--- test/lean/bitfield.expected.lean | 4 ++-- test/lean/registers.expected.lean | 18 +++++++++------ test/lean/registers.sail | 7 +++++- 5 files changed, 41 insertions(+), 21 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 10c0cdaad..7653d1345 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -1,29 +1,40 @@ import Std.Data.DHashMap namespace Sail +section Regs + +variable {Register : Type} {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] + /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ abbrev Error := Unit -structure SequentialSate (Register : Type) (RegisterType : Register → Type) [BEq Register] [Hashable Register] where +structure SequentialSate where regs : Std.DHashMap Register RegisterType mem : Unit tags : Unit -structure RegisterRef (Register : Type) (RegisterType : Register → Type) where - reg : Register +inductive RegisterRef : Type → Type where + | Reg (r: Register) : RegisterRef (RegisterType r) -abbrev PreSailM (Register : Type) (RegisterType : Register → Type) [BEq Register] [Hashable Register] := EStateM Error (SequentialSate Register RegisterType) +abbrev PreSailM := EStateM Error (SequentialSate (Register := Register) (RegisterType := RegisterType)) -def write_reg {RegisterType : Register → Type} [BEq Register] [Hashable Register] (r : Register) (v : RegisterType r) : PreSailM Register RegisterType Unit := +def writeReg (r : Register) (v : RegisterType r) : PreSailM (Register := Register) (RegisterType := RegisterType) Unit := modify fun s => { s with regs := s.regs.insert r v } -def read_reg {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] (r : Register) : PreSailM Register RegisterType (RegisterType r) := do +def readReg (r : Register) : PreSailM (Register := Register) (RegisterType := RegisterType) (RegisterType r) := do let .some s := (← get).regs.get? r | throw () pure s -def reg_deref {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] (reg_ref : RegisterRef Register RegisterType) : PreSailM Register RegisterType (RegisterType reg_ref.reg) := do - read_reg reg_ref.reg +def readRegRef (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) : PreSailM (Register := Register) (RegisterType := RegisterType) α := do + match reg_ref with | .Reg r => readReg r + +def writeRegRef (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) (a : α) : PreSailM (Register := Register) (RegisterType := RegisterType) Unit := do + match reg_ref with | .Reg r => writeReg r a + +def reg_deref (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) := readRegRef reg_ref + +end Regs namespace BitVec diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 1b550bebf..97d6ff765 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -347,7 +347,7 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = ^^ *) match e with | E_id id -> - if Env.is_register id env then string "read_reg " ^^ doc_id_ctor id + if Env.is_register id env then string "readReg " ^^ doc_id_ctor id else wrap_with_pure as_monadic (string (string_of_id id)) | E_lit l -> wrap_with_pure as_monadic (doc_lit l) | E_app (Id_aux (Id "undefined_int", _), _) (* TODO remove when we handle imports *) @@ -421,7 +421,7 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = (braces (space ^^ doc_exp false ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space)) | E_assign ((LE_aux (le_act, tannot) as le), e) -> ( match le_act with - | LE_id id | LE_typ (_, id) -> string "write_reg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e + | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e | LE_deref e -> string "sorry /- deref -/" | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") ) @@ -591,7 +591,7 @@ let doc_reg_info env registers = [ register_enums registers; type_enum bare_ctx registers; - string "abbrev SailM := PreSailM Register RegisterType"; + string "abbrev SailM := @PreSailM Register RegisterType"; empty; empty; ] diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index df1c4ad5f..ed880e90b 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -12,7 +12,7 @@ open Register abbrev RegisterType : Register → Type | .R => (BitVec 8) -abbrev SailM := PreSailM Register RegisterType +abbrev SailM := @PreSailM Register RegisterType def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do sorry @@ -81,5 +81,5 @@ def _set_cr_type_LT (r_ref : RegisterRef Register RegisterType) (v : (BitVec 1)) sorry /- deref -/ def initialize_registers : SailM Unit := do - write_reg R (undefined_cr_type ()) + writeReg R (undefined_cr_type ()) diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index 0ac66b78c..2de224193 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -20,13 +20,17 @@ abbrev RegisterType : Register → Type | .R1 => (BitVec 64) | .R0 => (BitVec 64) -abbrev SailM := PreSailM Register RegisterType +abbrev SailM := @PreSailM Register RegisterType + +def test : SailM Int := do + writeReg INT (HAdd.hAdd (← readReg INT) 1) + readReg INT def initialize_registers : SailM Unit := do - write_reg R0 sorry - write_reg R1 sorry - write_reg INT sorry - write_reg BOOL sorry - write_reg NAT sorry - write_reg BIT sorry + writeReg R0 sorry + writeReg R1 sorry + writeReg INT sorry + writeReg BOOL sorry + writeReg NAT sorry + writeReg BIT sorry diff --git a/test/lean/registers.sail b/test/lean/registers.sail index 43175ccb3..43907ff6c 100644 --- a/test/lean/registers.sail +++ b/test/lean/registers.sail @@ -7,4 +7,9 @@ register R1 : bits(64) register INT : int register BOOL : bool register NAT : nat -register BIT : bit \ No newline at end of file +register BIT : bit + +function test () -> int = { + INT = INT + 1; + INT +} \ No newline at end of file From eccf1c50a43792028100bfdcb725056e7cf327c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 13:32:14 +0000 Subject: [PATCH 15/23] Moving attributes inside SailM's definition --- src/sail_lean_backend/pretty_print_lean.ml | 2 +- test/lean/bitfield.expected.lean | 2 +- test/lean/registers.expected.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 97d6ff765..7f0a122b1 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -591,7 +591,7 @@ let doc_reg_info env registers = [ register_enums registers; type_enum bare_ctx registers; - string "abbrev SailM := @PreSailM Register RegisterType"; + string "abbrev SailM := @PreSailM Register RegisterType _ _"; empty; empty; ] diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index ed880e90b..c82037fc3 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -12,7 +12,7 @@ open Register abbrev RegisterType : Register → Type | .R => (BitVec 8) -abbrev SailM := @PreSailM Register RegisterType +abbrev SailM := @PreSailM Register RegisterType _ _ def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do sorry diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index 2de224193..c50aa30aa 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -20,7 +20,7 @@ abbrev RegisterType : Register → Type | .R1 => (BitVec 64) | .R0 => (BitVec 64) -abbrev SailM := @PreSailM Register RegisterType +abbrev SailM := @PreSailM Register RegisterType _ _ def test : SailM Int := do writeReg INT (HAdd.hAdd (← readReg INT) 1) From 33cd674dbf64f7e1d1d0f4b55e45ad728c79bb43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 13:33:16 +0000 Subject: [PATCH 16/23] Replacing the Eqs with DecidableEq --- src/sail_lean_backend/Sail/Sail.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 7653d1345..f76aba9b2 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -3,7 +3,7 @@ namespace Sail section Regs -variable {Register : Type} {RegisterType : Register → Type} [BEq Register] [LawfulBEq Register] [Hashable Register] +variable {Register : Type} {RegisterType : Register → Type} [DecidableEq Register] [Hashable Register] /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ abbrev Error := Unit From 059f39a6b7525c3c60128fe5ad4e49d9e5928485 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 13:37:13 +0000 Subject: [PATCH 17/23] reducing bloat in Sail.lean with @ --- src/sail_lean_backend/Sail/Sail.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index f76aba9b2..8fadb9b04 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -16,23 +16,23 @@ structure SequentialSate where inductive RegisterRef : Type → Type where | Reg (r: Register) : RegisterRef (RegisterType r) -abbrev PreSailM := EStateM Error (SequentialSate (Register := Register) (RegisterType := RegisterType)) +abbrev PreSailM := EStateM Error (@SequentialSate Register RegisterType _ _) -def writeReg (r : Register) (v : RegisterType r) : PreSailM (Register := Register) (RegisterType := RegisterType) Unit := +def writeReg (r : Register) (v : RegisterType r) : @PreSailM Register RegisterType _ _ Unit := modify fun s => { s with regs := s.regs.insert r v } -def readReg (r : Register) : PreSailM (Register := Register) (RegisterType := RegisterType) (RegisterType r) := do +def readReg (r : Register) : @PreSailM Register RegisterType _ _ (RegisterType r) := do let .some s := (← get).regs.get? r | throw () pure s -def readRegRef (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) : PreSailM (Register := Register) (RegisterType := RegisterType) α := do +def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : @PreSailM Register RegisterType _ _ α := do match reg_ref with | .Reg r => readReg r -def writeRegRef (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) (a : α) : PreSailM (Register := Register) (RegisterType := RegisterType) Unit := do +def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : @PreSailM Register RegisterType _ _ Unit := do match reg_ref with | .Reg r => writeReg r a -def reg_deref (reg_ref : RegisterRef (Register := Register) (RegisterType := RegisterType) α) := readRegRef reg_ref +def reg_deref (reg_ref : @RegisterRef Register RegisterType α) := readRegRef reg_ref end Regs From bf43b0a3aa6af4ff36220ef57d8e0d11d15fdd7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 14:49:10 +0000 Subject: [PATCH 18/23] Cleaner PreSailM and RegisterState --- src/sail_lean_backend/Sail/Sail.lean | 13 +++++++------ src/sail_lean_backend/pretty_print_lean.ml | 2 +- test/lean/bitfield.expected.lean | 2 +- test/lean/registers.expected.lean | 2 +- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 8fadb9b04..e7ec1cb31 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -8,7 +8,7 @@ variable {Register : Type} {RegisterType : Register → Type} [DecidableEq Regis /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/ abbrev Error := Unit -structure SequentialSate where +structure SequentialState (RegisterType : Register → Type) where regs : Std.DHashMap Register RegisterType mem : Unit tags : Unit @@ -16,20 +16,21 @@ structure SequentialSate where inductive RegisterRef : Type → Type where | Reg (r: Register) : RegisterRef (RegisterType r) -abbrev PreSailM := EStateM Error (@SequentialSate Register RegisterType _ _) +abbrev PreSailM (RegisterType : Register → Type) := + EStateM Error (SequentialState RegisterType) -def writeReg (r : Register) (v : RegisterType r) : @PreSailM Register RegisterType _ _ Unit := +def writeReg (r : Register) (v : RegisterType r) : PreSailM RegisterType Unit := modify fun s => { s with regs := s.regs.insert r v } -def readReg (r : Register) : @PreSailM Register RegisterType _ _ (RegisterType r) := do +def readReg (r : Register) : PreSailM RegisterType (RegisterType r) := do let .some s := (← get).regs.get? r | throw () pure s -def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : @PreSailM Register RegisterType _ _ α := do +def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : PreSailM RegisterType α := do match reg_ref with | .Reg r => readReg r -def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : @PreSailM Register RegisterType _ _ Unit := do +def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : PreSailM RegisterType Unit := do match reg_ref with | .Reg r => writeReg r a def reg_deref (reg_ref : @RegisterRef Register RegisterType α) := readRegRef reg_ref diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 7f0a122b1..f6b5360d0 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -591,7 +591,7 @@ let doc_reg_info env registers = [ register_enums registers; type_enum bare_ctx registers; - string "abbrev SailM := @PreSailM Register RegisterType _ _"; + string "abbrev SailM := PreSailM RegisterType"; empty; empty; ] diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index c82037fc3..be3be12f6 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -12,7 +12,7 @@ open Register abbrev RegisterType : Register → Type | .R => (BitVec 8) -abbrev SailM := @PreSailM Register RegisterType _ _ +abbrev SailM := PreSailM RegisterType def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do sorry diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean index c50aa30aa..145c22e1b 100644 --- a/test/lean/registers.expected.lean +++ b/test/lean/registers.expected.lean @@ -20,7 +20,7 @@ abbrev RegisterType : Register → Type | .R1 => (BitVec 64) | .R0 => (BitVec 64) -abbrev SailM := @PreSailM Register RegisterType _ _ +abbrev SailM := PreSailM RegisterType def test : SailM Int := do writeReg INT (HAdd.hAdd (← readReg INT) 1) From 1a29a4e38a4a09ef1a59e886610259ad8cfe6af5 Mon Sep 17 00:00:00 2001 From: lfrenot Date: Thu, 23 Jan 2025 15:09:57 +0000 Subject: [PATCH 19/23] Small style fixes Co-authored-by: Jakob von Raumer --- src/sail_lean_backend/Sail/Sail.lean | 5 +++-- test/lean/bitfield.sail | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index e7ec1cb31..fafed1243 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -14,7 +14,7 @@ structure SequentialState (RegisterType : Register → Type) where tags : Unit inductive RegisterRef : Type → Type where - | Reg (r: Register) : RegisterRef (RegisterType r) + | Reg (r : Register) : RegisterRef (RegisterType r) abbrev PreSailM (RegisterType : Register → Type) := EStateM Error (SequentialState RegisterType) @@ -30,7 +30,8 @@ def readReg (r : Register) : PreSailM RegisterType (RegisterType r) := do def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : PreSailM RegisterType α := do match reg_ref with | .Reg r => readReg r -def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : PreSailM RegisterType Unit := do +def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : + PreSailM RegisterType Unit := do match reg_ref with | .Reg r => writeReg r a def reg_deref (reg_ref : @RegisterRef Register RegisterType α) := readRegRef reg_ref diff --git a/test/lean/bitfield.sail b/test/lean/bitfield.sail index 53dd33086..70b259e69 100644 --- a/test/lean/bitfield.sail +++ b/test/lean/bitfield.sail @@ -10,4 +10,4 @@ bitfield cr_type : bits(8) = { CR3 : 1 .. 0 } -register R : cr_type \ No newline at end of file +register R : cr_type From 4a6a309c13175bcb052f8bcd892a3e76cd03cc57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 15:11:38 +0000 Subject: [PATCH 20/23] Fixing RegisterRef --- src/sail_lean_backend/Sail/Sail.lean | 4 ++-- src/sail_lean_backend/pretty_print_lean.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index fafed1243..965b9f890 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -13,8 +13,8 @@ structure SequentialState (RegisterType : Register → Type) where mem : Unit tags : Unit -inductive RegisterRef : Type → Type where - | Reg (r : Register) : RegisterRef (RegisterType r) +inductive RegisterRef (RegisterType : Register → Type) : Type → Type where + | Reg (r : Register) : RegisterRef _ (RegisterType r) abbrev PreSailM (RegisterType : Register → Type) := EStateM Error (SequentialState RegisterType) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index f6b5360d0..fbb54eb71 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -151,7 +151,7 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) = -> parens (string "BitVec " ^^ doc_nexp ctx m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int" - | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef Register RegisterType" + | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef RegisterType " ^^ separate_map comma (doc_typ_app ctx) 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 ctx) ts) From 35fd62dda7b7eb247e14d4104a33829b2adbfd80 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 15:15:55 +0000 Subject: [PATCH 21/23] Assign deref support --- src/sail_lean_backend/pretty_print_lean.ml | 2 +- test/lean/bitfield.expected.lean | 24 +++++++++++----------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index fbb54eb71..b3ae04fc0 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -422,7 +422,7 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = | E_assign ((LE_aux (le_act, tannot) as le), e) -> ( match le_act with | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e - | LE_deref e -> string "sorry /- deref -/" + | LE_deref e' -> string "writeRegRef " ^^ doc_exp false ctx e' ^^ space ^^ doc_exp false ctx e | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") ) (* | E_internal_return e -> nest 2 (string "return" ^^ space ^^ nest 5 (doc_exp false ctx e)) *) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index be3be12f6..96f086d2b 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -26,9 +26,9 @@ def _get_cr_type_bits (v : (BitVec 8)) : (BitVec 8) := 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 : RegisterRef Register RegisterType) (v : (BitVec 8)) : SailM Unit := do +def _set_cr_type_bits (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 8)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_bits r v) def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := (Sail.BitVec.extractLsb v 7 4) @@ -36,9 +36,9 @@ def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := 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 : RegisterRef Register RegisterType) (v : (BitVec 4)) : SailM Unit := do +def _set_cr_type_CR0 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 4)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_CR0 r v) def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 3 2) @@ -46,9 +46,9 @@ def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Register RegisterType) (v : (BitVec 2)) : SailM Unit := do +def _set_cr_type_CR1 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_CR1 r v) def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := (Sail.BitVec.extractLsb v 1 0) @@ -56,9 +56,9 @@ def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := 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 : RegisterRef Register RegisterType) (v : (BitVec 2)) : SailM Unit := do +def _set_cr_type_CR3 (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 2)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_CR3 r v) def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 6 6) @@ -66,9 +66,9 @@ def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Register RegisterType) (v : (BitVec 1)) : SailM Unit := do +def _set_cr_type_GT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_GT r v) def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := (Sail.BitVec.extractLsb v 7 7) @@ -76,9 +76,9 @@ def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := 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 : RegisterRef Register RegisterType) (v : (BitVec 1)) : SailM Unit := do +def _set_cr_type_LT (r_ref : RegisterRef RegisterType (BitVec 8)) (v : (BitVec 1)) : SailM Unit := do let r ← (reg_deref r_ref) - sorry /- deref -/ + writeRegRef r_ref (_update_cr_type_LT r v) def initialize_registers : SailM Unit := do writeReg R (undefined_cr_type ()) From 5f1cf9af18ecd25a4513d9d261df65d734d446d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Thu, 23 Jan 2025 15:17:40 +0000 Subject: [PATCH 22/23] formatting --- src/sail_lean_backend/pretty_print_lean.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index b3ae04fc0..7bb06f19d 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -151,7 +151,8 @@ let rec doc_typ ctx (Typ_aux (t, _) as typ) = -> parens (string "BitVec " ^^ doc_nexp ctx m) | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp x, _)]) -> if provably_nneg ctx x then string "Nat" else string "Int" - | Typ_app (Id_aux (Id "register", _), t_app) -> string "RegisterRef RegisterType " ^^ separate_map comma (doc_typ_app ctx) t_app + | Typ_app (Id_aux (Id "register", _), t_app) -> + string "RegisterRef RegisterType " ^^ separate_map comma (doc_typ_app ctx) 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 ctx) ts) From 05ea73d4caca8492a9671a2140d7312add4dd47f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Mon, 27 Jan 2025 10:47:31 +0000 Subject: [PATCH 23/23] Remove commented code --- src/sail_lean_backend/pretty_print_lean.ml | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 7bb06f19d..9cfb18e32 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -343,9 +343,6 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = let field_monadic = effectful (effect_of e) in doc_fexp field_monadic ctx fexp in - (* string (string_of_exp_con full_exp) - ^^ space - ^^ *) match e with | E_id id -> if Env.is_register id env then string "readReg " ^^ doc_id_ctor id @@ -360,12 +357,10 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = (* TODO replace by actual implementation of internal_pick *) string "sorry" | E_internal_plet (pat, e1, e2) -> - (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *) let e0 = doc_pat ctx false pat in let e1_pp = doc_exp false ctx e1 in let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in let e2_pp = doc_exp false ctx e2' in - (* infix 0 1 middle e1_pp e2_pp *) let e0_pp = begin match pat with @@ -387,14 +382,6 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = if effectful (effect_of e) then parens (separate space [doc_exp false ctx e; colon; string "SailM"; doc_typ ctx typ]) else wrap_with_pure as_monadic (parens (separate space [doc_exp false ctx e; colon; doc_typ ctx typ])) - (* | E_typ (typ, e) -> ( - match e with - | E_aux (E_assign _, _) -> doc_exp ctx e - | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) -> - string "return " ^^ nest 7 (parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ])) - | E_aux (E_id id, _) when Env.is_register id (env_of e) -> doc_exp ctx e - | _ -> parens (flow (break 1) [doc_exp ctx e; colon; doc_typ ctx typ]) - ) *) | E_tuple es -> wrap_with_pure as_monadic (parens (separate_map (comma ^^ space) d_of_arg es)) | E_let (LB_aux (LB_val (lpat, lexp), _), e) -> let id = @@ -426,7 +413,6 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) = | LE_deref e' -> string "writeRegRef " ^^ doc_exp false ctx e' ^^ space ^^ doc_exp false ctx e | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet") ) - (* | E_internal_return e -> nest 2 (string "return" ^^ space ^^ nest 5 (doc_exp false ctx e)) *) | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.") and doc_fexp with_arrow ctx (FE_aux (FE_fexp (field, e), _)) = @@ -602,7 +588,5 @@ let pp_ast_lean (env : Type_check.env) ({ defs; _ } as ast : Libsail.Type_check. let regs = State.find_registers defs in let register_refs = match regs with [] -> empty | _ -> doc_reg_info env regs in let types, fundefs = doc_defs (initial_context env) defs in - (* let types = separate empty types in - let fundefs = separate empty fundefs in *) print o (types ^^ register_refs ^^ fundefs); ()