diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 55 | ||||
| -rw-r--r-- | src/process_file.ml | 12 | ||||
| -rw-r--r-- | src/process_file.mli | 2 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
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 |