diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index b0034493..9ff208ca 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -228,16 +228,19 @@ 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 ^ "_embed_types" ^ seq_suffix) in - let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in + let monad_modules = + if !Pretty_print_lem.opt_sequential + then ["State_monad"; "State"] + else ["Prompt_monad"; "Prompt"] in let operators_module = "Sail_operators" (* if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" *) in let libs = List.map (fun lib -> lib ^ seq_suffix) libs in let base_imports = [ "Pervasives_extra"; "Sail_impl_base"; "Sail_values"; - operators_module; - monad_module - ] in + operators_module + ] @ monad_modules + in let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in let ((o,_, _) as ext_o) = |