From e3430dcb5e944af0903b272669e6ddbb8e7d59c3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 23 Feb 2022 22:23:45 +0100
Subject: Add an option to control the translation to error monad or
 state-error monad

---
 src/Translate.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/Translate.ml')

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.
        *)
-- 
cgit v1.2.3