Make minor modifications

5 files changed, 24 insertions, 29 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index 8ce518c9..2cd83db5 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -232,8 +232,7 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
 
 (** The list of assumed functions and all their information:
     - their signature
-    - a boolean indicating whether they are monadic or not (i.e., if they
-      can fail or not)
+    - a boolean indicating whether the function can fail or not
     - their name
 
     Rk.: following what is written above, we don't include `Box::free`.
@@ -282,6 +281,6 @@ let get_assumed_name (id : A.assumed_fun_id) : fun_name =
   let _, _, _, name = get_assumed_info id in
   name
 
-let assumed_is_monadic (id : A.assumed_fun_id) : bool =
+let assumed_can_fail (id : A.assumed_fun_id) : bool =
   let _, _, b, _ = get_assumed_info id in
   b
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 7d298f13..032d65d0 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -485,7 +485,7 @@ let get_fun_effect_info (use_state : bool) (fun_id : A.fun_id)
       { can_fail = true; input_state; output_state }
   | A.Assumed aid ->
       {
-        can_fail = Assumed.assumed_is_monadic aid;
+        can_fail = Assumed.assumed_can_fail aid;
         input_state = false;
         output_state = false;
       }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 01cc37eb..a9bf0a9d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -38,11 +38,9 @@ type config = {
           Note that we later filter the useless *forward* calls in the micro-passes,
           where it is more natural to do.
        *)
-  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.
+  use_state : bool;
+      (** Controls whether we need to use a state to model the external world
+          (I/O, for instance).
        *)
 }
 
@@ -477,7 +475,7 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
 (** Small utility. *)
 let get_fun_effect_info (config : config) (fun_id : A.fun_id)
     (gid : T.RegionGroupId.id option) : fun_effect_info =
-  PureUtils.get_fun_effect_info config.use_state_monad fun_id gid
+  PureUtils.get_fun_effect_info config.use_state fun_id gid
 
 (** Translate a function signature.
 
@@ -1081,7 +1079,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
        * - error-monad: Return x
        * - state-error: Return (state, x)
        * *)
-      if config.use_state_monad then
+      if config.use_state then
         let state_var =
           {
             id = ctx.state_var;
diff --git a/src/Translate.ml b/src/Translate.ml
index d5505894..2390dd69 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -15,11 +15,9 @@ let log = TranslateCore.log
 type config = {
   eval_config : Contexts.partial_config;
   mp_config : Micro.config;
-  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.
+  use_state : bool;
+      (** Controls whether we need to use a state to model the external world
+          (I/O, for instance).
        *)
   split_files : bool;
       (** Controls whether we split the generated definitions between different
@@ -98,7 +96,7 @@ let translate_function_to_symbolics (config : C.partial_config)
     TODO: maybe we should introduce a record for this.
 *)
 let translate_function_to_pure (config : C.partial_config)
-    (mp_config : Micro.config) (use_state_monad : bool) (trans_ctx : trans_ctx)
+    (mp_config : Micro.config) (use_state : bool) (trans_ctx : trans_ctx)
     (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
     : pure_fun_translation =
@@ -182,7 +180,7 @@ let translate_function_to_pure (config : C.partial_config)
     {
       SymbolicToPure.filter_useless_back_calls =
         mp_config.filter_useless_monadic_calls;
-      use_state_monad;
+      use_state;
     }
   in
 
@@ -227,7 +225,7 @@ let translate_function_to_pure (config : C.partial_config)
         (* We need to ignore the forward inputs, and the state input (if there is) *)
         let _, backward_inputs =
           Collections.List.split_at backward_sg.sg.inputs
-            (num_forward_inputs + if use_state_monad then 1 else 0)
+            (num_forward_inputs + if use_state then 1 else 0)
         in
         (* As we forbid nested borrows, the additional inputs for the backward
          * functions come from the borrows in the return value of the rust function:
@@ -276,7 +274,7 @@ let translate_function_to_pure (config : C.partial_config)
   (pure_forward, pure_backwards)
 
 let translate_module_to_pure (config : C.partial_config)
-    (mp_config : Micro.config) (use_state_monad : bool) (m : M.llbc_module) :
+    (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) :
     trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
@@ -320,7 +318,7 @@ let translate_module_to_pure (config : C.partial_config)
     {
       SymbolicToPure.filter_useless_back_calls =
         mp_config.filter_useless_monadic_calls;
-      use_state_monad;
+      use_state;
     }
   in
   let fun_sigs =
@@ -331,8 +329,8 @@ let translate_module_to_pure (config : C.partial_config)
   (* Translate all the *transparent* functions *)
   let pure_translations =
     List.map
-      (translate_function_to_pure config mp_config use_state_monad trans_ctx
-         fun_sigs type_decls_map)
+      (translate_function_to_pure config mp_config use_state trans_ctx fun_sigs
+         type_decls_map)
       m.functions
   in
 
@@ -357,7 +355,7 @@ type gen_ctx = {
 
 type gen_config = {
   mp_config : Micro.config;
-  use_state_monad : bool;
+  use_state : bool;
   extract_types : bool;
   extract_decreases_clauses : bool;
   extract_template_decreases_clauses : bool;
@@ -603,7 +601,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* Translate the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs =
     translate_module_to_pure config.eval_config config.mp_config
-      config.use_state_monad m
+      config.use_state m
   in
 
   (* Initialize the extraction context - for now we extract only to F* *)
@@ -715,14 +713,14 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     }
   in
 
-  let use_state = config.use_state_monad in
+  let use_state = config.use_state in
 
   (* Extract one or several files, depending on the configuration *)
   if config.split_files then (
     let base_gen_config =
       {
         mp_config = config.mp_config;
-        use_state_monad = use_state;
+        use_state;
         extract_types = false;
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses = false;
@@ -812,7 +810,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     let gen_config =
       {
         mp_config = config.mp_config;
-        use_state_monad = use_state;
+        use_state;
         extract_types = true;
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses =
diff --git a/src/main.ml b/src/main.ml
index 8afbc0cd..3fb162f3 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -188,7 +188,7 @@ let () =
           test_unit_functions;
           extract_decreases_clauses = not !no_decreases_clauses;
           extract_template_decreases_clauses = !template_decreases_clauses;
-          use_state_monad = not !no_state;
+          use_state = not !no_state;
         }
       in
       Translate.translate_module filename dest_dir trans_config m