Missing API in EConstr.

1 files changed, 36 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 2de6d7ae4..b6b202cd9 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -19,12 +19,17 @@ sig
 type t
 val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
 val of_kind : (t, t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
 val unsafe_eq : (t, Constr.t) eq
+val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
+val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
+val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
 end =
 struct
 
@@ -63,6 +68,7 @@ let rec whd_evar sigma c =
 
 let kind sigma c = Constr.kind (whd_evar sigma c)
 let kind_upto = kind
+let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
 let of_kind = Constr.of_kind
 let of_constr c = c
 let unsafe_to_constr c = c
@@ -71,6 +77,11 @@ let unsafe_eq = Refl
 let rec to_constr sigma t =
   Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t)
 
+let of_named_decl d = d
+let unsafe_to_named_decl d = d
+let of_rel_decl d = d
+let unsafe_to_rel_decl d = d
+
 end
 
 include API
@@ -261,6 +272,25 @@ let decompose_lam_n_decls sigma n =
   in
   lamdec_rec Context.Rel.empty n
 
+let lamn n env b =
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
+    | _ -> assert false
+  in
+  lamrec (n,env,b)
+
+let compose_lam l b = lamn (List.length l) l b
+
+let rec to_lambda sigma n prod =
+  if Int.equal n 0 then
+    prod
+  else
+    match kind sigma prod with
+      | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda sigma (n-1) bd)
+      | Cast (c,_,_) -> to_lambda sigma n c
+      | _   -> user_err ~hdr:"to_lambda" (Pp.mt ())
+
 let decompose_prod sigma c =
   let rec proddec_rec l c = match kind sigma c with
     | Prod (x,t,c) -> proddec_rec ((x,t)::l) c
@@ -682,9 +712,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 fresh_global ?loc ?rigid ?names env sigma reference =
+  let Sigma.Sigma (t,sigma,p) =
+    Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
+  Sigma.Sigma (of_constr t,sigma,p)
 
 module Unsafe =
 struct
 let to_constr = unsafe_to_constr
+let to_rel_decl = unsafe_to_rel_decl
+let to_named_decl = unsafe_to_named_decl
 let eq = unsafe_eq
 end