diff options
| author | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
| commit | 7ebe7fe5a37959b9004548b4287dbfc1f6faa087 (patch) | |
| tree | ebb50f11d57eb1e95a492c7be1b5dd8e51b7e86e /src/process_file.ml | |
| parent | 63fa9e0e2807e4b5fc3f825e6914a2fab5de37e3 (diff) | |
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.
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) = |