Merge branch 'sail2' into lean-register

src/sail_lean_backend/pretty_print_lean.ml

@@ -380,20 +380,20 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
   | E_app (Id_aux (Id "internal_pick", _), _) ->
       string "sorry" (* TODO replace by actual implementation of internal_pick *)
   | E_internal_plet (pat, e1, e2) ->
-      (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *)
-      let e0 = doc_pat ctxt false pat in
-      let e1_pp = doc_exp ctxt e1 in
-      let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in
-      let e2_pp = doc_exp ctxt 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
+    (* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *)
+    let e0 = doc_pat ctxt false pat in
+    let e1_pp = doc_exp ctxt e1 in
+    let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in
+    let e2_pp = doc_exp ctxt 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")
@@ -494,9 +494,8 @@ 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 ctxt exp]) else doc_exp ctxt exp *)
-  doc_exp ctxt exp
+  let is_monadic = effectful (effect_of exp) in
+  if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp empty_context exp]) else doc_exp empty_context exp
 
 let doc_funcl ctxt funcl =
   let comment, signature = doc_funcl_init ctxt funcl in

test/lean/struct.expected.lean

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