diff options
| author | Jon French | 2018-06-14 16:37:31 +0100 |
|---|---|---|
| committer | Jon French | 2018-06-14 16:37:31 +0100 |
| commit | 1bb5fcf93261f2de51909ff51bf229d21e4b13a6 (patch) | |
| tree | 85dad0aa6f1d29ede74aa5ec929552be7898653a /src/process_file.ml | |
| parent | b58c7dd97ab2a22002cc34ab25a558057834c31c (diff) | |
rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 710655c4..5ceb2a5c 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -279,17 +279,17 @@ let output_lem filename libs 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 - let monad_modules = ["Prompt_monad"; "Prompt"] in + let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"] in let operators_module = if !Pretty_print_lem.opt_mwords - then "Sail_operators_mwords" - else "Sail_operators_bitlists" in + then "Sail2_operators_mwords" + else "Sail2_operators_bitlists" in (* let libs = List.map (fun lib -> lib ^ seq_suffix) libs in *) let base_imports = [ "Pervasives_extra"; - "Sail_instr_kinds"; - "Sail_values"; - "Sail_string"; + "Sail2_instr_kinds"; + "Sail2_values"; + "Sail2_string"; operators_module ] @ monad_modules in @@ -298,8 +298,8 @@ let output_lem filename libs defs = separate hardline [ string ("theory " ^ isa_thy_name); string " imports"; - string " Sail.Sail_values_lemmas"; - string " Sail.State_lemmas"; + string " Sail.Sail2_values_lemmas"; + string " Sail.Sail2_state_lemmas"; string (" " ^ String.capitalize filename); string "begin"; string ""; @@ -326,11 +326,11 @@ let output_lem filename libs defs = let output_coq filename libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in - let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in - let operators_module = "Sail_operators_mwords" in + let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in + let operators_module = "Sail2_operators_mwords" in let base_imports = [ - "Sail_instr_kinds"; - "Sail_values"; + "Sail2_instr_kinds"; + "Sail2_values"; operators_module ] @ monad_modules in |