Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sig

3 files changed, 13 insertions, 5 deletions

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 0ae83007..d7aea0f7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -860,8 +860,8 @@ type fun_effect_info = {
           the set [{ forward function } U { backward functions }].
 
           We need this because of the option {!val:Config.backward_no_state_update}:
-          if it is [true], then in case of a backward function {!stateful} is [false],
-          but we might need to know whether the corresponding forward function
+          if it is [true], then in case of a backward function {!stateful} might be
+          [false], but we might need to know whether the corresponding forward function
           is stateful or not.
        *)
   stateful : bool;  (** [true] if the function is stateful (updates a state) *)
@@ -876,7 +876,9 @@ type fun_effect_info = {
 (** Meta information about a function signature *)
 type fun_sig_info = {
   has_fuel : bool;
-  (* TODO: add [num_fwd_inputs_no_fuel_no_state] *)
+  num_fwd_inputs_no_fuel_no_state : int;
+      (** The number of input types for forward computation, ignoring the fuel (if used)
+          and ignoring the state (if used) *)
   num_fwd_inputs_with_fuel_no_state : int;
       (** The number of input types for forward computation, with the fuel (if used)
           and ignoring the state (if used) *)
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 959ec1c8..34578750 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1340,6 +1340,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_sig_info =
               let fuel = if !Config.use_fuel then 1 else 0 in
               let num_inputs = List.length loop.inputs in
+              let num_fwd_inputs_no_fuel_no_state = num_inputs in
               let num_fwd_inputs_with_fuel_no_state = fuel + num_inputs in
               let fwd_state =
                 fun_sig_info.num_fwd_inputs_with_fuel_with_state
@@ -1350,6 +1351,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
               in
               {
                 has_fuel = !Config.use_fuel;
+                num_fwd_inputs_no_fuel_no_state;
                 num_fwd_inputs_with_fuel_no_state;
                 num_fwd_inputs_with_fuel_with_state;
                 num_back_inputs_no_state = fun_sig_info.num_back_inputs_no_state;
@@ -2168,6 +2170,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
           in
           let {
             has_fuel;
+            num_fwd_inputs_no_fuel_no_state;
             num_fwd_inputs_with_fuel_no_state;
             num_fwd_inputs_with_fuel_with_state;
             num_back_inputs_no_state;
@@ -2182,6 +2185,8 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
           let info =
             {
               has_fuel;
+              num_fwd_inputs_no_fuel_no_state =
+                num_fwd_inputs_no_fuel_no_state - num_filtered;
               num_fwd_inputs_with_fuel_no_state =
                 num_fwd_inputs_with_fuel_no_state - num_filtered;
               num_fwd_inputs_with_fuel_with_state =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index bf4d26f2..2ef313e6 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1035,10 +1035,10 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   let generics = translate_generic_params sg.generics in
   (* Return *)
   let has_fuel = fuel <> [] in
-  let num_fwd_inputs_no_state = List.length fwd_inputs in
+  let num_fwd_inputs_no_fuel_no_state = List.length fwd_inputs in
   let num_fwd_inputs_with_fuel_no_state =
     (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *)
-    List.length fuel + num_fwd_inputs_no_state
+    List.length fuel + num_fwd_inputs_no_fuel_no_state
   in
   let num_back_inputs_no_state =
     if bid = None then None else Some (List.length back_inputs)
@@ -1046,6 +1046,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
   let info =
     {
       has_fuel;
+      num_fwd_inputs_no_fuel_no_state;
       num_fwd_inputs_with_fuel_no_state;
       num_fwd_inputs_with_fuel_with_state =
         (* We use the fact that [fwd_state_ty] has length 1 if there is a state,