diff options
| author | Christopher Pulte | 2016-11-28 15:22:25 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2016-11-28 15:22:25 +0000 |
| commit | 45bd517a0c7a7b0a2d51bc9bae575218bfe54534 (patch) | |
| tree | 8352af979c6aa129db4a73cba177fa6ae6c259f6 /src/sail.ml | |
| parent | cf7478cf2ab1251902b0d78322d8588009707c21 (diff) | |
make sail produce prompt and state version of shallow embedding files at the same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 10 |
1 files changed, 0 insertions, 10 deletions
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 |