diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 41 | ||||
| -rw-r--r-- | src/process_file.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 6 |
4 files changed, 29 insertions, 23 deletions
diff --git a/src/Makefile b/src/Makefile index 4147b10c..6cfcf874 100644 --- a/src/Makefile +++ b/src/Makefile @@ -173,7 +173,7 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native _build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native mkdir -p _build cd _build ;\ - ../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS) + ../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS) _build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem cd _build ;\ diff --git a/src/process_file.ml b/src/process_file.ml index 46b6538e..0f789c9d 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -41,6 +41,8 @@ (**************************************************************************) let opt_new_parser = ref false +let opt_lem_sequential = ref false +let opt_lem_mwords = ref false type out_type = | Lem_ast_out @@ -136,31 +138,28 @@ let generated_line f = let output_lem filename libs defs = let generated_line = generated_line filename in - let types_module = (filename ^ "_embed_types") in - let types_module_seq = (filename ^ "_embed_types_sequential") in - let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in + let seq_suffix = if !opt_lem_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 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 let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_embed_types.lem") in - let ((ots,_, _) as ext_ots) = - open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in + open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ "_embed.lem") in - let ((os,_, _) as ext_os) = - open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem false false - (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"]) - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"; - String.capitalize types_module] @ libs) - defs generated_line); - (Pretty_print.pp_defs_lem true true - (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"]) - (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"; - String.capitalize types_module_seq] @ libs_seq) + open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in + (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords + (ot, base_imports) + (o, base_imports @ (String.capitalize types_module :: libs)) defs generated_line); close_output_with_check ext_ot; - close_output_with_check ext_ots; - close_output_with_check ext_o; - close_output_with_check ext_os + close_output_with_check ext_o let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in diff --git a/src/process_file.mli b/src/process_file.mli index cd867b0d..53a6f3f2 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -52,6 +52,8 @@ val load_file_no_check : Ast.order -> string -> unit Ast.defs val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t val opt_new_parser : bool ref +val opt_lem_sequential : bool ref +val opt_lem_mwords : bool ref val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref @@ -73,4 +75,3 @@ val output : files existed before. If it is set to [false] and an output file already exists, the output file is only updated, if its content really changes. *) val always_replace_files : bool ref - diff --git a/src/sail.ml b/src/sail.ml index 5e979738..56c29819 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -73,6 +73,12 @@ let options = Arg.align ([ ( "-ocaml_lib", Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), "<filename> provide additional library to open in OCaml output"); + ( "-lem_sequential", + Arg.Set Process_file.opt_lem_sequential, + " use sequential state monad for Lem output"); + ( "-lem_mwords", + Arg.Set Process_file.opt_lem_mwords, + " use native machine word library for Lem output"); (* ( "-i", Arg.String (fun l -> lib := l::!lib), |