summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Pure.ml8
-rw-r--r--compiler/PureMicroPasses.ml5
-rw-r--r--compiler/SymbolicToPure.ml5
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,