From 4ec8646c1bf426c848e8057cdf7c248df6999523 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 22:03:04 +0100
Subject: Make a minor cleanup

---
 compiler/Pure.ml | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index cc29469a..fc18dbd3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -511,11 +511,16 @@ type fun_effect_info = {
 
 (** Meta information about a function signature *)
 type fun_sig_info = {
-  num_fwd_inputs : int;
-      (** The number of input types for forward computation, ignoring the state *)
-  num_back_inputs : int option;
+  num_fwd_inputs_no_state : int;
+      (** The number of input types for forward computation, ignoring the state (if there is one) *)
+  num_fwd_inputs_with_state : int;
+      (** The number of input types for forward computation, with the state (if there is one) *)
+  num_back_inputs_no_state : int option;
       (** The number of additional inputs for the backward computation (if pertinent),
-          ignoring the state *)
+          ignoring the state (if there is one) *)
+  num_back_inputs_with_state : int option;
+      (** The number of additional inputs for the backward computation (if pertinent),
+          with the state (if there is one) *)
   effect_info : fun_effect_info;
 }
 
@@ -524,14 +529,14 @@ type fun_sig_info = {
     We have the following cases:
     - forward function:
       [in_ty0 -> ... -> in_tyn -> out_ty]                           (* pure function *)
-      `in_ty0 -> ... -> in_tyn -> result out_ty`                    (* error-monad *)
-      `in_ty0 -> ... -> in_tyn -> state -> result (state & out_ty)` (* state-error *)
+      [in_ty0 -> ... -> in_tyn -> result out_ty]                    (* error-monad *)
+      [in_ty0 -> ... -> in_tyn -> state -> result (state & out_ty)] (* state-error *)
     - backward function:
-      `in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm -> (back_out0 & ... & back_outp)` (* pure function *)
-      `in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm ->
-       result (back_out0 & ... & back_outp)` (* error-monad *)
-      `in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
-       result (state & (back_out0 & ... & back_outp))` (* state-error *)
+      [in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm -> (back_out0 & ... & back_outp)] (* pure function *)
+      [in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm ->
+       result (back_out0 & ... & back_outp)] (* error-monad *)
+      [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
+       result (state & (back_out0 & ... & back_outp))] (* state-error *)
        
        Note that a stateful backward function takes two states as inputs: the
        state received by the associated forward function, and the state at which
@@ -543,7 +548,7 @@ type fun_sig_info = {
          (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
        ]}
 
-    The function's type should be given by `mk_arrows sig.inputs sig.output`.
+    The function's type should be given by [mk_arrows sig.inputs sig.output].
     We provide additional meta-information:
     - we divide between forward inputs and backward inputs (i.e., inputs specific
       to the forward functions, and additional inputs necessary if the signature is
@@ -571,8 +576,8 @@ type fun_sig = {
             fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
           ]}
           Decomposed outputs:
-          - forward function:  [T]
-          - backward function: [T; T] (for "x" and "y")
+          - forward function:  [[T]]
+          - backward function: [[T; T]] (for "x" and "y")
           
        *)
   info : fun_sig_info;  (** Additional information *)
-- 
cgit v1.2.3