diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml index 12e90dd9..0464fc22 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -52,6 +52,7 @@ 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) @@ -68,7 +69,10 @@ let options = Arg.align ([ " pretty-print a Lem AST representation of the file"); ( "-lem", Arg.Set opt_print_lem, - " print a Lem translated version of the specification"); + " 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"); @@ -133,6 +137,12 @@ let main() = if !(opt_libs_lem) = [] 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 |