diff options
| -rw-r--r-- | compiler/Pure.ml | 8 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 5 |
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, |