From 2ef7c31074720997bbc519e44e34c076677ab282 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 14 Dec 2017 16:48:05 +0000 Subject: Make sequential and mwords global variables in Lem pretty-printer --- src/process_file.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'src/process_file.ml') diff --git a/src/process_file.ml b/src/process_file.ml index 68e5786e..44f2e832 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -49,8 +49,6 @@ (**************************************************************************) let opt_new_parser = ref false -let opt_lem_sequential = ref false -let opt_lem_mwords = ref false type out_type = | Lem_ast_out @@ -130,7 +128,7 @@ let opt_dmono_analysis = ref 0 let opt_auto_mono = ref false let monomorphise_ast locs type_env ast = - let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis) + let ast = Monomorphise.monomorphise (!Pretty_print_lem.opt_mwords) (!opt_auto_mono) (!opt_dmono_analysis) locs type_env ast in let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in @@ -159,10 +157,10 @@ let generated_line f = let output_lem filename libs defs = let generated_line = generated_line filename in - let seq_suffix = if !opt_lem_sequential then "_sequential" else "" 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 !opt_lem_sequential then "State" else "Prompt" in - let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in + let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in + let operators_module = 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"; @@ -175,7 +173,7 @@ let output_lem filename libs defs = open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in let ((o,_, _) as ext_o) = open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in - (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords + (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize types_module :: libs)) defs generated_line); @@ -233,7 +231,7 @@ let rewrite rewriters defs = raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err)) let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] -let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)] +let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil -- cgit v1.2.3 From 5cd77a145b886e614d4b5cb46e53d42736cc6865 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 18 Dec 2017 14:28:02 +0000 Subject: Handle multiple -lem_lib options --- src/process_file.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/process_file.ml') diff --git a/src/process_file.ml b/src/process_file.ml index 44f2e832..a1ce00ff 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,7 +52,7 @@ let opt_new_parser = ref false type out_type = | Lem_ast_out - | Lem_out of string option + | Lem_out of string list option let get_lexbuf f = let in_chan = open_in f in @@ -201,8 +201,8 @@ let output1 libpath out_arg filename defs = end | Lem_out None -> output_lem f' [] defs - | Lem_out (Some lib) -> - output_lem f' [lib] defs + | Lem_out (Some libs) -> + output_lem f' libs defs let output libpath out_arg files = List.iter -- cgit v1.2.3 From fb12f81bc8c682439a440e3939c7ae029d91fd5e Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 18 Dec 2017 14:32:09 +0000 Subject: Clean up last commit --- src/process_file.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'src/process_file.ml') diff --git a/src/process_file.ml b/src/process_file.ml index a1ce00ff..83cfd8a3 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,7 +52,7 @@ let opt_new_parser = ref false type out_type = | Lem_ast_out - | Lem_out of string list option + | Lem_out of string list let get_lexbuf f = let in_chan = open_in f in @@ -199,9 +199,7 @@ let output1 libpath out_arg filename defs = Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o end - | Lem_out None -> - output_lem f' [] defs - | Lem_out (Some libs) -> + | Lem_out libs -> output_lem f' libs defs let output libpath out_arg files = -- cgit v1.2.3