changes after merge

lfrenot · Jan 14, 2025 · 4613fb6 · 4613fb6
1 parent 4d6d31d
commit 4613fb6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/src/lib/state.ml b/src/lib/state.ml
@@ -835,7 +835,7 @@ 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 m] [Monad m]"; ""; "open MonadReg"; ""] in
+  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
@@ -847,19 +847,19 @@ let register_refs_lean doc_id doc_typ registers =
         colon;
         space;
         typp;
-        string " -> m Unit";
+        string " -> SailM Unit";
         hardline;
         string "  get_";
         idd;
         colon;
         space;
-        string "m (";
+        string "SailM (";
         typp;
         string ")";
       ]
   in
   let refs = separate_map hardline register_ref registers in
-  separate hardline [string "class MonadReg (m : Type -> Type) where"; refs; generic_convs]
+  separate hardline [string "class MonadReg where"; refs; generic_convs]
 
 let generate_regstate_defs ctx env ast =
   let defs = ast.defs in

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -478,7 +478,7 @@ let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) =
     else empty
   in
   (* Use auto-implicits for type quanitifiers for now and see if this works *)
-  let doc_ret_typ = doc_typ ret_typ in
+  let doc_ret_typ = doc_typ ctxt ret_typ in
   let is_monadic = effectful (effect_of exp) in
   (* Add monad for stateful functions *)
   let doc_ret_typ = if is_monadic then string "SailM " ^^ doc_ret_typ else doc_ret_typ in
@@ -490,11 +490,11 @@ let doc_funcl_init ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) =
 let doc_funcl_body ctxt (FCL_aux (FCL_funcl (id, pexp), annot)) =
   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 exp]) else doc_exp exp
+  if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp ctxt exp]) else doc_exp ctxt exp
 
 let doc_funcl ctxt funcl =
-  let comment, signature = doc_funcl_init ctxt funcl in
-  comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl)
+  let signature = doc_funcl_init ctxt funcl in
+  nest 2 (signature ^^ hardline ^^ doc_funcl_body ctxt funcl)
 
 let doc_fundef ctxt (FD_aux (FD_function (r, typa, fcls), fannot)) =
   match fcls with