Reductionops API using EConstr.

1 files changed, 51 insertions, 49 deletions

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8dcf5c084..911dab0b6 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 } *)