diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Translate.ml | 8 | ||||
| -rw-r--r-- | src/main.ml | 13 |
2 files changed, 16 insertions, 5 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index ab9ed216..ac2ee38c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -29,8 +29,14 @@ type config = { let _ = assert_norm (FUNCTION () = Success ()) ``` *) + use_state_monad : bool; + (** If `true`, use a state-error monad. + If `false`, only use an error monad. + + Using a state-error monad is necessary when modelling I/O, for instance. + *) extract_decreases_clauses : bool; - (** If true, insert `decreases` clauses for all the recursive definitions. + (** If `true`, insert `decreases` clauses for all the recursive definitions. The body of such clauses must be defined by the user. *) diff --git a/src/main.ml b/src/main.ml index 4a111a25..df2d1b0c 100644 --- a/src/main.ml +++ b/src/main.ml @@ -31,8 +31,9 @@ let () = let test_units = ref false in let test_trans_units = ref false in let no_decreases_clauses = ref false in + let no_state = ref false in let template_decreases_clauses = ref false in - let no_split = ref false in + let no_split_files = ref false in let no_check_inv = ref false in let spec = @@ -68,13 +69,16 @@ let () = ( "-no-decreases-clauses", Arg.Set no_decreases_clauses, " Do not add decrease clauses to the recursive definitions" ); + ( "-no-state", + Arg.Set no_state, + " Do not use state-error monads, simply use error monads" ); ( "-template-clauses", Arg.Set template_decreases_clauses, " Generate templates for the required decreases clauses, in a\n\ \ dedicated file. Incompatible with \ -no-decreases-clauses" ); - ( "-no-split", - Arg.Set no_split, + ( "-no-split-files", + Arg.Set no_split_files, " Don't split the definitions between different files for types,\n\ \ functions, etc." ); ( "-no-check-inv", @@ -179,8 +183,9 @@ let () = { Translate.eval_config; mp_config = micro_passes_config; - split_files = not !no_split; + split_files = not !no_split_files; test_unit_functions; + use_state_monad = not !no_state; extract_decreases_clauses = not !no_decreases_clauses; extract_template_decreases_clauses = !template_decreases_clauses; } |