Finish writing the code which generates the state-error monad

5 files changed, 43 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 53382164..25a8b06f 100644
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,7 @@ test: build translate-no_nested_borrows translate-hashmap translate-paper
 
 # Add specific options to some tests
 translate-no_nested_borrows translate-paper: \
-	TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses
+	TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-state -no-decreases-clauses
 translate-no_nested_borrows translate-paper: SUBDIR:=misc
 translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state
 translate-hashmap: SUBDIR:=hashmap
diff --git a/TODO.md b/TODO.md
index 62eb95d5..3816cda8 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,8 +1,7 @@
 # TODO
 
-0. borrows which are never ended? Drop locals in *symbolic* modes upon return
-
-0. improve variable names generation: "hash_map" -> "hm" (and not just "h")
+0. Improve treatments of error and state error monads. In particular, introduce
+   `return` and `fail`, and remove `Return` and `Fail`.
 
 0. replace all the `failwith` with `raise (Failure ...)`: in CPS, it messes
    up with provenance tracking
diff --git a/src/Pure.ml b/src/Pure.ml
index 96c7d211..bdcb35f8 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -34,6 +34,9 @@ type integer_type = T.integer_type [@@deriving show, ord]
   *)
 type assumed_ty = State | Result | Vec | Option [@@deriving show, ord]
 
+(* TODO: we should never directly manipulate `Return` and `Fail`, but rather
+ * the monadic functions `return` and `fail` (makes treatment of error and
+ * state-error monads more uniform) *)
 let result_return_id = VariantId.of_int 0
 
 let result_fail_id = VariantId.of_int 1
@@ -375,7 +378,15 @@ type unop = Not | Neg of integer_type [@@deriving show, ord]
 type fun_id =
   | Regular of A.fun_id * T.RegionGroupId.id option
       (** Backward id: `Some` if the function is a backward function, `None`
-          if it is a forward function *)
+          if it is a forward function.
+
+          TODO: we need to redefine A.fun_id here, to add `fail` and
+          `return` (important to get a unified treatment of the state-error
+          monad). For now, when using the state-error monad: extraction
+          works only if we unfold all the monadic let-bindings, and we
+          then replace the content of the occurrences of `Return` to also
+          return the state (which is really super ugly).
+       *)
   | Unop of unop
   | Binop of E.binop * integer_type
 [@@deriving show, ord]
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 61d247ea..6c61b9dc 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1008,6 +1008,31 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
             let switch_body = Match [ fail_branch; success_branch ] in
             let e = Switch (re, switch_body) in
             self#visit_expression state_var e
+
+      method! visit_Value state_var rv mp =
+        if config.use_state_monad then
+          match rv.ty with
+          | Adt (Assumed Result, _) -> (
+              match rv.value with
+              | RvAdt av ->
+                  (* We only need to replace the content of `Return ...` *)
+                  (* TODO: type checking is completely broken at this point... *)
+                  let variant_id = Option.get av.variant_id in
+                  if variant_id = result_return_id then
+                    let res_v = Collections.List.to_cons_nil av.field_values in
+                    let state_value = mk_typed_rvalue_from_var state_var in
+                    let res = mk_simpl_tuple_rvalue [ state_value; res_v ] in
+                    let res = mk_result_return_rvalue res in
+                    (mk_value_expression res None).e
+                  else super#visit_Value state_var rv mp
+              | _ -> raise (Failure "Unrechable"))
+          | _ -> super#visit_Value state_var rv mp
+        else super#visit_Value state_var rv mp
+      (** We also need to update values, in case this value is `Return ...`.
+
+            TODO: this is super ugly... We need to use the monadic functions
+           `fail` and `return` instead.
+         *)
     end
   in
   (* Update the body *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index f2ed1053..5709ce23 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -972,6 +972,9 @@ and translate_return (_config : config) (opt_v : V.typed_value option)
       (* Forward function *)
       let v = Option.get opt_v in
       let v = typed_value_to_rvalue ctx v in
+      (* TODO: we need to use a `return` function (otherwise we have problems
+       * with the state-error monad). We also need to update the type when using
+       * a state-error monad. *)
       let v = mk_result_return_rvalue v in
       let e = Value (v, None) in
       let ty = v.ty in