Make a minor cleanup

10 files changed, 63 insertions, 61 deletions

diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index a995d4a6..fc04ce90 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1456,16 +1456,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
        *)
       let inputs_lvs =
         let all_inputs = (Option.get def.body).inputs_lvs in
-        (* We have to count:
-         * - the forward inputs
-         * - the state (if there is one)
-         *)
-        let num_fwd_inputs = def.signature.info.num_fwd_inputs in
-        let num_fwd_inputs =
-          if def.signature.info.effect_info.stateful_group then
-            1 + num_fwd_inputs
-          else num_fwd_inputs
-        in
+        let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in
         Collections.List.prefix num_fwd_inputs all_inputs
       in
       let _ =
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 *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 74bc20ae..6b44a69c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -644,11 +644,23 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   (* Type parameters *)
   let type_params = sg.type_params in
   (* Return *)
+  let num_fwd_inputs_no_state = List.length fwd_inputs in
+  let num_back_inputs_no_state =
+    if bid = None then None else Some (List.length back_inputs)
+  in
   let info =
     {
-      num_fwd_inputs = List.length fwd_inputs;
-      num_back_inputs =
-        (if bid = None then None else Some (List.length back_inputs));
+      num_fwd_inputs_no_state;
+      num_fwd_inputs_with_state =
+        (* We use the fact that [fwd_state_ty] has length 1 if there is a state,
+           and 0 otherwise *)
+        num_fwd_inputs_no_state + List.length fwd_state_ty;
+      num_back_inputs_no_state;
+      num_back_inputs_with_state =
+        (* Length of [back_state_ty]: similar trick as for [fwd_state_ty] *)
+        Option.map
+          (fun n -> n + List.length back_state_ty)
+          num_back_inputs_no_state;
       effect_info;
     }
   in
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 453e02db..e943c78a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -134,7 +134,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   in
 
   (* We need to initialize the input/output variables *)
-  let num_forward_inputs = List.length fdef.signature.inputs in
   let add_forward_inputs input_svs ctx =
     match fdef.body with
     | None -> ctx
@@ -189,23 +188,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
           RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
         in
         (* We need to ignore the forward inputs, and the state input (if there is) *)
-        let fun_info =
-          SymbolicToPure.get_fun_effect_info fun_context.fun_infos
-            (A.Regular def_id) (Some back_id)
-        in
         let backward_inputs =
+          let sg = backward_sg.sg in
           (* We need to ignore the forward state and the backward state *)
-          (* TODO: this is ad-hoc and error-prone. We should group all this
-           * information in the signature information. *)
-          let fwd_state_n = if fun_info.stateful_group then 1 else 0 in
-          let num_forward_inputs = num_forward_inputs + fwd_state_n in
-          let back_state_n = if fun_info.stateful then 1 else 0 in
-          let num_back_inputs =
-            List.length backward_sg.sg.inputs
-            - num_forward_inputs - back_state_n
-          in
-          Collections.List.subslice backward_sg.sg.inputs num_forward_inputs
-            num_back_inputs
+          let num_forward_inputs = sg.info.num_fwd_inputs_with_state in
+          let num_back_inputs = Option.get sg.info.num_back_inputs_no_state in
+          Collections.List.subslice sg.inputs num_forward_inputs num_back_inputs
         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:
diff --git a/compiler/fstar/Primitives.fst b/compiler/fstar/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/compiler/fstar/Primitives.fst
+++ b/compiler/fstar/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/betree_back_stateful/Primitives.fst b/tests/betree_back_stateful/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree_back_stateful/Primitives.fst
+++ b/tests/betree_back_stateful/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x