final push before making a clean branch

rems-project · Jan 17, 2025 · 8de8351 · 8de8351
1 parent 573e520
commit 8de8351
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 17 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -406,7 +406,7 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
       match e with
       | E_aux (E_assign _, _) -> doc_exp ctxt e
       | E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) ->
-          string "return " ^^ parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ])
+          string "return " ^^ nest 7 (parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]))
       | _ -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ])
     end
   | E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctxt) es)
@@ -425,8 +425,13 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
   | E_struct_update (exp, fexps) ->
       let args = List.map (doc_fexp ctxt) fexps in
       braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space)
-  | E_assign ((LE_aux (le_act, tannot) as le), e) -> string "set_" ^^ doc_lexp_deref ctxt le ^^ space ^^ doc_exp ctxt e
-  | E_internal_return e -> nest 2 (flow (break 1) [string "return"; doc_exp ctxt e])
+  | E_assign ((LE_aux (le_act, tannot) as le), e) -> (
+      match le_act with
+      | LE_id id | LE_typ (_, id) -> string "set_" ^^ doc_id ctxt id ^^ space ^^ doc_exp ctxt 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 ctxt e))
   | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")
 
 and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor ctxt field ^^ string " := " ^^ doc_exp ctxt exp

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -5,7 +5,7 @@ open Sail
 inductive E where | A | B | C
   deriving Inhabited
 
-def undefined_E : SailM E := do
+def undefined_E : SailM E :=
   return (sorry : E)
 
 def initialize_registers : Unit :=

diff --git a/test/lean/reg.expected.lean b/test/lean/reg.expected.lean
@@ -3,14 +3,14 @@ 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]
 
 open MonadReg
 
-def initialize_registers : SailM Unit := do
+def initialize_registers : SailM Unit :=
   let w__0 := (undefined_bitvector 64)
   set_R0 w__0
-  return ()
+
diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -6,17 +6,11 @@ structure My_struct where
   field1 : Int
   field2 : (BitVec 1)
 
-
-def undefined_My_struct (lit : Unit) : SailM My_struct := do
+def undefined_My_struct (lit : Unit) : SailM My_struct :=
   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
-
-def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
-  {s with field2 := b}
+  return { field1 := w__0
+           field2 := w__1 }
 
 def struct_field2 (s : My_struct) : (BitVec 1) :=
   s.field2