Finish implementing to_monadic

3 files changed, 48 insertions, 13 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 30d4a0a8..90f6dc26 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -468,6 +468,8 @@ type fun_sig = {
   outputs : ty list;
       (** The list of outputs.
 
+          Immediately after the translation from symbolic to pure we have this
+          the following:
           In case of a forward function, the list will have length = 1.
           However, in case of backward function, the list may have length > 1.
           If the length is > 1, it gets extracted to a tuple type. Followingly,
@@ -475,6 +477,9 @@ type fun_sig = {
           want to account for the fact that we immediately deconstruct the tuple
           upon calling the backward function (because the backward function is
           called to update a set of values in the environment).
+          
+          After the "to monadic" pass, the list has size exactly one (and we
+          use the `Result` type).
        *)
 }
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 3b91eaa5..efe26bc4 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -307,18 +307,40 @@ let to_monadic (def : fun_def) : fun_def =
   let body = obj#visit_expression () def.body in
   let def = { def with body } in
 
-  (* Update the signature *)
-  if def.inputs = [] then (
-    assert (def.signature.inputs = []);
-    let signature =
-      { def.signature with inputs = [ SymbolicToPure.unit_ty ] }
-    in
-    let var_cnt = get_expression_min_var_counter def.body in
-    let id, _ = VarId.fresh var_cnt in
-    let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in
-    let inputs = [ var ] in
-    { def with signature; inputs })
-  else def
+  (* Update the signature: first the input types *)
+  let def =
+    if def.inputs = [] then (
+      assert (def.signature.inputs = []);
+      let signature =
+        { def.signature with inputs = [ SymbolicToPure.unit_ty ] }
+      in
+      let var_cnt = get_expression_min_var_counter def.body in
+      let id, _ = VarId.fresh var_cnt in
+      let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in
+      let inputs = [ var ] in
+      { def with signature; inputs })
+    else def
+  in
+  (* Then the output type *)
+  let output_ty =
+    match (def.back_id, def.signature.outputs) with
+    | None, [ out_ty ] ->
+        (* Forward function: there is always exactly one output *)
+        SymbolicToPure.mk_result_ty out_ty
+    | Some _, outputs ->
+        (* Backward function: we have to group them *)
+        SymbolicToPure.mk_result_ty (SymbolicToPure.mk_tuple_ty outputs)
+    | _ -> failwith "Unreachable"
+  in
+  let outputs = [ output_ty ] in
+  let signature = { def.signature with outputs } in
+  { def with signature }
+
+(** Convert the unit variables to `()` if they are used as right-values or
+    `_` if they are used as left values. *)
+let unit_vars_to_unit (def : fun_def) : fun_def =
+  (* TODO *)
+  def
 
 (** Apply all the micro-passes to a function.
 
@@ -349,10 +371,16 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
 
   (* Add unit arguments for functions with no arguments, and change their return type.
    * **Rk.**: from now onwards, the types in the AST are correct (until now,
-   * functions had return type `t` where they should have return type `result t`) *)
+   * functions had return type `t` where they should have return type `result t`).
+   * Also, from now onwards, the outputs list has length 1. x*)
   let def = to_monadic def in
   log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def));
 
+  (* Convert the unit variables to `()` if they are used as right-values or
+   * `_` if they are used as left values. *)
+  let def = unit_vars_to_unit def in
+  log#ldebug (lazy ("unit_vars_to_unit:\n" ^ fun_def_to_string ctx def));
+
   (* Inline the useless variable reassignments *)
   let def = inline_useless_var_reassignments def in
   log#ldebug
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 30142639..345555e7 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -75,6 +75,8 @@ let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue =
   in
   { value; ty }
 
+let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
+
 (** Type substitution *)
 let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty =
   let obj =