Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.

2 files changed, 30 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 53123c933..a65b3941e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -770,6 +770,20 @@ let rec isArity sigma c =
   | Sort _          -> true
   | _               -> false
 
+type arity = rel_context * ESorts.t
+
+let destArity sigma =
+  let open Context.Rel.Declaration in
+  let rec prodec_rec l c =
+    match kind sigma c with
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
+    | Cast (c,_,_)      -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
+  in
+  prodec_rec []
+
 let mkProd_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
@@ -817,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
 
+let map_rel_context_in_env f env sign =
+  let rec aux env acc = function
+    | d::sign ->
+        aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign
+    | [] ->
+        acc
+  in
+  aux env [] (List.rev sign)
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, of_constr t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6f2a30f4a..30de748a1 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -146,7 +146,11 @@ val isFix : Evd.evar_map -> t -> bool
 val isCoFix : Evd.evar_map -> t -> bool
 val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
+
+type arity = rel_context * ESorts.t
+val destArity : Evd.evar_map -> types -> arity
 val isArity : Evd.evar_map -> t -> bool
+
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
 val isRelN : Evd.evar_map -> int -> t -> bool
 
@@ -262,6 +266,9 @@ val lookup_rel : int -> env -> rel_declaration
 val lookup_named : variable -> env -> named_declaration
 val lookup_named_val : variable -> named_context_val -> named_declaration
 
+val map_rel_context_in_env :
+  (env -> constr -> constr) -> env -> rel_context -> rel_context
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->