diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 83 |
1 files changed, 51 insertions, 32 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..59bc4a8b72 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -57,9 +57,12 @@ module Stack : sig val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -69,10 +72,9 @@ module Stack : sig val empty : 'a t val is_empty : 'a t -> bool - val append_app : 'a array -> 'a t -> 'a t - val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + [@@ocaml.deprecated "Use decomp_rev"] val compare_shape : 'a t -> 'a t -> bool @@ -84,30 +86,56 @@ module Stack : sig val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t + + (** [append_app args sk] pushes array of arguments [args] on [sk] *) + val append_app : 'a array -> 'a t -> 'a t + + (** [append_app_list args sk] pushes list of arguments [args] on [sk] *) val append_app_list : 'a list -> 'a t -> 'a t - (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App *) + (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with + [sk1] purely applicative and [sk2] does not start with an argument *) val strip_app : 'a t -> 'a t * 'a t - (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) + (** @return (the nth first elements, the (n+1)th element, the remaining stack) + if there enough of those *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + (** [decomp sk] extracts the first argument of [sk] is there is some *) + val decomp : 'a t -> ('a * 'a t) option + + (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *) + val decomp_rev : 'a t -> ('a * 'a t) option + + (** [not_purely_applicative sk] *) val not_purely_applicative : 'a t -> bool + + (** [list_of_app_stack sk] either returns [Some sk] turned into a list of + arguments if [sk] is purely applicative and [None] otherwise *) val list_of_app_stack : constr t -> constr list option + (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0 + @raise an anomaly if there is less that [n] arguments available *) val assign : 'a t -> int -> 'a -> 'a t + + (** [args_size sk] returns the number of arguments available at the + head of [sk] *) val args_size : 'a t -> int + + (** [tail n sk] drops the [n] first arguments of [sk] + @raise [Invalid_argument] if there are not enough arguments *) val tail : int -> 'a t -> 'a t + + (** [nth sk n] returns the [n]-th argument of [sk], counting from 0 + @raise [Not_found] if there is no [n]th argument *) val nth : 'a t -> int -> 'a + (** [zip sigma t sk] *) val zip : evar_map -> constr * constr t -> constr end (************************************************************************) -type state = constr * constr Stack.t - type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -115,11 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type state_reduction_function = - env -> evar_map -> state -> state - -val pr_state : env -> evar_map -> state -> Pp.t - (** {6 Reduction Function Operators } *) val strong_with_flags : @@ -127,12 +150,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val whd_state_gen : - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state - -val iterate_whd_gen : CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> constr -> constr - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -166,24 +183,13 @@ val whd_all_stack : stack_reduction_function val whd_allnolet_stack : stack_reduction_function val whd_betalet_stack : stack_reduction_function -val whd_nored_state : state_reduction_function -val whd_beta_state : state_reduction_function -val whd_betaiota_state : state_reduction_function -val whd_betaiotazeta_state : state_reduction_function -val whd_all_state : state_reduction_function -val whd_allnolet_state : state_reduction_function -val whd_betalet_state : state_reduction_function - (** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function -val whd_delta_state : state_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function -val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function val whd_zeta_stack : stack_reduction_function -val whd_zeta_state : state_reduction_function val whd_zeta : reduction_function val shrink_eta : Environ.env -> constr -> constr @@ -269,11 +275,24 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (** {6 Heuristic for Conversion with Evar } *) +type state = constr * constr Stack.t + +type state_reduction_function = + env -> evar_map -> state -> state + +val pr_state : env -> evar_map -> state -> Pp.t + +val whd_nored_state : state_reduction_function + val whd_betaiota_deltazeta_for_iota_state : - TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state + TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) -val meta_instance : env -> evar_map -> constr freelisted -> constr +type meta_instance_subst + +val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst + +val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr exception AnomalyInConversion of exn |