diff options
| -rw-r--r-- | engine/eConstr.ml | 36 | ||||
| -rw-r--r-- | engine/eConstr.mli | 21 |
2 files changed, 57 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 diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 7992c0633..3b479a64d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -39,6 +39,8 @@ val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_ val to_constr : Evd.evar_map -> t -> Constr.t (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type + (** {5 Constructors} *) val of_kind : (t, t) Constr.kind_of_term -> t @@ -143,6 +145,9 @@ val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t +val compose_lam : (Name.t * t) list -> t -> t +val to_lambda : Evd.evar_map -> int -> t -> t + val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t @@ -212,6 +217,16 @@ val lookup_rel : int -> env -> rel_declaration val lookup_named : variable -> env -> named_declaration val lookup_named_val : variable -> named_context_val -> named_declaration +(* XXX Missing Sigma proxy *) +val fresh_global : + ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> + 'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma + +(** {5 Extra} *) + +val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt +val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt + (** {5 Unsafe operations} *) module Unsafe : @@ -219,6 +234,12 @@ sig val to_constr : t -> Constr.t (** Physical identity. Does not care for defined evars. *) + val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt + (** Physical identity. Does not care for defined evars. *) + + val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt + (** Physical identity. Does not care for defined evars. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end |