diff options
Diffstat (limited to 'compiler/Pure.ml')
| -rw-r--r-- | compiler/Pure.ml | 54 |
1 files changed, 37 insertions, 17 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 8d39cc69..c3716001 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -561,7 +561,7 @@ type fun_id_or_trait_method_ref = (** A function id for a non-assumed function *) type regular_fun_id = - fun_id_or_trait_method_ref * LoopId.id option * T.RegionGroupId.id option + fun_id_or_trait_method_ref * LoopId.id option * RegionGroupId.id option [@@deriving show, ord] (** A function identifier *) @@ -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) *) @@ -873,21 +873,41 @@ type fun_effect_info = { } [@@deriving show] -(** Meta information about a function signature *) -type fun_sig_info = { +type inputs_info = { has_fuel : bool; - (* TODO: add [num_fwd_inputs_no_fuel_no_state] *) - num_fwd_inputs_with_fuel_no_state : int; - (** The number of input types for forward computation, with the fuel (if used) + num_inputs_no_fuel_no_state : int; + (** The number of input types ignoring the fuel (if used) and ignoring the state (if used) *) - num_fwd_inputs_with_fuel_with_state : int; - (** The number of input types for forward computation, with fuel and state (if used) *) - num_back_inputs_no_state : int option; - (** The number of additional inputs for the backward computation (if pertinent), - 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) *) + num_inputs_with_fuel_no_state : int; + (** The number of input types, with the fuel (if used) + and ignoring the state (if used) *) + num_inputs_with_fuel_with_state : int; + (** The number of input types, with fuel and state (if used) *) +} +[@@deriving show] + +type 'a back_info = + | SingleBack of 'a option + (** Information about a single backward function, if pertinent. + + We use this variant if we split the forward and the backward functions. + *) + | AllBacks of 'a RegionGroupId.Map.t + (** Information about the various backward functions. + + We use this if we *do not* split the forward and the backward functions. + All the information is then carried by the forward function. + *) +[@@deriving show] + +type back_inputs_info = inputs_info back_info [@@deriving show] + +(** Meta information about a function signature *) +type fun_sig_info = { + fwd_info : inputs_info; + (** Information about the inputs of the forward function *) + back_info : back_inputs_info; + (** Information about the inputs of the backward functions. *) effect_info : fun_effect_info; } [@@deriving show] @@ -1020,7 +1040,7 @@ type fun_decl = { *) loop_id : LoopId.id option; (** [Some] if this definition was generated for a loop *) - back_id : T.RegionGroupId.id option; + back_id : RegionGroupId.id option; llbc_name : llbc_name; (** The original LLBC name. *) name : string; (** We use the name only for printing purposes (for debugging): |