Work around an issue with type abbreviations in HOL

If we use the bitlist representation of bitvectors, the type argument in
type abbreviations such as "bits('n)" becomes dead, which confuses HOL;
as a workaround, expand type synonyms in this case.

5 files changed, 41 insertions, 34 deletions

diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 2aaf5318..5537f42c 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -52,4 +52,4 @@ open Ast
 open Type_check
 
 (* Prints on formatter the defs as Lem Ast nodes *)
-val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
+val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot defs -> string -> unit
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 69c9b9e8..169bd824 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -338,7 +338,14 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | A_nexp n -> doc_nexp_lem (nexp_simp n)
       | A_order o -> empty
       | A_bool _ -> empty
-  in typ', atomic_typ
+  in
+  let top env ty =
+    (* If we use the bitlist representation of bitvectors, the type argument in
+       type abbreviations such as "bits('n)" becomes dead, which confuses HOL; as a
+       workaround, we expand type synonyms in this case. *)
+    let ty' = if !opt_mwords then ty else Env.expand_synonyms env ty in
+    typ' ty'
+  in top, atomic_typ
 
 (* Check for variables in types that would be pretty-printed. *)
 let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
@@ -375,7 +382,7 @@ let doc_tannot_lem ctxt env eff typ =
   match make_printable_type ctxt env typ with
   | None -> empty
   | Some typ ->
-     let ta = doc_typ_lem typ in
+     let ta = doc_typ_lem env typ in
      if eff then string " : M " ^^ parens ta
      else string " : " ^^ ta
 
@@ -475,8 +482,8 @@ let doc_typclasses_lem t =
   if NexpSet.is_empty nexps then (empty, NexpSet.empty) else
   (separate_map comma_sp (fun nexp -> string "Size " ^^ doc_nexp_lem nexp) (NexpSet.elements nexps) ^^ string " => ", nexps)
 
-let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  let pt = doc_typ_lem t in
+let doc_typschm_lem env quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  let pt = doc_typ_lem env t in
   if quants
   then
     let nexps_used = lem_nexps_of_typ t in
@@ -516,7 +523,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
     let doc_p = doc_pat_lem ctxt true p in
     (match make_printable_type ctxt (env_of_annot (l,annot)) typ with
     | None -> doc_p
-    | Some typ -> parens (doc_op colon doc_p (doc_typ_lem typ)))
+    | Some typ -> parens (doc_op colon doc_p (doc_typ_lem (env_of_annot (l,annot)) typ)))
   | P_vector pats ->
      let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in
      if apat_needed then parens ppp else ppp
@@ -950,8 +957,8 @@ let doc_exp_lem, doc_let_lem =
        | Some full_typ, Some r_typ ->
           separate space
             [string ": MR";
-            parens (doc_typ_lem full_typ);
-            parens (doc_typ_lem r_typ)]
+            parens (doc_typ_lem (env_of full_exp) full_typ);
+            parens (doc_typ_lem (env_of r) r_typ)]
        | _ -> empty
       in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
@@ -1005,28 +1012,28 @@ let doc_exp_lem, doc_let_lem =
   in top_exp, let_exp
 
 (*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem (Tu_aux(Tu_ty_id(typ,id),_)) =
+let doc_type_union_lem env (Tu_aux(Tu_ty_id(typ,id),_)) =
   separate space [pipe; doc_id_lem_ctor id; string "of";
-                  parens (doc_typ_lem typ)]
+                  parens (doc_typ_lem env typ)]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
   | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
+let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with
   | TD_abbrev(id,typq,A_aux (A_typ typ, _)) ->
      let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in
      doc_op equals
        (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
-       (doc_typschm_lem false typschm)
+       (doc_typschm_lem env false typschm)
   | TD_abbrev _ -> empty
   | TD_record(id,typq,fs,_) ->
     let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
     let f_pp (typ,fid) =
-      concat [fname fid;space;colon;space;doc_typ_lem typ; semi] in
+      concat [fname fid;space;colon;space;doc_typ_lem env typ; semi] in
     let rectyp = match typq with
       | TypQ_aux (TypQ_tq qs, _) ->
         let quant_item = function
@@ -1085,7 +1092,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
       | Id_aux ((Id "diafp"),_) -> empty *)
       | Id_aux ((Id "option"),_) -> empty
       | _ ->
-         let ar_doc = group (separate_map (break 1) doc_type_union_lem ar) in
+         let ar_doc = group (separate_map (break 1) (doc_type_union_lem env) ar) in
          let typ_pp =
            (doc_op equals)
              (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
@@ -1270,8 +1277,8 @@ let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) arg_typs =
   | _, _ ->
      [pat], identity
 
-let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ)
+let doc_tannot_opt_lem env (Typ_annot_opt_aux(t,_)) = match t with
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem env typ)
   | Typ_annot_opt_none -> empty
 
 let doc_fun_body_lem ctxt exp =
@@ -1366,13 +1373,13 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
-let doc_spec_lem (VS_aux (valspec,annot)) =
+let doc_spec_lem env (VS_aux (valspec,annot)) =
   match valspec with
   | VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
      (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
      if contains_t_pp_var typ then empty else *)
      doc_docstring_lem annot ^^
-     separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem true typschm] ^/^ hardline 
+     separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem env true typschm] ^/^ hardline
   (* | VS_val_spec (_,_,Some _,_) -> empty *)
   | _ -> empty
 
@@ -1419,13 +1426,13 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
   in
   separate_map hardline doc_field fields
 
-let rec doc_def_lem def =
+let rec doc_def_lem type_env def =
   (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
   match def with
-  | DEF_spec v_spec -> doc_spec_lem v_spec
+  | DEF_spec v_spec -> doc_spec_lem type_env v_spec
   | DEF_fixity _ -> empty
   | DEF_overload _ -> empty
-  | DEF_type t_def -> group (doc_typdef_lem t_def) ^/^ hardline
+  | DEF_type t_def -> group (doc_typdef_lem type_env t_def) ^/^ hardline
   | DEF_reg_dec dec -> group (doc_dec_lem dec)
 
   | DEF_default df -> empty
@@ -1444,7 +1451,7 @@ let find_exc_typ defs =
     | _ -> false in
   if List.exists is_exc_typ_def defs then "exception" else "unit"
 
-let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line =
+let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line =
   (* let regtypes = find_regtypes d in *)
   let state_ids =
     State.generate_regstate_defs !opt_mwords defs
@@ -1480,9 +1487,9 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        separate empty (List.map doc_def_lem typdefs); hardline;
+        separate empty (List.map (doc_def_lem type_env) typdefs); hardline;
         hardline;
-        separate empty (List.map doc_def_lem statedefs); hardline;
+        separate empty (List.map (doc_def_lem type_env) statedefs); hardline;
         hardline;
         register_refs; hardline;
         concat [
@@ -1496,5 +1503,5 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs)
         (separate_map hardline)
           (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline;
         hardline;
-        separate empty (List.map doc_def_lem defs);
+        separate empty (List.map (doc_def_lem type_env) defs);
         hardline]);
diff --git a/src/process_file.ml b/src/process_file.ml
index 785d7a18..ed34238b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -275,7 +275,7 @@ let close_output_with_check (o, temp_file_name, file_name) =
 let generated_line f =
   Printf.sprintf "Generated by Sail from %s." f
 
-let output_lem filename libs defs =
+let output_lem filename libs type_env defs =
   let generated_line = generated_line filename in
   (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *)
   let types_module = (filename ^ "_types") in
@@ -315,7 +315,7 @@ let output_lem filename libs defs =
   (Pretty_print.pp_defs_lem
      (ot, base_imports)
      (o, base_imports @ (String.capitalize_ascii types_module :: libs))
-     defs generated_line);
+     type_env defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_o;
   let ((ol, _, _) as ext_ol) =
@@ -351,18 +351,18 @@ let rec iterate (f : int -> unit) (n : int) : unit =
   if n = 0 then ()
   else (f n; iterate f (n - 1))
 
-let output1 libpath out_arg filename defs  =
+let output1 libpath out_arg filename type_env defs  =
   let f' = Filename.basename (Filename.chop_extension filename) in
   match out_arg with
   | Lem_out libs ->
-     output_lem f' libs defs
+     output_lem f' libs type_env defs
   | Coq_out libs ->
      output_coq f' libs defs
 
 let output libpath out_arg files =
   List.iter
-    (fun (f, defs) ->
-      output1 libpath out_arg f defs)
+    (fun (f, type_env, defs) ->
+      output1 libpath out_arg f type_env defs)
     files
 
 let rewrite_step n total defs (name, rewriter) =
diff --git a/src/process_file.mli b/src/process_file.mli
index 1d4d629a..181443fb 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -78,7 +78,7 @@ type out_type =
 val output :
   string ->                           (* The path to the library *)
   out_type ->                         (* Backend kind *)
-  (string * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *)
+  (string * Type_check.Env.t * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *)
   unit
 
 (** [always_replace_files] determines whether Sail only updates modified files.
diff --git a/src/sail.ml b/src/sail.ml
index 9336dfb2..6e5e7556 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -390,13 +390,13 @@ let main() =
          let mwords = !Pretty_print_lem.opt_mwords in
          let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in
          let ast_lem = rewrite_ast_lem ast_lem in
-         output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem]
+         output "" (Lem_out (!opt_libs_lem)) [out_name,type_envs,ast_lem]
        else ());
       (if !(opt_print_coq)
        then
          let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in
          let ast_coq = rewrite_ast_coq ast_coq in
-         output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq]
+         output "" (Coq_out (!opt_libs_coq)) [out_name,type_envs,ast_coq]
        else ());
       (if !(opt_print_latex)
        then