summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile9
-rw-r--r--src/pretty_print.ml40
-rw-r--r--src/pretty_print.mli2
-rw-r--r--src/process_file.ml57
-rw-r--r--src/process_file.mli1
-rw-r--r--src/sail.ml10
6 files changed, 64 insertions, 55 deletions
diff --git a/src/Makefile b/src/Makefile
index 4f16f2b9..573bef36 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -60,16 +60,11 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
cd _build ;\
../sail.native -lem_ast -o mips $(MIPS_SAILS)
-_build/mips_embedded.lem: $(MIPS_SAILS) ./sail.native
+_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
-_build/mips_sequential_embedded.lem: $(MIPS_SAILS) ./sail.native
- mkdir -p _build
- cd _build ;\
- ../sail.native -lem_lib "Mips_extras_sequential_embed" -lem_sequential -o mips $(MIPS_NOTLB_SAILS)
-
_build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
mkdir -p _build
cd _build ; \
@@ -101,7 +96,7 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native
-mips_notlb: _build/mips_notlb.ml _build/mips_embedded.lem _build/mips_sequential_embedded.lem _build/mips_extras.ml
+mips_notlb: _build/mips_notlb.ml _build/mips_embed_types.lem _build/mips_extras.ml
true
mips: elf run_mips.native
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 65650a33..9c9ad1f4 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -3057,17 +3057,19 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
let doc_def_lem regtypes def = match def with
- | DEF_default df -> empty
- | DEF_spec v_spec -> doc_spec_lem regtypes v_spec
- | DEF_type t_def -> group (doc_typdef_lem regtypes t_def) ^/^ hardline
- | DEF_fundef f_def -> group (doc_fundef_lem regtypes f_def) ^/^ hardline
- | DEF_val lbind -> group (doc_let_lem regtypes lbind) ^/^ hardline
- | DEF_reg_dec dec -> group (doc_dec_lem dec)
+ | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty)
+ | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty)
+ | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
+
+ | DEF_default df -> (empty,empty)
+ | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
+ | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline)
| DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
let doc_defs_lem regtypes (Defs defs) =
- separate_map empty (doc_def_lem regtypes) defs
+ let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
+ (separate empty typdefs,separate empty valdefs)
let find_regtypes (Defs defs) =
List.fold_left
@@ -3081,14 +3083,14 @@ let find_regtypes (Defs defs) =
let typ_to_t env =
Type_check.typ_to_t env false false
-let pp_defs_lem f d top_line opens =
+let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line =
let regtypes = find_regtypes d in
- let defs = doc_defs_lem regtypes d in
- (print f)
+ let (typdefs,valdefs) = doc_defs_lem regtypes d in
+ (print types_file)
(concat
[string "(*" ^^ (string top_line) ^^ string "*)";hardline;
(separate_map hardline)
- (fun lib -> separate space [string "open import";string lib]) opens;hardline;
+ (fun lib -> separate space [string "open import";string lib]) types_modules;hardline;
(separate_map hardline)
(fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; hardline;
hardline;
@@ -3096,4 +3098,18 @@ let pp_defs_lem f d top_line opens =
string "module SIA = Interp_ast"; hardline;
string "module SV = Sail_values"; hardline;
hardline;
- defs])
+ typdefs]);
+ (print prompt_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline;
+ hardline;
+ valdefs]);
+ (print state_file)
+ (concat
+ [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+ (separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
+ hardline;
+ valdefs]);
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 4b51db8a..500d19e2 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -10,4 +10,4 @@ val pat_to_string : tannot pat -> string
val pp_lem_defs : Format.formatter -> tannot defs -> unit
val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
-val pp_defs_lem : out_channel -> tannot defs -> string -> string list -> unit
+val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/process_file.ml b/src/process_file.ml
index 8f5dec40..7bd7e134 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -49,7 +49,6 @@ open Type_internal
type out_type =
| Lem_ast_out
| Lem_out of string option
- | Lem_sequential_out of string option
| Ocaml_out of string option
let get_lexbuf fn =
@@ -175,33 +174,43 @@ let output1 libpath out_arg filename defs =
close_output_with_check ext_o
end
| Lem_out None ->
+ let generated_line = generated_line filename in
+ let types_module = (f' ^ "_embed_types") in
let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (f' ^ "_embedded.lem") in
- (Pretty_print.pp_defs_lem o defs (generated_line filename))
- ["Pervasives_extra";"Sail_impl_base";"Prompt";
- "Sail_values";"Deep_shallow_convert"];
- close_output_with_check ext_o
- | Lem_out (Some lib) ->
- let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (f' ^ "_embedded.lem") in
- (Pretty_print.pp_defs_lem o defs (generated_line filename))
- ["Pervasives_extra";"Sail_impl_base";"Prompt";
- "Sail_values";"Deep_shallow_convert";lib];
+ open_output_with_check_unformatted (f' ^ "_embed_types.lem") in
+ let ((o',_, _) as ext_o') =
+ open_output_with_check_unformatted (f' ^ "_embed.lem") in
+ let ((o'',_, _) as ext_o'') =
+ open_output_with_check_unformatted (f' ^ "embed_sequential.lem") in
+ (Pretty_print.pp_defs_lem
+ (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert"])
+ (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";
+ String.capitalize types_module])
+ (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values";
+ String.capitalize types_module])
+ defs generated_line);
close_output_with_check ext_o;
- | Lem_sequential_out None ->
- let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
- (Pretty_print.pp_defs_lem o defs (generated_line filename))
- ["Pervasives_extra";"Sail_impl_base";"State";
- "Sail_values";"Deep_shallow_convert"];
- close_output_with_check ext_o
- | Lem_sequential_out (Some lib) ->
+ close_output_with_check ext_o';
+ close_output_with_check ext_o'';
+ | Lem_out (Some lib) ->
+ let generated_line = generated_line filename in
+ let types_module = (f' ^ "_embed_types") in
let ((o,_, _) as ext_o) =
- open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
- (Pretty_print.pp_defs_lem o defs (generated_line filename))
- ["Pervasives_extra";"Sail_impl_base";"State";
- "Sail_values";"Deep_shallow_convert";lib];
+ open_output_with_check_unformatted (f' ^ "_embed_types.lem") in
+ let ((o',_, _) as ext_o') =
+ open_output_with_check_unformatted (f' ^ "_embed.lem") in
+ let ((o'',_, _) as ext_o'') =
+ open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in
+ (Pretty_print.pp_defs_lem
+ (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert";lib])
+ (o',["Pervasives_extra";"Sail_impl_base";"Prompt";
+ "Sail_values";String.capitalize types_module;lib])
+ (o'',["Pervasives_extra";"Sail_impl_base";"State";
+ "Sail_values";String.capitalize types_module;lib ^ "_sequential"])
+ defs generated_line);
close_output_with_check ext_o;
+ close_output_with_check ext_o';
+ close_output_with_check ext_o''
| Ocaml_out None ->
let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];
diff --git a/src/process_file.mli b/src/process_file.mli
index 52c5474e..66b1d8af 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -55,7 +55,6 @@ val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot As
type out_type =
| Lem_ast_out
| Lem_out of string option (* If present, the string is a file to open in the lem backend*)
- | Lem_sequential_out of string option (* If present, the string is a file to open in the lem backend*)
| Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*)
val output :
diff --git a/src/sail.ml b/src/sail.ml
index 0464fc22..80560746 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -52,7 +52,6 @@ let opt_print_version = ref false
let opt_print_verbose = ref false
let opt_print_lem_ast = ref false
let opt_print_lem = ref false
-let opt_print_lem_sequential = ref false
let opt_print_ocaml = ref false
let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
@@ -70,9 +69,6 @@ let options = Arg.align ([
( "-lem",
Arg.Set opt_print_lem,
" print a Lem translated version of the specification to integrate with a concurrency model");
- ( "-lem_sequential",
- Arg.Set opt_print_lem_sequential,
- " print a Lem translated version of the specification as a sequential model");
( "-ocaml",
Arg.Set opt_print_ocaml,
" print an Ocaml translated version of the specification");
@@ -138,12 +134,6 @@ let main() =
then output "" (Lem_out None) [out_name,ast_lem]
else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
else ());
- (if !(opt_print_lem_sequential)
- then let ast_lem = rewrite_ast_lem ast in
- if !(opt_libs_lem) = []
- then output "" (Lem_sequential_out None) [out_name,ast_lem]
- else output "" (Lem_sequential_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
- else ())
end
let _ = try
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 10:25:33 +0000