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.

1 files changed, 31 insertions, 24 deletions

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]);