Fixing more tests

rems-project · Jan 15, 2025 · abbf08a · abbf08a
1 parent 7be2cb9
commit abbf08a
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 2 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -405,6 +405,8 @@ let rec doc_exp (ctxt : context) (E_aux (e, (l, annot)) as full_exp) =
   | E_typ (typ, e) -> begin
       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])
       | _ -> 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)

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -8,7 +8,9 @@ structure My_struct where
 
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
-  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

diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -1,8 +1,8 @@
 import Out.Sail.Sail
 
-/-- Type quantifiers: n : Int -/
 open Sail
 
+/-- Type quantifiers: n : Int -/
 def foo (n : Int) : BitVec 4 :=
   (0xF : BitVec 4)