Lean: Fix more tests

src/sail_lean_backend/pretty_print_lean.ml

@@ -49,6 +49,7 @@ let rec fix_id name =
   match name with
   (* Lean keywords to avoid, to expand as needed *)
   | "rec" -> name ^ "'"
+  | "def" -> name ^ "'"
   | "main" ->
       the_main_function_has_been_seen := true;
       "sail_main"
@@ -235,6 +236,8 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
   | 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_app (Id_aux (Id "option", _), [A_aux (A_typ typ, _)]) -> parens (string "Option " ^^ doc_typ ctx typ)
+  | Typ_app (Id_aux (Id "list", _), args) ->
+      parens (string "List" ^^ space ^^ separate_map space (doc_typ_arg ctx `Only_relevant) args)
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctx) ts)
   | Typ_id id -> doc_id_ctor id
   | Typ_app (Id_aux (Id "range", _), [A_aux (A_nexp low, _); A_aux (A_nexp high, _)]) ->
@@ -437,6 +440,7 @@ let rec doc_pat ?(in_vector = false) (P_aux (p, (l, annot)) as pat) =
   | P_struct (pats, _) ->
       let pats = List.map (fun (id, pat) -> separate space [doc_id_ctor id; coloneq; doc_pat pat]) pats in
       braces (space ^^ separate (comma ^^ space) pats ^^ space)
+  | P_cons (hd_pat, tl_pat) -> parens (separate space [doc_pat hd_pat; string "::"; doc_pat tl_pat])
   | _ -> failwith ("Doc Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.")
 
 (* Copied from the Coq PP *)
@@ -658,6 +662,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       ^^ parens (string "fun the_exception => " ^^ hardline ^^ cases)
   | E_assert (e1, e2) -> string "assert " ^^ d_of_arg e1 ^^ space ^^ d_of_arg e2
   | E_list es -> brackets (separate_map comma_sp (doc_exp as_monadic ctx) es)
+  | E_cons (hd_e, tl_e) -> parens (separate space [doc_exp false ctx hd_e; string "::"; doc_exp false ctx tl_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), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp false ctx e

test/lean/run_tests.py

@@ -13,6 +13,7 @@
 from sailtest import *
 
 update_expected = args.update_expected
+run_skips = args.run_skips
 
 sail_dir = get_sail_dir()
 sail = get_sail()
@@ -25,7 +26,6 @@
     'struct_pattern_partial',
     'issue202_1',
     'list_rec_functions2',
-    'list_mut',
     'eq_struct',
     'either_rvbug',
     'bv_literal',
@@ -41,7 +41,6 @@
     'match_bind',
     'sv_dpi',
     'rev_bits_in_byte',
-    'list_let',
     'foreach_none',
     'letbind',
     'enum_map',
@@ -77,7 +76,6 @@
     'constructor247',
     'config_bit',
     'varswap',
-    'empty_list',
     'struct_fn_arg',
     'rv_format2',
     'let_option_shadow',
@@ -100,11 +98,9 @@
     'concurrency_interface',
     'vector_example',
     'reg_init_let',
-    'list_scope',
     'for_shadow',
     'list_torture',
     'rv_format',
-    'list_scope3',
     'option_nest',
     'vector_subrange_pattern',
     'string_literal_type',
@@ -115,9 +111,7 @@
     'bitvector',
     'xlen32',
     'rv_duopod_bug',
-    'warl2',
     'mapping',
-    'list_scope2',
     'issue232_2',
     'poly_int_record',
     'cheri_capreg',
@@ -199,10 +193,14 @@ def test_lean(subdir: str, skip_list = None, runnable: bool = False):
         tests = {}
         for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
+            is_skip = False
 
             if skip_list is not None and basename in skip_list:
-                print_skip(filename)
-                continue
+                if run_skips:
+                    is_skip = True
+                else:
+                    print_skip(filename)
+                    continue
 
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -229,12 +227,15 @@ def test_lean(subdir: str, skip_list = None, runnable: bool = False):
                             step(f'cp {basename}/out/Out.lean {basename}.expected.lean')
                         else:
                             sys.exit(1)
-
-                if runnable:
+                else:
                     status = step_with_status(f'diff {basename}/out/expected {basename}.expect', name=filename)
                     if status != 0:
                         sys.exit(1)
+
                 step('rm -r {}'.format(basename))
+
+                if is_skip:
+                    print(f'{basename} now passes!')
                 print_ok(filename)
                 sys.exit(0)
         results.collect(tests)

test/sailtest.py

@@ -10,6 +10,7 @@
 parser.add_argument("--compact", help="Compact output.", action='store_true')
 parser.add_argument("--targets", help="Targets to use (where supported).", action='append')
 parser.add_argument("--update-expected", help="Update the expected file (where supported)", action="store_true")
+parser.add_argument("--run-skips", help="Run tests that would otherwise be skipped", action="store_true")
 args = parser.parse_args()
 
 def is_compact():