From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 4cd7a2a869..8dcf5c084e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -44,7 +44,7 @@ module Cst_stack : sig val add_args : constr array -> t -> t val add_cst : constr -> t -> t val best_cst : t -> (constr * constr list) option - val best_replace : constr -> t -> constr -> constr + val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : t -> Constant.t option val pr : t -> Pp.std_ppcmds end -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- pretyping/reductionops.mli | 100 +++++++++++++++++++++++---------------------- 1 file changed, 51 insertions(+), 49 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 8dcf5c084e..911dab0b67 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -38,6 +38,7 @@ val set_refolding_in_reduction : bool -> unit cst applied to params must convertible to term of the state applied to args *) module Cst_stack : sig + open EConstr type t val empty : t val add_param : constr -> t -> t @@ -45,12 +46,13 @@ module Cst_stack : sig val add_cst : constr -> t -> t val best_cst : t -> (constr * constr list) option val best_replace : Evd.evar_map -> constr -> t -> constr -> constr - val reference : t -> Constant.t option + val reference : Evd.evar_map -> t -> Constant.t option val pr : t -> Pp.std_ppcmds end module Stack : sig + open EConstr type 'a app_node val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds @@ -63,7 +65,7 @@ module Stack : sig | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t - | Fix of fixpoint * 'a t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t | Shift of int @@ -82,9 +84,9 @@ module Stack : sig val compare_shape : 'a t -> 'a t -> bool (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)]. @return the result and the lifts to apply on the terms *) - val fold2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a -> - Term.constr t -> Term.constr t -> 'a * int * int - val map : (Term.constr -> Term.constr) -> Term.constr t -> Term.constr t + val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> + constr t -> constr t -> 'a * int * int + val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not @@ -101,25 +103,25 @@ module Stack : sig val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : constr * constr t -> Cst_stack.t -> constr * constr t - val zip : ?refold:bool -> constr * constr t -> constr + val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t + val zip : ?refold:bool -> evar_map -> constr * constr t -> constr end (************************************************************************) -type state = constr * constr Stack.t +type state = EConstr.t * EConstr.t Stack.t -type contextual_reduction_function = env -> evar_map -> constr -> constr +type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr type reduction_function = contextual_reduction_function -type local_reduction_function = evar_map -> constr -> constr +type local_reduction_function = evar_map -> EConstr.t -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = - env -> evar_map -> constr -> constr * constr list + env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list type stack_reduction_function = contextual_stack_reduction_function type local_stack_reduction_function = - evar_map -> constr -> constr * constr list + evar_map -> EConstr.t -> EConstr.t * EConstr.t list type contextual_state_reduction_function = env -> evar_map -> state -> state @@ -137,13 +139,13 @@ val strong_prodspine : local_reduction_function -> local_reduction_function val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function i*) -val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a +val stacklam : (state -> 'a) -> EConstr.t list -> evar_map -> EConstr.t -> EConstr.t Stack.t -> 'a val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr (** {6 Generic Optimized Reduction Function using Closures } *) @@ -196,46 +198,46 @@ val whd_zeta_stack : local_stack_reduction_function val whd_zeta_state : local_state_reduction_function val whd_zeta : local_reduction_function -val shrink_eta : constr -> constr +val shrink_eta : EConstr.t -> constr (** Various reduction functions *) val safe_evar_value : evar_map -> existential -> constr option -val beta_applist : constr * constr list -> constr - -val hnf_prod_app : env -> evar_map -> constr -> constr -> constr -val hnf_prod_appvect : env -> evar_map -> constr -> constr array -> constr -val hnf_prod_applist : env -> evar_map -> constr -> constr list -> constr -val hnf_lam_app : env -> evar_map -> constr -> constr -> constr -val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr -val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr - -val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts -val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr -val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val beta_applist : evar_map -> EConstr.t * EConstr.t list -> constr + +val hnf_prod_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr +val hnf_prod_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr +val hnf_prod_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr +val hnf_lam_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr +val hnf_lam_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr +val hnf_lam_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr + +val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr +val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr +val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * constr) list * sorts +val sort_of_arity : env -> evar_map -> EConstr.t -> sorts +val splay_prod_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr +val splay_lam_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr val splay_prod_assum : - env -> evar_map -> constr -> Context.Rel.t * constr + env -> evar_map -> EConstr.t -> Context.Rel.t * constr type 'a miota_args = { - mP : constr; (** the result type *) - mconstr : constr; (** the constructor *) + mP : EConstr.t; (** the result type *) + mconstr : EConstr.t; (** the constructor *) mci : case_info; (** special info to re-build pattern *) mcargs : 'a list; (** the constructor's arguments *) mlf : 'a array } (** the branch code vector *) -val reducible_mind_case : constr -> bool -val reduce_mind_case : constr miota_args -> constr +val reducible_mind_case : evar_map -> EConstr.t -> bool +val reduce_mind_case : evar_map -> EConstr.t miota_args -> EConstr.t -val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term -val is_arity : env -> evar_map -> constr -> bool -val is_sort : env -> evar_map -> types -> bool +val find_conclusion : env -> evar_map -> EConstr.t -> (EConstr.t,EConstr.t) kind_of_term +val is_arity : env -> evar_map -> EConstr.t -> bool +val is_sort : env -> evar_map -> EConstr.types -> bool -val contract_fix : ?env:Environ.env -> ?reference:Constant.t -> fixpoint -> constr -val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option +val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> (EConstr.t, EConstr.t) pfixpoint -> EConstr.t +val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> constant tableKey -> bool @@ -247,14 +249,14 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool +val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool +val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> EConstr.t -> EConstr.t -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) -val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool +val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @@ -280,11 +282,11 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (** {6 Special-Purpose Reduction Functions } *) -val whd_meta : evar_map -> constr -> constr -val plain_instance : constr Metamap.t -> constr -> constr -val instance : evar_map -> constr Metamap.t -> constr -> constr +val whd_meta : local_reduction_function +val plain_instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> EConstr.t +val instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> constr val head_unfold_under_prod : transparent_state -> reduction_function -val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr +val betazetaevar_applist : evar_map -> int -> EConstr.t -> EConstr.t list -> constr (** {6 Heuristic for Conversion with Evar } *) -- cgit v1.2.3 From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- pretyping/reductionops.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 911dab0b67..5e6a40786c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -264,12 +264,12 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> ECo otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool (** Conversion with inference of universe constraints *) -val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> +val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool) -> unit -val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> +val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool @@ -278,7 +278,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) -- cgit v1.2.3 From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Nov 2016 11:39:27 +0100 Subject: Unification API using EConstr. --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 5e6a40786c..c3b82729d5 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -198,7 +198,7 @@ val whd_zeta_stack : local_stack_reduction_function val whd_zeta_state : local_state_reduction_function val whd_zeta : local_reduction_function -val shrink_eta : EConstr.t -> constr +val shrink_eta : EConstr.constr -> EConstr.constr (** Various reduction functions *) -- cgit v1.2.3 From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 21:55:33 +0100 Subject: Clenv API using EConstr. --- pretyping/reductionops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index c3b82729d5..864b1a625c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -295,6 +295,6 @@ val whd_betaiota_deltazeta_for_iota_state : state * Cst_stack.t (** {6 Meta-related reduction functions } *) -val meta_instance : evar_map -> constr freelisted -> constr +val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr val nf_meta : evar_map -> constr -> constr -val meta_reducible_instance : evar_map -> constr freelisted -> constr +val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr -- cgit v1.2.3 From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:07:35 +0100 Subject: Inv API using EConstr. --- pretyping/reductionops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 864b1a625c..e67fad3fd4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -213,9 +213,9 @@ val hnf_lam_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr val hnf_lam_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr val hnf_lam_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr -val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr -val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * constr) list * sorts +val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr +val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr +val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts val sort_of_arity : env -> evar_map -> EConstr.t -> sorts val splay_prod_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr val splay_lam_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr -- cgit v1.2.3 From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 03:04:13 +0100 Subject: Rewrite API using EConstr. --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e67fad3fd4..1e6527b297 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -296,5 +296,5 @@ val whd_betaiota_deltazeta_for_iota_state : (** {6 Meta-related reduction functions } *) val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr -val nf_meta : evar_map -> constr -> constr +val nf_meta : evar_map -> EConstr.constr -> EConstr.constr val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1e6527b297..3b3242537f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -204,7 +204,7 @@ val shrink_eta : EConstr.constr -> EConstr.constr val safe_evar_value : evar_map -> existential -> constr option -val beta_applist : evar_map -> EConstr.t * EConstr.t list -> constr +val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr val hnf_prod_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr val hnf_prod_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- pretyping/reductionops.mli | 101 ++++++++++++++++++++++----------------------- 1 file changed, 50 insertions(+), 51 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3b3242537f..add1d186bb 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -8,6 +8,7 @@ open Names open Term +open EConstr open Univ open Evd open Environ @@ -38,7 +39,6 @@ val set_refolding_in_reduction : bool -> unit cst applied to params must convertible to term of the state applied to args *) module Cst_stack : sig - open EConstr type t val empty : t val add_param : constr -> t -> t @@ -52,7 +52,6 @@ end module Stack : sig - open EConstr type 'a app_node val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds @@ -109,19 +108,19 @@ end (************************************************************************) -type state = EConstr.t * EConstr.t Stack.t +type state = constr * constr Stack.t -type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr +type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function -type local_reduction_function = evar_map -> EConstr.t -> constr +type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma } +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } type contextual_stack_reduction_function = - env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list + env -> evar_map -> constr -> constr * constr list type stack_reduction_function = contextual_stack_reduction_function type local_stack_reduction_function = - evar_map -> EConstr.t -> EConstr.t * EConstr.t list + evar_map -> constr -> constr * constr list type contextual_state_reduction_function = env -> evar_map -> state -> state @@ -139,13 +138,13 @@ val strong_prodspine : local_reduction_function -> local_reduction_function val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function i*) -val stacklam : (state -> 'a) -> EConstr.t list -> evar_map -> EConstr.t -> EConstr.t Stack.t -> 'a +val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr + Environ.env -> Evd.evar_map -> constr -> constr (** {6 Generic Optimized Reduction Function using Closures } *) @@ -156,11 +155,11 @@ val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betaiotazeta : local_reduction_function val nf_all : reduction_function -val nf_evar : evar_map -> constr -> constr +val nf_evar : evar_map -> Constr.constr -> Constr.constr (** Lazy strategy, weak head reduction *) -val whd_evar : evar_map -> constr -> constr +val whd_evar : evar_map -> Constr.constr -> Constr.constr val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function @@ -198,45 +197,45 @@ val whd_zeta_stack : local_stack_reduction_function val whd_zeta_state : local_state_reduction_function val whd_zeta : local_reduction_function -val shrink_eta : EConstr.constr -> EConstr.constr +val shrink_eta : constr -> constr (** Various reduction functions *) -val safe_evar_value : evar_map -> existential -> constr option +val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option -val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr +val beta_applist : evar_map -> constr * constr list -> constr -val hnf_prod_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr -val hnf_prod_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr -val hnf_prod_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr -val hnf_lam_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr -val hnf_lam_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr -val hnf_lam_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr +val hnf_prod_app : env -> evar_map -> constr -> constr -> constr +val hnf_prod_appvect : env -> evar_map -> constr -> constr array -> constr +val hnf_prod_applist : env -> evar_map -> constr -> constr list -> constr +val hnf_lam_app : env -> evar_map -> constr -> constr -> constr +val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr +val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr -val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr -val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts -val sort_of_arity : env -> evar_map -> EConstr.t -> sorts -val splay_prod_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr -val splay_lam_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr +val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts +val sort_of_arity : env -> evar_map -> constr -> sorts +val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_prod_assum : - env -> evar_map -> EConstr.t -> Context.Rel.t * constr + env -> evar_map -> constr -> Context.Rel.t * constr type 'a miota_args = { - mP : EConstr.t; (** the result type *) - mconstr : EConstr.t; (** the constructor *) + mP : constr; (** the result type *) + mconstr : constr; (** the constructor *) mci : case_info; (** special info to re-build pattern *) mcargs : 'a list; (** the constructor's arguments *) mlf : 'a array } (** the branch code vector *) -val reducible_mind_case : evar_map -> EConstr.t -> bool -val reduce_mind_case : evar_map -> EConstr.t miota_args -> EConstr.t +val reducible_mind_case : evar_map -> constr -> bool +val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> EConstr.t -> (EConstr.t,EConstr.t) kind_of_term -val is_arity : env -> evar_map -> EConstr.t -> bool -val is_sort : env -> evar_map -> EConstr.types -> bool +val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term +val is_arity : env -> evar_map -> constr -> bool +val is_sort : env -> evar_map -> types -> bool -val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> (EConstr.t, EConstr.t) pfixpoint -> EConstr.t +val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) @@ -249,14 +248,14 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool -val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool -val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> EConstr.t -> EConstr.t -> bool +val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) -val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool +val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @@ -264,29 +263,29 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> ECo otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map * bool (** Conversion with inference of universe constraints *) -val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> +val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> evar_map * bool) -> unit -val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> +val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> evar_map * bool (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> - (constr, evar_map) Reduction.generic_conversion_function) -> + (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) val whd_meta : local_reduction_function -val plain_instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> EConstr.t -val instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> constr +val plain_instance : evar_map -> constr Metamap.t -> constr -> constr +val instance : evar_map -> constr Metamap.t -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function -val betazetaevar_applist : evar_map -> int -> EConstr.t -> EConstr.t list -> constr +val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr (** {6 Heuristic for Conversion with Evar } *) @@ -295,6 +294,6 @@ val whd_betaiota_deltazeta_for_iota_state : state * Cst_stack.t (** {6 Meta-related reduction functions } *) -val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr -val nf_meta : evar_map -> EConstr.constr -> EConstr.constr -val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr +val meta_instance : evar_map -> constr freelisted -> constr +val nf_meta : evar_map -> constr -> constr +val meta_reducible_instance : evar_map -> constr freelisted -> constr -- cgit v1.2.3 From fa638c3e71752b6a59261776b36f1bed7d9c26d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 12:07:55 +0100 Subject: Cc API using EConstr. --- pretyping/reductionops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index add1d186bb..8aaeeb2c21 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -149,6 +149,7 @@ val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function +val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- pretyping/reductionops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 8aaeeb2c21..dcc11cfcf3 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -156,11 +156,11 @@ val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function val nf_betaiotazeta : local_reduction_function val nf_all : reduction_function -val nf_evar : evar_map -> Constr.constr -> Constr.constr +val nf_evar : evar_map -> constr -> constr (** Lazy strategy, weak head reduction *) -val whd_evar : evar_map -> Constr.constr -> Constr.constr +val whd_evar : evar_map -> constr -> constr val whd_nored : local_reduction_function val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- pretyping/reductionops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index dcc11cfcf3..15ddeb15c0 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,10 +217,10 @@ val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr -val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : - env -> evar_map -> constr -> Context.Rel.t * constr + env -> evar_map -> constr -> rel_context * constr type 'a miota_args = { mP : constr; (** the result type *) -- cgit v1.2.3 From ce029533a1f0fc6ac9e28d162350a64446522246 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:05:17 +0200 Subject: Make the Constr.kind_of_term type parametric in sorts and universes. --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 15ddeb15c0..18416b1424 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -232,7 +232,7 @@ type 'a miota_args = { val reducible_mind_case : evar_map -> constr -> bool val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, Sorts.t, Univ.Instance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool -- cgit v1.2.3 From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- pretyping/reductionops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 18416b1424..01707b47a7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -215,8 +215,8 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts -val sort_of_arity : env -> evar_map -> constr -> sorts +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * ESorts.t +val sort_of_arity : env -> evar_map -> constr -> ESorts.t val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : @@ -232,7 +232,7 @@ type 'a miota_args = { val reducible_mind_case : evar_map -> constr -> bool val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr, constr, Sorts.t, Univ.Instance.t) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- pretyping/reductionops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/reductionops.mli') diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 01707b47a7..752c30a8ac 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -232,7 +232,7 @@ type 'a miota_args = { val reducible_mind_case : evar_map -> constr -> bool val reduce_mind_case : evar_map -> constr miota_args -> constr -val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term +val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool -- cgit v1.2.3