diff options
author | Son Ho | 2022-02-23 22:23:45 +0100 |
---|---|---|
committer | Son Ho | 2022-02-23 22:23:45 +0100 |
commit | e3430dcb5e944af0903b272669e6ddbb8e7d59c3 (patch) | |
tree | b538fc2151d7a7fb01b94ef9a5c7b29925f3c1c0 /src/Translate.ml | |
parent | 284a6042ca9d5d7bcbc19a10909156769443c9be (diff) |
Add an option to control the translation to error monad or state-error
monad
Diffstat (limited to 'src/Translate.ml')
-rw-r--r-- | src/Translate.ml | 8 |
1 files changed, 7 insertions, 1 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. *) |