aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml782
-rw-r--r--engine/eConstr.mli282
-rw-r--r--engine/engine.mllib3
-rw-r--r--engine/evarutil.ml204
-rw-r--r--engine/evarutil.mli38
-rw-r--r--engine/evd.ml352
-rw-r--r--engine/evd.mli35
-rw-r--r--engine/namegen.ml118
-rw-r--r--engine/namegen.mli44
-rw-r--r--engine/proofview.ml28
-rw-r--r--engine/proofview.mli13
-rw-r--r--engine/sigma.ml4
-rw-r--r--engine/sigma.mli2
-rw-r--r--engine/termops.ml763
-rw-r--r--engine/termops.mli220
-rw-r--r--engine/universes.ml9
-rw-r--r--engine/universes.mli6
17 files changed, 2016 insertions, 887 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
new file mode 100644
index 000000000..bb9075e74
--- /dev/null
+++ b/engine/eConstr.ml
@@ -0,0 +1,782 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CSig
+open CErrors
+open Util
+open Names
+open Term
+open Context
+open Evd
+
+module API :
+sig
+module ESorts :
+sig
+type t
+val make : Sorts.t -> t
+val kind : Evd.evar_map -> t -> Sorts.t
+val unsafe_to_sorts : t -> Sorts.t
+end
+module EInstance :
+sig
+type t
+val make : Univ.Instance.t -> t
+val kind : Evd.evar_map -> t -> Univ.Instance.t
+val empty : t
+val is_empty : t -> bool
+val unsafe_to_instance : t -> Univ.Instance.t
+end
+type t
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) 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, ESorts.t, EInstance.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
+
+module ESorts =
+struct
+ type t = Sorts.t
+ let make s = s
+ let kind sigma = function
+ | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+ | s -> s
+ let unsafe_to_sorts s = s
+end
+
+module EInstance =
+struct
+ type t = Univ.Instance.t
+ let make i = i
+ let kind sigma i =
+ if Univ.Instance.is_empty i then i
+ else Evd.normalize_universe_instance sigma i
+ let empty = Univ.Instance.empty
+ let is_empty = Univ.Instance.is_empty
+ let unsafe_to_instance t = t
+end
+
+type t = Constr.t
+
+let safe_evar_value sigma ev =
+ try Some (Evd.existential_value sigma ev)
+ with NotInstantiatedEvar | Not_found -> None
+
+let rec whd_evar sigma c =
+ match Constr.kind c with
+ | Evar ev ->
+ begin match safe_evar_value sigma ev with
+ | Some c -> whd_evar sigma c
+ | None -> c
+ end
+ | App (f, args) when isEvar f ->
+ (** Enforce smart constructor invariant on applications *)
+ let ev = destEvar f in
+ begin match safe_evar_value sigma ev with
+ | None -> c
+ | Some f -> whd_evar sigma (mkApp (f, args))
+ end
+ | Cast (c0, k, t) when isEvar c0 ->
+ (** Enforce smart constructor invariant on casts. *)
+ let ev = destEvar c0 in
+ begin match safe_evar_value sigma ev with
+ | None -> c
+ | Some c -> whd_evar sigma (mkCast (c, k, t))
+ end
+ | _ -> 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
+let unsafe_eq = Refl
+
+let rec to_constr sigma c = match Constr.kind c with
+| Evar ev ->
+ begin match safe_evar_value sigma ev with
+ | Some c -> to_constr sigma c
+ | None -> Constr.map (fun c -> to_constr sigma c) c
+ end
+| Sort (Type u) ->
+ let u' = Evd.normalize_universe sigma u in
+ if u' == u then c else mkSort (Sorts.sort_of_univ u')
+| Const (c', u) when not (Univ.Instance.is_empty u) ->
+ let u' = Evd.normalize_universe_instance sigma u in
+ if u' == u then c else mkConstU (c', u')
+| Ind (i, u) when not (Univ.Instance.is_empty u) ->
+ let u' = Evd.normalize_universe_instance sigma u in
+ if u' == u then c else mkIndU (i, u')
+| Construct (co, u) when not (Univ.Instance.is_empty u) ->
+ let u' = Evd.normalize_universe_instance sigma u in
+ if u' == u then c else mkConstructU (co, u')
+| _ -> Constr.map (fun c -> to_constr sigma c) c
+
+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
+
+type types = t
+type constr = t
+type existential = t pexistential
+type fixpoint = (t, t) pfixpoint
+type cofixpoint = (t, t) pcofixpoint
+type unsafe_judgment = (constr, types) Environ.punsafe_judgment
+type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_context = (constr, types) Context.Named.pt
+type rel_context = (constr, types) Context.Rel.pt
+
+let in_punivs a = (a, EInstance.empty)
+
+let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
+let mkSet = of_kind (Sort (ESorts.make Sorts.set))
+let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u)))
+let mkRel n = of_kind (Rel n)
+let mkVar id = of_kind (Var id)
+let mkMeta n = of_kind (Meta n)
+let mkEvar e = of_kind (Evar e)
+let mkSort s = of_kind (Sort (ESorts.make s))
+let mkCast (b, k, t) = of_kind (Cast (b, k, t))
+let mkProd (na, t, u) = of_kind (Prod (na, t, u))
+let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
+let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
+let mkApp (f, arg) = of_kind (App (f, arg))
+let mkConstU pc = of_kind (Const pc)
+let mkConst c = of_kind (Const (in_punivs c))
+let mkIndU pi = of_kind (Ind pi)
+let mkInd i = of_kind (Ind (in_punivs i))
+let mkConstructU pc = of_kind (Construct pc)
+let mkConstruct c = of_kind (Construct (in_punivs c))
+let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
+let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
+let mkFix f = of_kind (Fix f)
+let mkCoFix f = of_kind (CoFix f)
+let mkProj (p, c) = of_kind (Proj (p, c))
+let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+
+let applist (f, arg) = mkApp (f, Array.of_list arg)
+
+let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
+let isVar sigma c = match kind sigma c with Var _ -> true | _ -> false
+let isInd sigma c = match kind sigma c with Ind _ -> true | _ -> false
+let isEvar sigma c = match kind sigma c with Evar _ -> true | _ -> false
+let isMeta sigma c = match kind sigma c with Meta _ -> true | _ -> false
+let isSort sigma c = match kind sigma c with Sort _ -> true | _ -> false
+let isCast sigma c = match kind sigma c with Cast _ -> true | _ -> false
+let isApp sigma c = match kind sigma c with App _ -> true | _ -> false
+let isLambda sigma c = match kind sigma c with Lambda _ -> true | _ -> false
+let isLetIn sigma c = match kind sigma c with LetIn _ -> true | _ -> false
+let isProd sigma c = match kind sigma c with Prod _ -> true | _ -> false
+let isConst sigma c = match kind sigma c with Const _ -> true | _ -> false
+let isConstruct sigma c = match kind sigma c with Construct _ -> true | _ -> false
+let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
+let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
+let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
+let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+let isVarId sigma id c =
+ match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+let isRelN sigma n c =
+ match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
+
+let destRel sigma c = match kind sigma c with
+| Rel p -> p
+| _ -> raise DestKO
+
+let destVar sigma c = match kind sigma c with
+| Var p -> p
+| _ -> raise DestKO
+
+let destInd sigma c = match kind sigma c with
+| Ind p -> p
+| _ -> raise DestKO
+
+let destEvar sigma c = match kind sigma c with
+| Evar p -> p
+| _ -> raise DestKO
+
+let destMeta sigma c = match kind sigma c with
+| Meta p -> p
+| _ -> raise DestKO
+
+let destSort sigma c = match kind sigma c with
+| Sort p -> p
+| _ -> raise DestKO
+
+let destCast sigma c = match kind sigma c with
+| Cast (c, k, t) -> (c, k, t)
+| _ -> raise DestKO
+
+let destApp sigma c = match kind sigma c with
+| App (f, a) -> (f, a)
+| _ -> raise DestKO
+
+let destLambda sigma c = match kind sigma c with
+| Lambda (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destLetIn sigma c = match kind sigma c with
+| LetIn (na, b, t, c) -> (na, b, t, c)
+| _ -> raise DestKO
+
+let destProd sigma c = match kind sigma c with
+| Prod (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destConst sigma c = match kind sigma c with
+| Const p -> p
+| _ -> raise DestKO
+
+let destConstruct sigma c = match kind sigma c with
+| Construct p -> p
+| _ -> raise DestKO
+
+let destFix sigma c = match kind sigma c with
+| Fix p -> p
+| _ -> raise DestKO
+
+let destCoFix sigma c = match kind sigma c with
+| CoFix p -> p
+| _ -> raise DestKO
+
+let destCase sigma c = match kind sigma c with
+| Case (ci, t, c, p) -> (ci, t, c, p)
+| _ -> raise DestKO
+
+let destProj sigma c = match kind sigma c with
+| Proj (p, c) -> (p, c)
+| _ -> raise DestKO
+
+let decompose_app sigma c =
+ match kind sigma c with
+ | App (f,cl) -> (f, Array.to_list cl)
+ | _ -> (c,[])
+
+let decompose_lam sigma c =
+ let rec lamdec_rec l c = match kind sigma c with
+ | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+ | Cast (c,_,_) -> lamdec_rec l c
+ | _ -> l,c
+ in
+ lamdec_rec [] c
+
+let decompose_lam_assum sigma c =
+ let open Rel.Declaration in
+ let rec lamdec_rec l c =
+ match kind sigma c with
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
+ | Cast (c,_,_) -> lamdec_rec l c
+ | _ -> l,c
+ in
+ lamdec_rec Context.Rel.empty c
+
+let decompose_lam_n_assum sigma n c =
+ let open Rel.Declaration in
+ if n < 0 then
+ error "decompose_lam_n_assum: integer parameter must be positive";
+ let rec lamdec_rec l n c =
+ if Int.equal n 0 then l,c
+ else
+ match kind sigma c with
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
+ | Cast (c,_,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n_assum: not enough abstractions"
+ in
+ lamdec_rec Context.Rel.empty n c
+
+let decompose_lam_n_decls sigma n =
+ let open Rel.Declaration in
+ if n < 0 then
+ error "decompose_lam_n_decls: integer parameter must be positive";
+ let rec lamdec_rec l n c =
+ if Int.equal n 0 then l,c
+ else
+ match kind sigma c with
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
+ | Cast (c,_,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n_decls: not enough abstractions"
+ 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
+ | Cast (c,_,_) -> proddec_rec l c
+ | _ -> l,c
+ in
+ proddec_rec [] c
+
+let decompose_prod_assum sigma c =
+ let open Rel.Declaration in
+ let rec proddec_rec l c =
+ match kind sigma c with
+ | Prod (x,t,c) -> proddec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+ | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
+ | Cast (c,_,_) -> proddec_rec l c
+ | _ -> l,c
+ in
+ proddec_rec Context.Rel.empty c
+
+let decompose_prod_n_assum sigma n c =
+ let open Rel.Declaration in
+ if n < 0 then
+ error "decompose_prod_n_assum: integer parameter must be positive";
+ let rec prodec_rec l n c =
+ if Int.equal n 0 then l,c
+ else
+ match kind sigma c with
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
+ | Cast (c,_,_) -> prodec_rec l n c
+ | c -> error "decompose_prod_n_assum: not enough assumptions"
+ in
+ prodec_rec Context.Rel.empty n c
+
+let existential_type sigma (evk, args) =
+ of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+
+let map sigma f c = match kind sigma c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (b,k,t) ->
+ let b' = f b in
+ let t' = f t in
+ if b'==b && t' == t then c
+ else mkCast (b', k, t')
+ | Prod (na,t,b) ->
+ let b' = f b in
+ let t' = f t in
+ if b'==b && t' == t then c
+ else mkProd (na, t', b')
+ | Lambda (na,t,b) ->
+ let b' = f b in
+ let t' = f t in
+ if b'==b && t' == t then c
+ else mkLambda (na, t', b')
+ | LetIn (na,b,t,k) ->
+ let b' = f b in
+ let t' = f t in
+ let k' = f k in
+ if b'==b && t' == t && k'==k then c
+ else mkLetIn (na, b', t', k')
+ | App (b,l) ->
+ let b' = f b in
+ let l' = Array.smartmap f l in
+ if b'==b && l'==l then c
+ else mkApp (b', l')
+ | Proj (p,t) ->
+ let t' = f t in
+ if t' == t then c
+ else mkProj (p, t')
+ | Evar (e,l) ->
+ let l' = Array.smartmap f l in
+ if l'==l then c
+ else mkEvar (e, l')
+ | Case (ci,p,b,bl) ->
+ let b' = f b in
+ let p' = f p in
+ let bl' = Array.smartmap f bl in
+ if b'==b && p'==p && bl'==bl then c
+ else mkCase (ci, p', b', bl')
+ | Fix (ln,(lna,tl,bl)) ->
+ let tl' = Array.smartmap f tl in
+ let bl' = Array.smartmap f bl in
+ if tl'==tl && bl'==bl then c
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let tl' = Array.smartmap f tl in
+ let bl' = Array.smartmap f bl in
+ if tl'==tl && bl'==bl then c
+ else mkCoFix (ln,(lna,tl',bl'))
+
+let map_with_binders sigma g f l c0 = match kind sigma c0 with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c0
+ | Cast (c, k, t) ->
+ let c' = f l c in
+ let t' = f l t in
+ if c' == c && t' == t then c0
+ else mkCast (c', k, t')
+ | Prod (na, t, c) ->
+ let t' = f l t in
+ let c' = f (g l) c in
+ if t' == t && c' == c then c0
+ else mkProd (na, t', c')
+ | Lambda (na, t, c) ->
+ let t' = f l t in
+ let c' = f (g l) c in
+ if t' == t && c' == c then c0
+ else mkLambda (na, t', c')
+ | LetIn (na, b, t, c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = f (g l) c in
+ if b' == b && t' == t && c' == c then c0
+ else mkLetIn (na, b', t', c')
+ | App (c, al) ->
+ let c' = f l c in
+ let al' = CArray.Fun1.smartmap f l al in
+ if c' == c && al' == al then c0
+ else mkApp (c', al')
+ | Proj (p, t) ->
+ let t' = f l t in
+ if t' == t then c0
+ else mkProj (p, t')
+ | Evar (e, al) ->
+ let al' = CArray.Fun1.smartmap f l al in
+ if al' == al then c0
+ else mkEvar (e, al')
+ | Case (ci, p, c, bl) ->
+ let p' = f l p in
+ let c' = f l c in
+ let bl' = CArray.Fun1.smartmap f l bl in
+ if p' == p && c' == c && bl' == bl then c0
+ else mkCase (ci, p', c', bl')
+ | Fix (ln, (lna, tl, bl)) ->
+ let tl' = CArray.Fun1.smartmap f l tl in
+ let l' = iterate g (Array.length tl) l in
+ let bl' = CArray.Fun1.smartmap f l' bl in
+ if tl' == tl && bl' == bl then c0
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let tl' = CArray.Fun1.smartmap f l tl in
+ let l' = iterate g (Array.length tl) l in
+ let bl' = CArray.Fun1.smartmap f l' bl in
+ mkCoFix (ln,(lna,tl',bl'))
+
+let iter sigma f c = match kind sigma c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> ()
+ | Cast (c,_,t) -> f c; f t
+ | Prod (_,t,c) -> f t; f c
+ | Lambda (_,t,c) -> f t; f c
+ | LetIn (_,b,t,c) -> f b; f t; f c
+ | App (c,l) -> f c; Array.iter f l
+ | Proj (p,c) -> f c
+ | Evar (_,l) -> Array.iter f l
+ | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+ | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+ | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+
+let iter_with_full_binders sigma g f n c =
+ let open Context.Rel.Declaration in
+ match kind sigma c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> ()
+ | Cast (c,_,t) -> f n c; f n t
+ | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+ | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+ | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
+ | App (c,l) -> f n c; CArray.Fun1.iter f n l
+ | Evar (_,l) -> CArray.Fun1.iter f n l
+ | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+ | Proj (p,c) -> f n c
+ | Fix (_,(lna,tl,bl)) ->
+ Array.iter (f n) tl;
+ let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+ Array.iter (f n') bl
+ | CoFix (_,(lna,tl,bl)) ->
+ Array.iter (f n) tl;
+ let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+ Array.iter (f n') bl
+
+let iter_with_binders sigma g f n c =
+ iter_with_full_binders sigma (fun _ acc -> g acc) f n c
+
+let fold sigma f acc c = match kind sigma c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> acc
+ | Cast (c,_,t) -> f (f acc c) t
+ | Prod (_,t,c) -> f (f acc t) c
+ | Lambda (_,t,c) -> f (f acc t) c
+ | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+ | App (c,l) -> Array.fold_left f (f acc c) l
+ | Proj (p,c) -> f acc c
+ | Evar (_,l) -> Array.fold_left f acc l
+ | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+ | CoFix (_,(lna,tl,bl)) ->
+ Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+
+let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
+ (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
+
+let eq_constr sigma c1 c2 =
+ let kind c = kind_upto sigma c in
+ let rec eq_constr c1 c2 =
+ compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2
+ in
+ eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+let eq_constr_nounivs sigma c1 c2 =
+ let kind c = kind_upto sigma c in
+ let rec eq_constr c1 c2 =
+ compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2
+ in
+ eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+let compare_constr sigma cmp c1 c2 =
+ let kind c = kind_upto sigma c in
+ let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
+ compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+(** TODO: factorize with universes.ml *)
+let test_constr_universes sigma leq m n =
+ let open Universes in
+ let kind c = kind_upto sigma c in
+ if m == n then Some Constraints.empty
+ else
+ let cstrs = ref Constraints.empty in
+ let eq_universes strict l l' =
+ cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+ let eq_sorts s1 s2 =
+ if Sorts.equal s1 s2 then true
+ else (cstrs := Constraints.add
+ (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
+ true)
+ in
+ let leq_sorts s1 s2 =
+ if Sorts.equal s1 s2 then true
+ else
+ (cstrs := Constraints.add
+ (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs;
+ true)
+ in
+ let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in
+ let res =
+ if leq then
+ let rec compare_leq m n =
+ Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n
+ and leq_constr' m n = m == n || compare_leq m n in
+ compare_leq m n
+ else
+ Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n
+ in
+ if res then Some !cstrs else None
+
+let eq_constr_universes sigma m n =
+ test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+let leq_constr_universes sigma m n =
+ test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+
+let compare_head_gen_proj env sigma equ eqs eqc' m n =
+ let kind c = kind_upto sigma c in
+ match kind_upto sigma m, kind_upto sigma n with
+ | Proj (p, c), App (f, args)
+ | App (f, args), Proj (p, c) ->
+ (match kind_upto sigma f with
+ | Const (p', u) when Constant.equal (Projection.constant p) p' ->
+ let pb = Environ.lookup_projection p env in
+ let npars = pb.Declarations.proj_npars in
+ if Array.length args == npars + 1 then
+ eqc' c args.(npars)
+ else false
+ | _ -> false)
+ | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n
+
+let eq_constr_universes_proj env sigma m n =
+ let open Universes in
+ if m == n then Some Constraints.empty
+ else
+ let cstrs = ref Constraints.empty in
+ let eq_universes strict l l' =
+ cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+ let eq_sorts s1 s2 =
+ if Sorts.equal s1 s2 then true
+ else
+ (cstrs := Constraints.add
+ (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+ true)
+ in
+ let rec eq_constr' m n =
+ m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n
+ in
+ let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
+ if res then Some !cstrs else None
+
+module Vars =
+struct
+exception LocalOccur
+let to_constr = unsafe_to_constr
+
+(** Operations that commute with evar-normalization *)
+let lift n c = of_constr (Vars.lift n (to_constr c))
+let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
+
+let substnl subst n c = of_constr (Vars.substnl (List.map to_constr subst) n (to_constr c))
+let substl subst c = of_constr (Vars.substl (List.map to_constr subst) (to_constr c))
+let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
+
+let replace_vars subst c =
+ let map (id, c) = (id, to_constr c) in
+ of_constr (Vars.replace_vars (List.map map subst) (to_constr c))
+let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
+let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
+let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
+
+let subst_univs_level_constr subst c =
+ of_constr (Vars.subst_univs_level_constr subst (to_constr c))
+(** Operations that dot NOT commute with evar-normalization *)
+let noccurn sigma n term =
+ let rec occur_rec n c = match kind sigma c with
+ | Rel m -> if Int.equal m n then raise LocalOccur
+ | _ -> iter_with_binders sigma succ occur_rec n c
+ in
+ try occur_rec n term; true with LocalOccur -> false
+
+let noccur_between sigma n m term =
+ let rec occur_rec n c = match kind sigma c with
+ | Rel p -> if n<=p && p<n+m then raise LocalOccur
+ | _ -> iter_with_binders sigma succ occur_rec n c
+ in
+ try occur_rec n term; true with LocalOccur -> false
+
+let closedn sigma n c =
+ let rec closed_rec n c = match kind sigma c with
+ | Rel m -> if m>n then raise LocalOccur
+ | _ -> iter_with_binders sigma succ closed_rec n c
+ in
+ try closed_rec n c; true with LocalOccur -> false
+
+let closed0 sigma c = closedn sigma 0 c
+
+let subst_of_rel_context_instance ctx subst =
+ List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst))
+
+end
+
+let rec isArity sigma c =
+ match kind sigma c with
+ | Prod (_,_,c) -> isArity sigma c
+ | LetIn (_,b,_,c) -> isArity sigma (Vars.subst1 b c)
+ | Cast (c,_,_) -> isArity sigma c
+ | Sort _ -> true
+ | _ -> false
+
+let mkProd_or_LetIn decl c =
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (na,t) -> mkProd (na, t, c)
+ | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkLambda_or_LetIn decl c =
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (na,t) -> mkLambda (na, t, c)
+ | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
+let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
+
+let mkNamedProd_or_LetIn decl c =
+ let open Context.Named.Declaration in
+ match decl with
+ | LocalAssum (id,t) -> mkNamedProd id t c
+ | LocalDef (id,b,t) -> mkNamedLetIn id b t c
+
+let mkNamedLambda_or_LetIn decl c =
+ let open Context.Named.Declaration in
+ match decl with
+ | LocalAssum (id,t) -> mkNamedLambda id t c
+ | LocalDef (id,b,t) -> mkNamedLetIn id b t c
+
+let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
+let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
+
+open Context
+open Environ
+
+let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
+
+let cast_rel_decl :
+ type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
+ fun Refl x -> x
+
+let cast_rel_context :
+ type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
+ fun Refl x -> x
+
+let cast_named_decl :
+ type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
+ fun Refl x -> x
+
+let cast_named_context :
+ type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
+ fun Refl x -> x
+
+let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
+let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
+let push_named d e = push_named (cast_named_decl unsafe_eq d) e
+let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e
+let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e
+
+let rel_context e = cast_rel_context (sym unsafe_eq) (rel_context e)
+let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
+
+let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
+let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
+
+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_sorts = ESorts.unsafe_to_sorts
+let to_instance = EInstance.unsafe_to_instance
+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
new file mode 100644
index 000000000..3a9469e55
--- /dev/null
+++ b/engine/eConstr.mli
@@ -0,0 +1,282 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CSig
+open Names
+open Constr
+open Context
+open Environ
+
+type t
+(** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
+ that {!Constr.kind} does not observe defined evars. *)
+
+type types = t
+type constr = t
+type existential = t pexistential
+type fixpoint = (t, t) pfixpoint
+type cofixpoint = (t, t) pcofixpoint
+type unsafe_judgment = (constr, types) Environ.punsafe_judgment
+type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_context = (constr, types) Context.Named.pt
+type rel_context = (constr, types) Context.Rel.pt
+
+(** {5 Universe variables} *)
+
+module ESorts :
+sig
+ type t
+ (** Type of sorts up-to universe unification. Essentially a wrapper around
+ Sorts.t so that normalization is ensured statically. *)
+
+ val make : Sorts.t -> t
+ (** Turn a sort into an up-to sort. *)
+
+ val kind : Evd.evar_map -> t -> Sorts.t
+ (** Returns the view into the current sort. Note that the kind of a variable
+ may change if the unification state of the evar map changes. *)
+
+end
+
+module EInstance :
+sig
+ type t
+ (** Type of universe instances up-to universe unification. Similar to
+ {ESorts.t} for {Univ.Instance.t}. *)
+
+ val make : Univ.Instance.t -> t
+ val kind : Evd.evar_map -> t -> Univ.Instance.t
+ val empty : t
+ val is_empty : t -> bool
+end
+
+(** {5 Destructors} *)
+
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
+(** Same as {!Constr.kind} except that it expands evars and normalizes
+ universes on the fly. *)
+
+val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+
+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, ESorts.t, EInstance.t) Constr.kind_of_term -> t
+(** Construct a term from a view. *)
+
+val of_constr : Constr.t -> t
+(** Translate a kernel term into an incomplete term in O(1). *)
+
+(** {5 Insensitive primitives}
+
+ Evar-insensitive versions of the corresponding functions. See the {!Constr}
+ module for more information.
+
+*)
+
+(** {6 Constructors} *)
+
+val mkRel : int -> t
+val mkVar : Id.t -> t
+val mkMeta : metavariable -> t
+val mkEvar : t pexistential -> t
+val mkSort : Sorts.t -> t
+val mkProp : t
+val mkSet : t
+val mkType : Univ.universe -> t
+val mkCast : t * cast_kind * t -> t
+val mkProd : Name.t * t * t -> t
+val mkLambda : Name.t * t * t -> t
+val mkLetIn : Name.t * t * t * t -> t
+val mkApp : t * t array -> t
+val mkConst : constant -> t
+val mkConstU : constant * EInstance.t -> t
+val mkProj : (projection * t) -> t
+val mkInd : inductive -> t
+val mkIndU : inductive * EInstance.t -> t
+val mkConstruct : constructor -> t
+val mkConstructU : constructor * EInstance.t -> t
+val mkConstructUi : (inductive * EInstance.t) * int -> t
+val mkCase : case_info * t * t * t array -> t
+val mkFix : (t, t) pfixpoint -> t
+val mkCoFix : (t, t) pcofixpoint -> t
+val mkArrow : t -> t -> t
+
+val applist : t * t list -> t
+
+val mkProd_or_LetIn : rel_declaration -> t -> t
+val mkLambda_or_LetIn : rel_declaration -> t -> t
+val it_mkProd_or_LetIn : t -> rel_context -> t
+val it_mkLambda_or_LetIn : t -> rel_context -> t
+
+val mkNamedLambda : Id.t -> types -> constr -> constr
+val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t -> types -> types -> types
+val mkNamedLambda_or_LetIn : named_declaration -> types -> types
+val mkNamedProd_or_LetIn : named_declaration -> types -> types
+
+(** {6 Simple case analysis} *)
+
+val isRel : Evd.evar_map -> t -> bool
+val isVar : Evd.evar_map -> t -> bool
+val isInd : Evd.evar_map -> t -> bool
+val isEvar : Evd.evar_map -> t -> bool
+val isMeta : Evd.evar_map -> t -> bool
+val isSort : Evd.evar_map -> t -> bool
+val isCast : Evd.evar_map -> t -> bool
+val isApp : Evd.evar_map -> t -> bool
+val isLambda : Evd.evar_map -> t -> bool
+val isLetIn : Evd.evar_map -> t -> bool
+val isProd : Evd.evar_map -> t -> bool
+val isConst : Evd.evar_map -> t -> bool
+val isConstruct : Evd.evar_map -> t -> bool
+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
+val isArity : Evd.evar_map -> t -> bool
+val isVarId : Evd.evar_map -> Id.t -> t -> bool
+val isRelN : Evd.evar_map -> int -> t -> bool
+
+val destRel : Evd.evar_map -> t -> int
+val destMeta : Evd.evar_map -> t -> metavariable
+val destVar : Evd.evar_map -> t -> Id.t
+val destSort : Evd.evar_map -> t -> ESorts.t
+val destCast : Evd.evar_map -> t -> t * cast_kind * t
+val destProd : Evd.evar_map -> t -> Name.t * types * types
+val destLambda : Evd.evar_map -> t -> Name.t * types * t
+val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
+val destApp : Evd.evar_map -> t -> t * t array
+val destConst : Evd.evar_map -> t -> constant * EInstance.t
+val destEvar : Evd.evar_map -> t -> t pexistential
+val destInd : Evd.evar_map -> t -> inductive * EInstance.t
+val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
+val destCase : Evd.evar_map -> t -> case_info * t * t * t array
+val destProj : Evd.evar_map -> t -> projection * t
+val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
+val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+
+val decompose_app : Evd.evar_map -> t -> t * t list
+
+val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+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
+
+val existential_type : Evd.evar_map -> existential -> types
+val whd_evar : Evd.evar_map -> constr -> constr
+
+(** {6 Equality} *)
+
+val eq_constr : Evd.evar_map -> t -> t -> bool
+val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
+val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
+
+(** {6 Iterators} *)
+
+val map : Evd.evar_map -> (t -> t) -> t -> t
+val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
+val iter : Evd.evar_map -> (t -> unit) -> t -> unit
+val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
+
+(** {6 Substitutions} *)
+
+module Vars :
+sig
+val lift : int -> t -> t
+val liftn : int -> int -> t -> t
+val substnl : t list -> int -> t -> t
+val substl : t list -> t -> t
+val subst1 : t -> t -> t
+
+val replace_vars : (Id.t * t) list -> t -> t
+val substn_vars : int -> Id.t list -> t -> t
+val subst_vars : Id.t list -> t -> t
+val subst_var : Id.t -> t -> t
+
+val noccurn : Evd.evar_map -> int -> t -> bool
+val noccur_between : Evd.evar_map -> int -> int -> t -> bool
+
+val closedn : Evd.evar_map -> int -> t -> bool
+val closed0 : Evd.evar_map -> t -> bool
+
+val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+val subst_of_rel_context_instance : rel_context -> t list -> t list
+
+
+end
+
+(** {5 Environment handling} *)
+
+val push_rel : rel_declaration -> env -> env
+val push_rel_context : rel_context -> env -> env
+
+val push_named : named_declaration -> env -> env
+val push_named_context : named_context -> env -> env
+val push_named_context_val : named_declaration -> named_context_val -> named_context_val
+
+val rel_context : env -> rel_context
+val named_context : env -> named_context
+
+val val_of_named_context : named_context -> named_context_val
+val named_context_of_val : named_context_val -> named_context
+
+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 :
+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 to_sorts : ESorts.t -> Sorts.t
+ (** Physical identity. Does not care for normalization. *)
+
+ val to_instance : EInstance.t -> Univ.Instance.t
+ (** Physical identity. Does not care for normalization. *)
+
+ val eq : (t, Constr.t) eq
+ (** Use for transparent cast between types. *)
+end
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 53cbbd73e..1b670d366 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,9 +1,10 @@
Logic_monad
-Namegen
Universes
UState
Evd
Sigma
+EConstr
+Namegen
Termops
Proofview_monad
Evarutil
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13444cb37..1624dc93e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -21,10 +21,6 @@ open Sigma.Notations
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-let safe_evar_info sigma evk =
- try Some (Evd.find sigma evk)
- with Not_found -> None
-
let safe_evar_value sigma ev =
try Some (Evd.existential_value sigma ev)
with NotInstantiatedEvar | Not_found -> None
@@ -47,10 +43,11 @@ let evd_comb2 f evdref x y =
z
let e_new_global evdref x =
- evd_comb1 (Evd.fresh_global (Global.env())) evdref x
+ EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x)
let new_global evd x =
- Sigma.fresh_global (Global.env()) evd x
+ let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in
+ Sigma (EConstr.of_constr c, sigma, p)
(****************************************************)
(* Expanding/testing/exposing existential variables *)
@@ -68,34 +65,15 @@ let rec flush_and_check_evars sigma c =
| Some c -> flush_and_check_evars sigma c)
| _ -> map_constr (flush_and_check_evars sigma) c
-(* let nf_evar_key = Profile.declare_profile "nf_evar" *)
-(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
+let flush_and_check_evars sigma c =
+ flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
-let rec whd_evar sigma c =
- match kind_of_term c with
- | Evar (evk, args) ->
- begin match safe_evar_info sigma evk with
- | Some ({ evar_body = Evar_defined c } as info) ->
- let args = Array.map (fun c -> whd_evar sigma c) args in
- let c = instantiate_evar_array info c args in
- whd_evar sigma c
- | _ -> c
- end
- | Sort (Type u) ->
- let u' = Evd.normalize_universe sigma u in
- if u' == u then c else mkSort (Sorts.sort_of_univ u')
- | Const (c', u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkConstU (c', u')
- | Ind (i, u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkIndU (i, u')
- | Construct (co, u) when not (Univ.Instance.is_empty u) ->
- let u' = Evd.normalize_universe_instance sigma u in
- if u' == u then c else mkConstructU (co, u')
- | _ -> c
-
-let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
+(** Term exploration up to instantiation. *)
+let kind_of_term_upto = EConstr.kind_upto
+
+let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t)
+let whd_evar = EConstr.whd_evar
+let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c)
let j_nf_evar sigma j =
{ uj_val = nf_evar sigma j.uj_val;
@@ -120,23 +98,23 @@ let e_nf_evars_and_universes evdref =
let nf_evar_map_universes evm =
let evm = Evd.nf_constraints evm in
let subst = Evd.universe_subst evm in
- if Univ.LMap.is_empty subst then evm, nf_evar evm
+ if Univ.LMap.is_empty subst then evm, nf_evar0 evm
else
let f = nf_evars_universes evm in
Evd.raw_map (fun _ -> map_evar_info f) evm, f
let nf_named_context_evar sigma ctx =
- Context.Named.map (nf_evar sigma) ctx
+ Context.Named.map (nf_evar0 sigma) ctx
let nf_rel_context_evar sigma ctx =
Context.Rel.map (nf_evar sigma) ctx
let nf_env_evar sigma env =
let nc' = nf_named_context_evar sigma (Environ.named_context env) in
- let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
- push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
+ let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
+ EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
-let nf_evar_info evc info = map_evar_info (nf_evar evc) info
+let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
let nf_evar_map evm =
Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
@@ -148,21 +126,11 @@ let nf_evar_map_undefined evm =
(* Auxiliary functions for the conversion algorithms modulo evars
*)
-(* A probably faster though more approximative variant of
- [has_undefined (nf_evar c)]: instances are not substituted and
- maybe an evar occurs in an instance and it would disappear by
- instantiation *)
-
let has_undefined_evars evd t =
let rec has_ev t =
- match kind_of_term t with
- | Evar (ev,args) ->
- (match evar_body (Evd.find evd ev) with
- | Evar_defined c ->
- has_ev c; Array.iter has_ev args
- | Evar_empty ->
- raise NotInstantiatedEvar)
- | _ -> iter_constr has_ev t in
+ match EConstr.kind evd t with
+ | Evar _ -> raise NotInstantiatedEvar
+ | _ -> EConstr.iter evd has_ev t in
try let _ = has_ev t in false
with (Not_found | NotInstantiatedEvar) -> true
@@ -171,10 +139,10 @@ let is_ground_term evd t =
let is_ground_env evd env =
let is_ground_rel_decl = function
- | RelDecl.LocalDef (_,b,_) -> is_ground_term evd b
+ | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
| _ -> true in
let is_ground_named_decl = function
- | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd b
+ | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
| _ -> true in
List.for_all is_ground_rel_decl (rel_context env) &&
List.for_all is_ground_named_decl (named_context env)
@@ -193,7 +161,9 @@ let is_ground_env = memo is_ground_env
exception NoHeadEvar
-let head_evar =
+let head_evar sigma c =
+ (** FIXME: this breaks if using evar-insensitive code *)
+ let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind_of_term c with
| Evar (evk,_) -> evk
| Case (_,_,c,_) -> hrec c
@@ -202,33 +172,24 @@ let head_evar =
| Proj (p, c) -> hrec c
| _ -> raise NoHeadEvar
in
- hrec
+ hrec c
(* Expand head evar if any (currently consider only applications but I
guess it should consider Case too) *)
let whd_head_evar_stack sigma c =
- let rec whrec (c, l as s) =
- match kind_of_term c with
- | Evar (evk,args as ev) ->
- let v =
- try Some (existential_value sigma ev)
- with NotInstantiatedEvar | Not_found -> None in
- begin match v with
- | None -> s
- | Some c -> whrec (c, l)
- end
+ let rec whrec (c, l) =
+ match EConstr.kind sigma c with
| Cast (c,_,_) -> whrec (c, l)
| App (f,args) -> whrec (f, args :: l)
- | _ -> s
+ | c -> (EConstr.of_kind c, l)
in
whrec (c, [])
let whd_head_evar sigma c =
+ let open EConstr in
let (f, args) = whd_head_evar_stack sigma c in
- (** optim: don't reallocate if empty/singleton *)
match args with
- | [] -> f
| [arg] -> mkApp (f, arg)
| _ -> mkApp (f, Array.concat args)
@@ -243,7 +204,7 @@ let new_meta =
let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
fun () -> incr meta_ctr; !meta_ctr
-let mk_new_meta () = mkMeta(new_meta())
+let mk_new_meta () = EConstr.mkMeta(new_meta())
(* The list of non-instantiated existential declarations (order is important) *)
@@ -297,17 +258,20 @@ let make_pure_subst evi args =
*)
let csubst_subst (k, s) c =
+ (** Safe because this is a substitution *)
+ let c = EConstr.Unsafe.to_constr c in
let rec subst n c = match Constr.kind c with
| Rel m ->
if m <= n then c
- else if m - n <= k then Int.Map.find (k - m + n) s
+ else if m - n <= k then EConstr.Unsafe.to_constr (Int.Map.find (k - m + n) s)
else mkRel (m - k)
| _ -> Constr.map_with_binders succ subst n c
in
- if k = 0 then c else subst 0 c
+ let c = if k = 0 then c else subst 0 c in
+ EConstr.of_constr c
let subst2 subst vsubst c =
- csubst_subst subst (replace_vars vsubst c)
+ csubst_subst subst (EConstr.Vars.replace_vars vsubst c)
let next_ident_away id avoid =
let avoid id = Id.Set.mem id avoid in
@@ -318,24 +282,29 @@ let next_name_away na avoid =
let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
next_ident_away_from id avoid
-type csubst = int * Constr.t Int.Map.t
+type csubst = int * EConstr.t Int.Map.t
let empty_csubst = (0, Int.Map.empty)
type ext_named_context =
- csubst * (Id.t * Constr.constr) list *
- Id.Set.t * Context.Named.t
+ csubst * (Id.t * EConstr.constr) list *
+ Id.Set.t * EConstr.named_context
let push_var id (n, s) =
- let s = Int.Map.add n (mkVar id) s in
+ let s = Int.Map.add n (EConstr.mkVar id) s in
(succ n, s)
-let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
+let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
+ let open EConstr in
+ let open Vars in
+ let map_decl f d =
+ NamedDecl.map_constr f d
+ in
let replace_var_named_declaration id0 id decl =
let id' = NamedDecl.get_id decl in
let id' = if Id.equal id0 id' then id else id' in
let vsubst = [id0 , mkVar id] in
- decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst)
+ decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst)
in
let extract_if_neq id = function
| Anonymous -> None
@@ -353,7 +322,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
else
(** id_of_name_using_hdchar only depends on the rel context which is empty
here *)
- next_ident_away (id_of_name_using_hdchar empty_env (RelDecl.get_type decl) na) avoid
+ next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
in
match extract_if_neq id na with
| Some id0 when not (is_section_variable id0) ->
@@ -363,7 +332,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
context. Unless [id] is a section variable. *)
let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in
let vsubst = (id0,mkVar id)::vsubst in
- let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> NamedDecl.map_constr (subst2 subst vsubst) in
+ let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (subst2 subst vsubst) in
let nc = List.map (replace_var_named_declaration id0 id) nc in
(push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc)
| _ ->
@@ -371,12 +340,13 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
incorrect. We revert to a less robust behaviour where
the new binder has name [id]. Which amounts to the same
behaviour than when [id=id0]. *)
- let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> NamedDecl.map_constr (subst2 subst vsubst) in
+ let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in
(push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
-let push_rel_context_to_named_context env typ =
+let push_rel_context_to_named_context env sigma typ =
(* compute the instances relative to the named context and rel_context *)
let open Context.Named.Declaration in
+ let open EConstr in
let ids = List.map get_id (named_context env) in
let inst_vars = List.map mkVar ids in
if List.is_empty (Environ.rel_context env) then
@@ -388,7 +358,7 @@ let push_rel_context_to_named_context env typ =
(* with vars of the rel context *)
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, vsubst, _, env) =
- Context.Rel.fold_outside push_rel_decl_to_named_context
+ Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
(rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
(val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
@@ -400,6 +370,7 @@ let default_source = (Loc.ghost,Evar_kinds.InternalHole)
let restrict_evar evd evk filter candidates =
let evd = Sigma.to_evar_map evd in
+ let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
let evd, evk' = Evd.restrict evk filter ?candidates evd in
Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
@@ -410,9 +381,19 @@ let new_pure_evar_full evd evi =
Sigma.Unsafe.of_pair (evk, evd)
let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+ let typ = EConstr.Unsafe.to_constr typ in
let evd = Sigma.to_evar_map evd in
+ let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
let default_naming = Misctypes.IntroAnonymous in
let naming = Option.default default_naming naming in
+ let name = match naming with
+ | Misctypes.IntroAnonymous -> None
+ | Misctypes.IntroIdentifier id -> Some id
+ | Misctypes.IntroFresh id ->
+ let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
+ let id = Namegen.next_ident_away_from id has_name in
+ Some id
+ in
let evi = {
evar_hyps = sign;
evar_concl = typ;
@@ -422,7 +403,7 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
evar_candidates = candidates;
evar_extra = store; }
in
- let (evd, newevk) = Evd.new_evar evd ~naming evi in
+ let (evd, newevk) = Evd.new_evar evd ?name evi in
let evd =
if principal then Evd.declare_principal_goal newevk evd
else Evd.declare_future_goal newevk evd
@@ -430,6 +411,7 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
Sigma.Unsafe.of_pair (newevk, evd)
let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+ let open EConstr in
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
@@ -438,8 +420,9 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
- let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
- let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
+ let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env (Sigma.to_evar_map evd) typ in
+ let map c = subst2 subst vsubst c in
+ let candidates = Option.map (fun l -> List.map map l) candidates in
let instance =
match filter with
| None -> instance
@@ -453,7 +436,7 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
- let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+ let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in
Sigma ((e, s), evd', p +> q)
let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
@@ -464,12 +447,13 @@ let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
c
let new_Type ?(rigid=Evd.univ_flexible) env evd =
+ let open EConstr in
let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
Sigma (mkSort s, sigma, p)
let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
let evd', s = new_sort_variable rigid !evdref in
- evdref := evd'; mkSort s
+ evdref := evd'; EConstr.mkSort s
(* The same using side-effect *)
let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
@@ -480,12 +464,13 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
(* This assumes an evar with identity instance and generalizes it over only
the De Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
+ let open EConstr in
let evi = Evd.find sigma ev in
let sign = named_context_of_val evi.evar_hyps in
List.fold_left2
(fun (c,inst as x) a d ->
- if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
- (evi.evar_concl,[]) (Array.to_list args) sign
+ if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+ (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign
(************************************)
(* Removing a dependency in an evar *)
@@ -523,7 +508,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
| Evar (evk,l as ev) ->
if Evd.is_defined !evdref evk then
(* If evk is already defined we replace it by its definition *)
- let nc = whd_evar !evdref c in
+ let nc = Evd.existential_value !evdref ev in
(check_and_clear_in_constr env evdref err ids global nc)
else
(* We check for dependencies to elements of ids in the
@@ -533,6 +518,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
removed *)
let evi = Evd.find_undefined !evdref evk in
let ctxt = Evd.evar_filtered_context evi in
+ let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in
let (rids,filter) =
List.fold_right2
(fun h a (ri,filter) ->
@@ -540,12 +526,12 @@ let rec check_and_clear_in_constr env evdref err ids global c =
(* Check if some id to clear occurs in the instance
a of rid in ev and remember the dependency *)
let check id = if Id.Set.mem id ids then raise (Depends id) in
- let () = Id.Set.iter check (collect_vars a) in
+ let () = Id.Set.iter check (collect_vars !evdref (EConstr.of_constr a)) in
(* Check if some rid to clear in the context of ev
has dependencies in another hyp of the context of ev
and transitively remember the dependency *)
let check id _ =
- if occur_var_in_decl (Global.env ()) id h
+ if occur_var_in_decl (Global.env ()) !evdref id h
then raise (Depends id)
in
let () = Id.Map.iter check ri in
@@ -578,7 +564,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
let evi' = { evi with evar_extra = extra' } in
evdref := Evd.add !evdref evk evi' ;
(* spiwack: /hacking session *)
- whd_evar !evdref c
+ Evd.existential_value !evdref ev
| _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
@@ -586,6 +572,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
hypothesis does not depend on a element of ids, and erases ids in
the contexts of the evars occurring in evi *)
+ let terms = List.map EConstr.Unsafe.to_constr terms in
let global = Id.Set.exists is_section_variable ids in
let terms =
List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in
@@ -607,7 +594,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
in
remove_hyps ids check_context check_value hyps
in
- (nhyps,terms)
+ (nhyps,List.map EConstr.of_constr terms)
let clear_hyps_in_evi env evdref hyps concl ids =
match clear_hyps_in_evi_main env evdref hyps [concl] ids with
@@ -696,29 +683,26 @@ let rec advance sigma evk =
let undefined_evars_of_term evd t =
let rec evrec acc c =
- match kind_of_term c with
+ match EConstr.kind evd c with
| Evar (n, l) ->
- let acc = Array.fold_left evrec acc l in
- (try match (Evd.find evd n).evar_body with
- | Evar_empty -> Evar.Set.add n acc
- | Evar_defined c -> evrec acc c
- with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
- | _ -> fold_constr evrec acc c
+ let acc = Evar.Set.add n acc in
+ Array.fold_left evrec acc l
+ | _ -> EConstr.fold evd evrec acc c
in
evrec Evar.Set.empty t
let undefined_evars_of_named_context evd nc =
Context.Named.fold_outside
- (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+ (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
nc
~init:Evar.Set.empty
let undefined_evars_of_evar_info evd evi =
- Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+ Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
(Evar.Set.union
(match evi.evar_body with
| Evar_empty -> Evar.Set.empty
- | Evar_defined b -> undefined_evars_of_term evd b)
+ | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
(undefined_evars_of_named_context evd
(named_context_of_val evi.evar_hyps)))
@@ -727,6 +711,7 @@ let undefined_evars_of_evar_info evd evi =
[evar_map]. If unification only need to check superficially, tactics
do not have this luxury, and need the more complete version. *)
let occur_evar_upto sigma n c =
+ let c = EConstr.Unsafe.to_constr c in
let rec occur_rec c = match kind_of_term c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
| Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
@@ -738,6 +723,7 @@ let occur_evar_upto sigma n c =
any type has type Type. May cause some trouble, but not so far... *)
let judge_of_new_Type evd =
+ let open EConstr in
let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
@@ -748,10 +734,6 @@ let subterm_source evk (loc,k) =
(loc,Evar_kinds.SubEvar evk)
-(** Term exploration up to instantiation. *)
-let kind_of_term_upto sigma t =
- Constr.kind (whd_evar sigma t)
-
(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
[u] up to existential variable instantiation and equalisable
universes. The term [t] is interpreted in [sigma1] while [u] is
@@ -772,5 +754,5 @@ let eq_constr_univs_test sigma1 sigma2 t u =
in
match ans with None -> false | Some _ -> true
-type type_constraint = types option
-type val_constraint = constr option
+type type_constraint = EConstr.types option
+type val_constraint = EConstr.constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 7fdc7aac7..ca9591e71 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -10,6 +10,7 @@ open Names
open Term
open Evd
open Environ
+open EConstr
(** This module provides useful higher-level functions for evar manipulation. *)
@@ -76,9 +77,9 @@ val new_evar_instance :
?principal:bool ->
constr list -> (constr, 'r) Sigma.sigma
-val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
+val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
-val safe_evar_value : evar_map -> existential -> constr option
+val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
(** {6 Evars/Metas switching...} *)
@@ -88,7 +89,7 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t
(** [head_evar c] returns the head evar of [c] if any *)
exception NoHeadEvar
-val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
+val head_evar : evar_map -> constr -> existential_key (** may raise NoHeadEvar *)
(* Expand head evar if any *)
val whd_head_evar : evar_map -> constr -> constr
@@ -128,7 +129,7 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
[c]. It looks up recursively in [sigma] for the value of existential
variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
+val occur_evar_upto : evar_map -> Evar.t -> constr -> bool
(** {6 Value/Type constraints} *)
@@ -150,7 +151,7 @@ val tj_nf_evar :
evar_map -> unsafe_type_judgment -> unsafe_type_judgment
val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
-val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
+val nf_rel_context_evar : evar_map -> rel_context -> rel_context
val nf_env_evar : evar_map -> env -> env
val nf_evar_info : evar_map -> evar_info -> evar_info
@@ -159,39 +160,40 @@ val nf_evar_map_undefined : evar_map -> evar_map
(** Presenting terms without solved evars *)
-val nf_evars_universes : evar_map -> constr -> constr
+val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
-val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
-val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
+val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
(** Normalize the evar map w.r.t. universes, after simplification of constraints.
Return the substitution function for constrs as well. *)
-val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
+val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
exception Uninstantiated_evar of existential_key
-val flush_and_check_evars : evar_map -> constr -> constr
+val flush_and_check_evars : evar_map -> constr -> Constr.constr
(** {6 Term manipulation up to instantiation} *)
(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+val kind_of_term_upto : evar_map -> Constr.constr ->
+ (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
[u] up to existential variable instantiation and equalisable
universes. The term [t] is interpreted in [sigma1] while [u] is
interpreted in [sigma2]. The universe constraints in [sigma2] are
assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
(** {6 Removing hyps in evars'context}
raise OccurHypInSimpleClause if the removal breaks dependencies *)
type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
+| EvarTypingBreak of Constr.existential
exception ClearDependencyError of Id.t * clear_dependency_error
@@ -208,16 +210,16 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
type csubst
val empty_csubst : csubst
-val csubst_subst : csubst -> Constr.t -> Constr.t
+val csubst_subst : csubst -> constr -> constr
type ext_named_context =
- csubst * (Id.t * Constr.constr) list *
- Id.Set.t * Context.Named.t
+ csubst * (Id.t * constr) list *
+ Id.Set.t * named_context
val push_rel_decl_to_named_context :
- Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+ evar_map -> rel_declaration -> ext_named_context -> ext_named_context
-val push_rel_context_to_named_context : Environ.env -> types ->
+val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
named_context_val * types * constr list * csubst * (identifier*constr) list
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/engine/evd.ml b/engine/evd.ml
index b7d56a698..5419a10a8 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -258,7 +258,6 @@ type evar_universe_context = UState.t
type 'a in_evar_universe_context = 'a * evar_universe_context
let empty_evar_universe_context = UState.empty
-let is_empty_evar_universe_context = UState.is_empty
let union_evar_universe_context = UState.union
let evar_universe_context_set = UState.context_set
let evar_universe_context_constraints = UState.constraints
@@ -366,7 +365,7 @@ open Misctypes
type t
val empty : t
-val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : Id.t option -> Evar.t -> evar_info -> t -> t
val remove_name_defined : Evar.t -> t -> t
val rename : Evar.t -> Id.t -> t -> t
val reassign_name_defined : Evar.t -> Evar.t -> t -> t
@@ -380,20 +379,13 @@ type t = Id.t EvMap.t * existential_key Idmap.t
let empty = (EvMap.empty, Idmap.empty)
-let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
- let id = match naming with
- | Misctypes.IntroAnonymous -> None
- | Misctypes.IntroIdentifier id ->
- if Idmap.mem id idtoev then
- user_err (str "Already an existential evar of name " ++ pr_id id);
- Some id
- | Misctypes.IntroFresh id ->
- let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- Some id
- in
+let add_name_newly_undefined id evk evi (evtoid, idtoev as names) =
match id with
| None -> names
- | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+ | Some id ->
+ if Idmap.mem id idtoev then
+ user_err (str "Already an existential evar of name " ++ pr_id id);
+ (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
if EvMap.mem evk evtoid then
@@ -463,9 +455,9 @@ type evar_map = {
let rename evk id evd =
{ evd with evar_names = EvNames.rename evk id evd.evar_names }
-let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
+let add_with_name ?name d e i = match i.evar_body with
| Evar_empty ->
- let evar_names = EvNames.add_name_undefined naming e i d.evar_names in
+ let evar_names = EvNames.add_name_undefined name e i d.evar_names in
{ d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
| Evar_defined _ ->
let evar_names = EvNames.remove_name_defined e d.evar_names in
@@ -482,9 +474,9 @@ let new_untyped_evar =
let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
-let new_evar evd ?naming evi =
+let new_evar evd ?name evi =
let evk = new_untyped_evar () in
- let evd = add_with_name evd ?naming evk evi in
+ let evd = add_with_name evd ?name evk evi in
(evd, evk)
let remove d e =
@@ -505,15 +497,6 @@ let find_undefined d e = EvMap.find e d.undf_evars
let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
-(* spiwack: this function loses information from the original evar_map
- it might be an idea not to export it. *)
-let to_list d =
- (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
- let l = ref [] in
- EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
- EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
- !l
-
let undefined_map d = d.undf_evars
let drop_all_defined d = { d with defn_evars = EvMap.empty }
@@ -732,13 +715,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
(* excluding defined evars *)
-let evar_list c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (evk, _ as ev) -> ev :: acc
- | _ -> Term.fold_constr evrec acc c in
- evrec [] c
-
let evars_of_term c =
let rec evrec acc c =
match kind_of_term c with
@@ -776,7 +752,6 @@ let evar_universe_context d = d.universes
let universe_context_set d = UState.context_set d.universes
-let pr_uctx_level = UState.pr_uctx_level
let universe_context ?names evd = UState.universe_context ?names evd.universes
let restrict_universe_context evd vars =
@@ -958,37 +933,8 @@ let universes evd = UState.ugraph evd.universes
let update_sigma_env evd env =
{ evd with universes = UState.update_sigma_env evd.universes env }
-(* Conversion w.r.t. an evar map and its local universes. *)
-
-let test_conversion_gen env evd pb t u =
- match pb with
- | Reduction.CONV ->
- Reduction.conv env
- ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
- t u
- | Reduction.CUMUL -> Reduction.conv_leq env
- ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
- t u
-
-let test_conversion env d pb t u =
- try test_conversion_gen env d pb t u; true
- with _ -> false
-
exception UniversesDiffer = UState.UniversesDiffer
-let eq_constr_univs evd t u =
- let fold cstr sigma =
- try Some (add_universe_constraints sigma cstr)
- with Univ.UniverseInconsistency _ | UniversesDiffer -> None
- in
- match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
- | None -> evd, false
- | Some evd -> evd, true
-
-let e_eq_constr_univs evdref t u =
- let evd, b = eq_constr_univs !evdref t u in
- evdref := evd; b
-
(**********************************************************)
(* Side effects *)
@@ -1220,281 +1166,3 @@ module Monad =
(* Failure explanation *)
type unsolvability_explanation = SeveralInstancesFound of int
-
-(**********************************************************)
-(* Pretty-printing *)
-
-let pr_evar_suggested_name evk sigma =
- let base_id evk' evi =
- match evar_ident evk' sigma with
- | Some id -> id
- | None -> match evi.evar_source with
- | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
- | _,Evar_kinds.VarInstance id -> id
- | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
- | _ ->
- let env = reset_with_named_context evi.evar_hyps (Global.env()) in
- Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
- in
- let names = EvMap.mapi base_id sigma.undf_evars in
- let id = EvMap.find evk names in
- let fold evk' id' (seen, n) =
- if seen then (seen, n)
- else if Evar.equal evk evk' then (true, n)
- else if Id.equal id id' then (seen, succ n)
- else (seen, n)
- in
- let (_, n) = EvMap.fold fold names (false, 0) in
- if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
-
-let pr_existential_key sigma evk = match evar_ident evk sigma with
-| None ->
- str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
-| Some id ->
- str "?" ++ pr_id id
-
-let pr_instance_status (sc,typ) =
- begin match sc with
- | IsSubType -> str " [or a subtype of it]"
- | IsSuperType -> str " [or a supertype of it]"
- | Conv -> mt ()
- end ++
- begin match typ with
- | CoerceToType -> str " [up to coercion]"
- | TypeNotProcessed -> mt ()
- | TypeProcessed -> str " [type is checked]"
- end
-
-let protect f x =
- try f x
- with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
-
-let (f_print_constr, print_constr_hook) = Hook.make ()
-
-let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a
-
-let pr_meta_map mmap =
- let pr_name = function
- Name id -> str"[" ++ pr_id id ++ str"]"
- | _ -> mt() in
- let pr_meta_binding = function
- | (mv,Cltyp (na,b)) ->
- hov 0
- (pr_meta mv ++ pr_name na ++ str " : " ++
- print_constr b.rebus ++ fnl ())
- | (mv,Clval(na,(b,s),t)) ->
- hov 0
- (pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr b.rebus ++
- str " : " ++ print_constr t.rebus ++
- spc () ++ pr_instance_status s ++ fnl ())
- in
- prlist pr_meta_binding (metamap_to_list mmap)
-
-let pr_decl (decl,ok) =
- match decl with
- | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
- | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
- print_constr c ++ str (if ok then ")" else "}")
-
-let pr_evar_source = function
- | Evar_kinds.NamedHole id -> pr_id id
- | Evar_kinds.QuestionMark _ -> str "underscore"
- | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
- | Evar_kinds.CasesType true ->
- str "subterm of pattern-matching return predicate"
- | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
- | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
- | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
- let id = Option.get ido in
- str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
- spc () ++ print_constr (printable_constr_of_global c)
- | Evar_kinds.InternalHole -> str "internal placeholder"
- | Evar_kinds.TomatchTypeParameter (ind,n) ->
- pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
- | Evar_kinds.GoalEvar -> str "goal evar"
- | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
- | Evar_kinds.MatchingVar _ -> str "matching variable"
- | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
- | Evar_kinds.SubEvar evk ->
- str "subterm of " ++ str (string_of_existential evk)
-
-let pr_evar_info evi =
- let phyps =
- try
- let decls = match Filter.repr (evar_filter evi) with
- | None -> List.map (fun c -> (c, true)) (evar_context evi)
- | Some filter -> List.combine (evar_context evi) filter
- in
- prlist_with_sep spc pr_decl (List.rev decls)
- with Invalid_argument _ -> str "Ill-formed filtered context" in
- let pty = print_constr evi.evar_concl in
- let pb =
- match evi.evar_body with
- | Evar_empty -> mt ()
- | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
- in
- let candidates =
- match evi.evar_body, evi.evar_candidates with
- | Evar_empty, Some l ->
- spc () ++ str "{" ++
- prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
- | _ ->
- mt ()
- in
- let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
- hov 2
- (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
- candidates ++ spc() ++ src)
-
-let compute_evar_dependency_graph (sigma : evar_map) =
- (* Compute the map binding ev to the evars whose body depends on ev *)
- let fold evk evi acc =
- let fold_ev evk' acc =
- let tab =
- try EvMap.find evk' acc
- with Not_found -> Evar.Set.empty
- in
- EvMap.add evk' (Evar.Set.add evk tab) acc
- in
- match evar_body evi with
- | Evar_empty -> assert false
- | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
- in
- EvMap.fold fold sigma.defn_evars EvMap.empty
-
-let evar_dependency_closure n sigma =
- (** Create the DAG of depth [n] representing the recursive dependencies of
- undefined evars. *)
- let graph = compute_evar_dependency_graph sigma in
- let rec aux n curr accu =
- if Int.equal n 0 then Evar.Set.union curr accu
- else
- let fold evk accu =
- try
- let deps = EvMap.find evk graph in
- Evar.Set.union deps accu
- with Not_found -> accu
- in
- (** Consider only the newly added evars *)
- let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
- (** Merge the others *)
- let accu = Evar.Set.union curr accu in
- aux (n - 1) ncurr accu
- in
- let undef = EvMap.domain (undefined_map sigma) in
- aux n undef Evar.Set.empty
-
-let evar_dependency_closure n sigma =
- let deps = evar_dependency_closure n sigma in
- let map = EvMap.bind (fun ev -> find sigma ev) deps in
- EvMap.bindings map
-
-let has_no_evar sigma =
- EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
-
-let pr_evd_level evd = pr_uctx_level evd.universes
-
-let pr_evar_universe_context ctx =
- let prl = pr_uctx_level ctx in
- if is_empty_evar_universe_context ctx then mt ()
- else
- (str"UNIVERSES:"++brk(0,1)++
- h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
- str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
- h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
- str"UNDEFINED UNIVERSES:"++brk(0,1)++
- h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
-
-let print_env_short env =
- let pr_rel_decl = function
- | RelDecl.LocalAssum (n,_) -> pr_name n
- | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
- in
- let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
- let nc = List.rev (named_context env) in
- let rc = List.rev (rel_context env) in
- str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
- str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
-
-let pr_evar_constraints pbs =
- let pr_evconstr (pbty, env, t1, t2) =
- let env =
- (** We currently allow evar instances to refer to anonymous de
- Bruijn indices, so we protect the error printing code in this
- case by giving names to every de Bruijn variable in the
- rel_context of the conversion problem. MS: we should rather
- stop depending on anonymous variables, they can be used to
- indicate independency. Also, this depends on a strategy for
- naming/renaming. *)
- Namegen.make_all_name_different env
- in
- print_env_short env ++ spc () ++ str "|-" ++ spc () ++
- Hook.get f_print_constr env t1 ++ spc () ++
- str (match pbty with
- | Reduction.CONV -> "=="
- | Reduction.CUMUL -> "<=") ++
- spc () ++ Hook.get f_print_constr env t2
- in
- prlist_with_sep fnl pr_evconstr pbs
-
-let pr_evar_map_gen with_univs pr_evars sigma =
- let { universes = uvs } = sigma in
- let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
- and svs = if with_univs then pr_evar_universe_context uvs else mt ()
- and cstrs =
- if List.is_empty sigma.conv_pbs then mt ()
- else
- str "CONSTRAINTS:" ++ brk (0, 1) ++
- pr_evar_constraints sigma.conv_pbs ++ fnl ()
- and metas =
- if Metamap.is_empty sigma.metas then mt ()
- else
- str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas
- in
- evs ++ svs ++ cstrs ++ metas
-
-let pr_evar_list sigma l =
- let pr (ev, evi) =
- h 0 (str (string_of_existential ev) ++
- str "==" ++ pr_evar_info evi ++
- (if evi.evar_body == Evar_empty
- then str " {" ++ pr_existential_key sigma ev ++ str "}"
- else mt ()))
- in
- h 0 (prlist_with_sep fnl pr l)
-
-let pr_evar_by_depth depth sigma = match depth with
-| None ->
- (* Print all evars *)
- str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
-| Some n ->
- (* Print all evars *)
- str"UNDEFINED EVARS:"++
- (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
- brk(0,1)++
- pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
-
-let pr_evar_by_filter filter sigma =
- let defined = Evar.Map.filter filter sigma.defn_evars in
- let undefined = Evar.Map.filter filter sigma.undf_evars in
- let prdef =
- if Evar.Map.is_empty defined then mt ()
- else str "DEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma (Evar.Map.bindings defined)
- in
- let prundef =
- if Evar.Map.is_empty undefined then mt ()
- else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma (Evar.Map.bindings undefined)
- in
- prdef ++ prundef
-
-let pr_evar_map ?(with_univs=true) depth sigma =
- pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
-
-let pr_evar_map_filter ?(with_univs=true) filter sigma =
- pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
-
-let pr_metaset metas =
- str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/engine/evd.mli b/engine/evd.mli
index 5619b7af2..9c40c8b71 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -149,7 +149,7 @@ val has_undefined : evar_map -> bool
there are uninstantiated evars in [sigma]. *)
val new_evar : evar_map ->
- ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar
+ ?name:Id.t -> evar_info -> evar_map * evar
(** Creates a fresh evar mapping to the given information. *)
val add : evar_map -> evar -> evar_info -> evar_map
@@ -420,10 +420,6 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
contained in the object; need the term to be evar-normal otherwise
defined evars are returned too. *)
-val evar_list : constr -> existential list
- (** excluding evars in instances of evars and collected with
- redundancies from right to left (used by tactic "instantiate") *)
-
val evars_of_term : constr -> Evar.Set.t
(** including evars in instances of evars *)
@@ -584,19 +580,6 @@ val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor ->
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
evar_map -> Globnames.global_reference -> evar_map * constr
-(********************************************************************
- Conversion w.r.t. an evar map, not unifying universes. See
- [Reductionops.infer_conv] for conversion up-to universes. *)
-
-val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** WARNING: This does not allow unification of universes *)
-
-val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
-(** Syntactic equality up to universes, recording the associated constraints *)
-
-val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
-(** Syntactic equality up to universes. *)
-
(********************************************************************)
(* constr with holes and pending resolution of classes, conversion *)
(* problems, candidates, etc. *)
@@ -608,22 +591,6 @@ type open_constr = evar_map * constr (* Special case when before is empty *)
type unsolvability_explanation = SeveralInstancesFound of int
(** Failure explanation. *)
-val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
-
-val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
-
-(** {5 Debug pretty-printers} *)
-
-val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t
-val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
-val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
- evar_map -> Pp.std_ppcmds
-val pr_metaset : Metaset.t -> Pp.std_ppcmds
-val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
-val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
-
(** {5 Deprecated functions} *)
val create_evar_defs : evar_map -> evar_map
diff --git a/engine/namegen.ml b/engine/namegen.ml
index e56ec2877..3b979f206 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -15,12 +15,13 @@
open Util
open Names
open Term
+open Environ
+open EConstr
open Vars
open Nametab
open Nameops
open Libnames
open Globnames
-open Environ
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -84,13 +85,20 @@ let is_section_variable id =
(**********************************************************************)
(* Generating "intuitive" names from its type *)
-let head_name c = (* Find the head constant of a constr if any *)
+let global_of_constr = function
+| Const (c, _) -> ConstRef c
+| Ind (i, _) -> IndRef i
+| Construct (c, _) -> ConstructRef c
+| Var id -> VarRef id
+| _ -> assert false
+
+let head_name sigma c = (* Find the head constant of a constr if any *)
let rec hdrec c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
| Cast (c,_,_) | App (c,_) -> hdrec c
| Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
- | Const _ | Ind _ | Construct _ | Var _ ->
+ | Const _ | Ind _ | Construct _ | Var _ as c ->
Some (basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
Some (match lna.(i) with Name id -> id | _ -> assert false)
@@ -105,9 +113,9 @@ let sort_hdchar = function
| Prop(_) -> "P"
| Type(_) -> "T"
-let hdchar env c =
+let hdchar env sigma c =
let rec hdrec k c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
| Cast (c,_,_) | App (c,_) -> hdrec k c
| Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
@@ -115,11 +123,11 @@ let hdchar env c =
| Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
| Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
| Var id -> lowercase_first_char id
- | Sort s -> sort_hdchar s
+ | Sort s -> sort_hdchar (ESorts.kind sigma s)
| Rel n ->
(if n<=k then "p" (* the initial term is flexible product/function *)
else
- try match Environ.lookup_rel (n-k) env with
+ try match lookup_rel (n-k) env with
| LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id
| LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
with Not_found -> "y")
@@ -131,41 +139,41 @@ let hdchar env c =
in
hdrec 0 c
-let id_of_name_using_hdchar env a = function
- | Anonymous -> Id.of_string (hdchar env a)
+let id_of_name_using_hdchar env sigma a = function
+ | Anonymous -> Id.of_string (hdchar env sigma a)
| Name id -> id
-let named_hd env a = function
- | Anonymous -> Name (Id.of_string (hdchar env a))
+let named_hd env sigma a = function
+ | Anonymous -> Name (Id.of_string (hdchar env sigma a))
| x -> x
-let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b)
-let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+let mkProd_name env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b)
+let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b)
let lambda_name = mkLambda_name
let prod_name = mkProd_name
-let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b)
-let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b)
+let prod_create env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b)
+let lambda_create env sigma (a,b) = mkLambda (named_hd env sigma a Anonymous, a, b)
-let name_assumption env = function
- | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
- | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+let name_assumption env sigma = function
+ | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t)
+ | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t)
-let name_context env hyps =
+let name_context env sigma hyps =
snd
(List.fold_left
(fun (env,hyps) d ->
- let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+ let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
(env,[]) (List.rev hyps))
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
-let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b
+let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b
-let it_mkProd_or_LetIn_name env b hyps =
- it_mkProd_or_LetIn b (name_context env hyps)
-let it_mkLambda_or_LetIn_name env b hyps =
- it_mkLambda_or_LetIn b (name_context env hyps)
+let it_mkProd_or_LetIn_name env sigma b hyps =
+ it_mkProd_or_LetIn b (name_context env sigma hyps)
+let it_mkLambda_or_LetIn_name env sigma b hyps =
+ it_mkLambda_or_LetIn b (name_context env sigma hyps)
(**********************************************************************)
(* Fresh names *)
@@ -185,10 +193,10 @@ let restart_subscript id =
*** make_ident id (Some 0) *** but compatibility would be lost... *)
forget_subscript id
-let visible_ids (nenv, c) =
+let visible_ids sigma (nenv, c) =
let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
- let rec visible_ids n c = match kind_of_term c with
- | Const _ | Ind _ | Construct _ | Var _ ->
+ let rec visible_ids n c = match EConstr.kind sigma c with
+ | Const _ | Ind _ | Construct _ | Var _ as c ->
let (gseen, vseen, ids) = !accu in
let g = global_of_constr c in
if not (Refset_env.mem g gseen) then
@@ -218,7 +226,7 @@ let visible_ids (nenv, c) =
| _ -> ids
in
accu := (gseen, vseen, ids)
- | _ -> Constr.iter_with_binders succ visible_ids n c
+ | _ -> EConstr.iter_with_binders sigma succ visible_ids n c
in
let () = visible_ids 1 c in
let (_, _, ids) = !accu in
@@ -228,9 +236,9 @@ let visible_ids (nenv, c) =
(* 1- Looks for a fresh name for printing in cases pattern *)
-let next_name_away_in_cases_pattern env_t na avoid =
+let next_name_away_in_cases_pattern sigma env_t na avoid =
let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
- let visible = visible_ids env_t in
+ let visible = visible_ids sigma env_t in
let bad id = Id.List.mem id avoid || is_constructor id
|| Id.Set.mem id visible in
next_ident_away_from id bad
@@ -292,7 +300,7 @@ let next_name_away_with_default_using_types default na avoid t =
let next_name_away = next_name_away_with_default default_non_dependent_string
-let make_all_name_different env =
+let make_all_name_different env sigma =
(** FIXME: this is inefficient, but only used in printing *)
let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
let sign = named_context_val env in
@@ -300,7 +308,7 @@ let make_all_name_different env =
let env0 = reset_with_named_context sign env in
Context.Rel.fold_outside
(fun decl newenv ->
- let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in
+ let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in
let id = next_name_away na !avoid in
avoid := id::!avoid;
push_rel (RelDecl.set_name (Name id) decl) newenv)
@@ -311,12 +319,12 @@ let make_all_name_different env =
looks for name of same base with lower available subscript beyond current
subscript *)
-let next_ident_away_for_default_printing env_t id avoid =
- let visible = visible_ids env_t in
+let next_ident_away_for_default_printing sigma env_t id avoid =
+ let visible = visible_ids sigma env_t in
let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
next_ident_away_from id bad
-let next_name_away_for_default_printing env_t na avoid =
+let next_name_away_for_default_printing sigma env_t na avoid =
let id = match na with
| Name id -> id
| Anonymous ->
@@ -324,7 +332,7 @@ let next_name_away_for_default_printing env_t na avoid =
(* taken into account by the function compute_displayed_name_in; *)
(* just in case, invent a valid name *)
default_non_dependent_ident in
- next_ident_away_for_default_printing env_t id avoid
+ next_ident_away_for_default_printing sigma env_t id avoid
(**********************************************************************)
(* Displaying terms avoiding bound variables clashes *)
@@ -349,45 +357,45 @@ type renaming_flags =
| RenamingForGoal
| RenamingElsewhereFor of (Name.t list * constr)
-let next_name_for_display flags =
+let next_name_for_display sigma flags =
match flags with
- | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
+ | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t
| RenamingForGoal -> next_name_away_in_goal
- | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
+ | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in flags avoid na c =
+let compute_displayed_name_in sigma flags avoid na c =
match na with
- | Anonymous when noccurn 1 c ->
+ | Anonymous when noccurn sigma 1 c ->
(Anonymous,avoid)
| _ ->
- let fresh_id = next_name_for_display flags na avoid in
- let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
+ let fresh_id = next_name_for_display sigma flags na avoid in
+ let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
(idopt, fresh_id::avoid)
-let compute_and_force_displayed_name_in flags avoid na c =
+let compute_and_force_displayed_name_in sigma flags avoid na c =
match na with
- | Anonymous when noccurn 1 c ->
+ | Anonymous when noccurn sigma 1 c ->
(Anonymous,avoid)
| _ ->
- let fresh_id = next_name_for_display flags na avoid in
+ let fresh_id = next_name_for_display sigma flags na avoid in
(Name fresh_id, fresh_id::avoid)
-let compute_displayed_let_name_in flags avoid na c =
- let fresh_id = next_name_for_display flags na avoid in
+let compute_displayed_let_name_in sigma flags avoid na c =
+ let fresh_id = next_name_for_display sigma flags na avoid in
(Name fresh_id, fresh_id::avoid)
-let rename_bound_vars_as_displayed avoid env c =
+let rename_bound_vars_as_displayed sigma avoid env c =
let rec rename avoid env c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Prod (na,c1,c2) ->
let na',avoid' =
- compute_displayed_name_in
+ compute_displayed_name_in sigma
(RenamingElsewhereFor (env,c2)) avoid na c2 in
mkProd (na', c1, rename avoid' (na' :: env) c2)
| LetIn (na,c1,t,c2) ->
let na',avoid' =
- compute_displayed_let_name_in
+ compute_displayed_let_name_in sigma
(RenamingElsewhereFor (env,c2)) avoid na c2 in
mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
| Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 33ce9a34d..058b1c228 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -11,6 +11,8 @@
open Names
open Term
open Environ
+open Evd
+open EConstr
(*********************************************************************
Conventional default names *)
@@ -26,27 +28,27 @@ val default_dependent_ident : Id.t (* "x" *)
val lowercase_first_char : Id.t -> string
val sort_hdchar : sorts -> string
-val hdchar : env -> types -> string
-val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
-val named_hd : env -> types -> Name.t -> Name.t
-val head_name : types -> Id.t option
+val hdchar : env -> evar_map -> types -> string
+val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
+val named_hd : env -> evar_map -> types -> Name.t -> Name.t
+val head_name : evar_map -> types -> Id.t option
-val mkProd_name : env -> Name.t * types * types -> types
-val mkLambda_name : env -> Name.t * types * constr -> constr
+val mkProd_name : env -> evar_map -> Name.t * types * types -> types
+val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr
(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> Name.t * types * types -> types
-val lambda_name : env -> Name.t * types * constr -> constr
+val prod_name : env -> evar_map -> Name.t * types * types -> types
+val lambda_name : env -> evar_map -> Name.t * types * constr -> constr
-val prod_create : env -> types * types -> constr
-val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
-val name_context : env -> Context.Rel.t -> Context.Rel.t
+val prod_create : env -> evar_map -> types * types -> constr
+val lambda_create : env -> evar_map -> types * constr -> constr
+val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration
+val name_context : env -> evar_map -> rel_context -> rel_context
-val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
-val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
-val it_mkProd_or_LetIn_name : env -> types -> Context.Rel.t -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
+val mkProd_or_LetIn_name : env -> evar_map -> types -> rel_declaration -> types
+val mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_declaration -> constr
+val it_mkProd_or_LetIn_name : env -> evar_map -> types -> rel_context -> types
+val it_mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_context -> constr
(*********************************************************************
Fresh names *)
@@ -98,16 +100,16 @@ type renaming_flags =
| RenamingForGoal (** avoid all globals (as in intro) *)
| RenamingElsewhereFor of (Name.t list * constr)
-val make_all_name_different : env -> env
+val make_all_name_different : env -> evar_map -> env
val compute_displayed_name_in :
- renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+ evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
val compute_and_force_displayed_name_in :
- renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+ evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
val compute_displayed_let_name_in :
- renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+ evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
val rename_bound_vars_as_displayed :
- Id.t list -> Name.t list -> types -> types
+ evar_map -> Id.t list -> Name.t list -> types -> types
(**********************************************************************)
(* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 721389af4..9c264439b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -24,7 +24,7 @@ type proofview = Proofview_monad.proofview
(* The first items in pairs below are proofs (under construction).
The second items in the pairs below are statements that are being proved. *)
-type entry = (Term.constr * Term.types) list
+type entry = (EConstr.constr * EConstr.types) list
(** Returns a stylised view of a proofview for use by, for instance,
ide-s. *)
@@ -37,15 +37,16 @@ let proofview p =
p.comb , p.solution
let compact el ({ solution } as pv) =
- let nf = Evarutil.nf_evar solution in
+ let nf c = Evarutil.nf_evar solution c in
+ let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
let pruned_solution = Evd.drop_all_defined solution in
let apply_subst_einfo _ ei =
Evd.({ ei with
- evar_concl = nf ei.evar_concl;
- evar_hyps = Environ.map_named_val nf ei.evar_hyps;
- evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
+ evar_concl = nf0 ei.evar_concl;
+ evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+ evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -56,7 +57,7 @@ let compact el ({ solution } as pv) =
type telescope =
| TNil of Evd.evar_map
- | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+ | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
let typeclass_resolvable = Evd.Store.field ()
@@ -72,9 +73,9 @@ let dependent_init =
| TCons (env, sigma, typ, t) ->
let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+ let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in
let sigma = Sigma.to_evar_map sigma in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
- let (gl, _) = Term.destEvar econstr in
let entry = (econstr, typ) :: ret in
entry, { solution = sol; comb = gl :: comb; shelf = [] }
in
@@ -1010,7 +1011,7 @@ module Goal = struct
type ('a, 'r) t = {
env : Environ.env;
sigma : Evd.evar_map;
- concl : Term.constr ;
+ concl : EConstr.constr ;
self : Evar.t ; (* for compatibility with old-style definitions *)
}
@@ -1021,17 +1022,14 @@ module Goal = struct
let env { env=env } = env
let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
- let hyps { env=env } = Environ.named_context env
+ let hyps { env=env } = EConstr.named_context env
let concl { concl=concl } = concl
let extra { sigma=sigma; self=self } = goal_extra sigma self
- let raw_concl { concl=concl } = concl
-
-
let gmake_with info env sigma goal =
{ env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
sigma = sigma ;
- concl = Evd.evar_concl info ;
+ concl = EConstr.of_constr (Evd.evar_concl info);
self = goal }
let nf_gmake env sigma goal =
@@ -1244,12 +1242,12 @@ module V82 = struct
{ Evd.it = comb ; sigma = solution }
let top_goals initial { solution=solution; } =
- let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in
+ let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }
let top_evars initial =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evd.evars_of_term c)
+ Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
in
CList.flatten (CList.map evars_of_initial initial)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 294b03dca..a3b0304b1 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -14,6 +14,7 @@
open Util
open Term
+open EConstr
(** Main state of tactics *)
type proofview
@@ -43,7 +44,7 @@ val compact : entry -> proofview -> entry * proofview
empty [evar_map] (indeed a proof can be triggered by an incomplete
pretyping), [init] takes an additional argument to represent the
initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview
(** A [telescope] is a list of environment and conclusion like in
{!init}, except that each element may depend on the previous
@@ -52,7 +53,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
[evar_map] is threaded in state passing style. *)
type telescope =
| TNil of Evd.evar_map
- | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+ | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope)
(** Like {!init}, but goals are allowed to be dependent on one
another. Dependencies between goals is represented with the type
@@ -484,16 +485,12 @@ module Goal : sig
respectively the conclusion of [gl], the hypotheses of [gl], the
environment of [gl] (i.e. the global environment and the
hypotheses) and the current evar map. *)
- val concl : ([ `NF ], 'r) t -> Term.constr
- val hyps : ([ `NF ], 'r) t -> Context.Named.t
+ val concl : ('a, 'r) t -> constr
+ val hyps : ('a, 'r) t -> named_context
val env : ('a, 'r) t -> Environ.env
val sigma : ('a, 'r) t -> 'r Sigma.t
val extra : ('a, 'r) t -> Evd.Store.t
- (** Returns the goal's conclusion even if the goal is not
- normalised. *)
- val raw_concl : ('a, 'r) t -> Term.constr
-
type ('a, 'b) enter =
{ enter : 'r. ('a, 'r) t -> 'b }
diff --git a/engine/sigma.ml b/engine/sigma.ml
index 9381a33af..001f8be80 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -29,8 +29,8 @@ let here x s = Sigma (x, s, ())
type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-let new_evar sigma ?naming info =
- let (sigma, evk) = Evd.new_evar sigma ?naming info in
+let new_evar sigma ?name info =
+ let (sigma, evk) = Evd.new_evar sigma ?name info in
Fresh (evk, sigma, ())
let define evk c sigma =
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 7473a251b..8e8df02f2 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -61,7 +61,7 @@ val to_evar : 'r evar -> Evar.t
type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+val new_evar : 'r t -> ?name:Id.t ->
Evd.evar_info -> 'r fresh
val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
diff --git a/engine/termops.ml b/engine/termops.ml
index 2f4c5e204..64f4c6dc5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -97,11 +97,334 @@ let rec pr_constr c = match kind_of_term c with
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
-let term_printer = ref (fun _ -> pr_constr)
-let print_constr_env t = !term_printer t
-let print_constr t = !term_printer (Global.env()) t
+let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let print_constr_env env sigma t = !term_printer env sigma t
+let print_constr t = !term_printer (Global.env()) Evd.empty t
let set_print_constr f = term_printer := f
-let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c)
+
+module EvMap = Evar.Map
+
+let pr_evar_suggested_name evk sigma =
+ let open Evd in
+ let base_id evk' evi =
+ match evar_ident evk' sigma with
+ | Some id -> id
+ | None -> match evi.evar_source with
+ | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+ | _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+ | _ ->
+ let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+ Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
+ in
+ let names = EvMap.mapi base_id (undefined_map sigma) in
+ let id = EvMap.find evk names in
+ let fold evk' id' (seen, n) =
+ if seen then (seen, n)
+ else if Evar.equal evk evk' then (true, n)
+ else if Id.equal id id' then (seen, succ n)
+ else (seen, n)
+ in
+ let (_, n) = EvMap.fold fold names (false, 0) in
+ if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk =
+let open Evd in
+match evar_ident evk sigma with
+| None ->
+ str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+ str "?" ++ pr_id id
+
+let pr_instance_status (sc,typ) =
+ let open Evd in
+ begin match sc with
+ | IsSubType -> str " [or a subtype of it]"
+ | IsSuperType -> str " [or a supertype of it]"
+ | Conv -> mt ()
+ end ++
+ begin match typ with
+ | CoerceToType -> str " [up to coercion]"
+ | TypeNotProcessed -> mt ()
+ | TypeProcessed -> str " [type is checked]"
+ end
+
+let protect f x =
+ try f x
+ with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_kconstr a =
+ protect (fun c -> print_constr (EConstr.of_constr c)) a
+
+let pr_meta_map evd =
+ let open Evd in
+ let print_constr = print_kconstr in
+ let pr_name = function
+ Name id -> str"[" ++ pr_id id ++ str"]"
+ | _ -> mt() in
+ let pr_meta_binding = function
+ | (mv,Cltyp (na,b)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " : " ++
+ print_constr b.rebus ++ fnl ())
+ | (mv,Clval(na,(b,s),t)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " := " ++
+ print_constr b.rebus ++
+ str " : " ++ print_constr t.rebus ++
+ spc () ++ pr_instance_status s ++ fnl ())
+ in
+ prlist pr_meta_binding (meta_list evd)
+
+let pr_decl (decl,ok) =
+ let open NamedDecl in
+ let print_constr = print_kconstr in
+ match decl with
+ | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+ | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+ print_constr c ++ str (if ok then ")" else "}")
+
+let pr_evar_source = function
+ | Evar_kinds.NamedHole id -> pr_id id
+ | Evar_kinds.QuestionMark _ -> str "underscore"
+ | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
+ | Evar_kinds.CasesType true ->
+ str "subterm of pattern-matching return predicate"
+ | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
+ | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+ | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
+ let open Globnames in
+ let print_constr = print_kconstr in
+ let id = Option.get ido in
+ str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
+ spc () ++ print_constr (printable_constr_of_global c)
+ | Evar_kinds.InternalHole -> str "internal placeholder"
+ | Evar_kinds.TomatchTypeParameter (ind,n) ->
+ let print_constr = print_kconstr in
+ pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+ | Evar_kinds.GoalEvar -> str "goal evar"
+ | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
+ | Evar_kinds.MatchingVar _ -> str "matching variable"
+ | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
+ | Evar_kinds.SubEvar evk ->
+ let open Evd in
+ str "subterm of " ++ str (string_of_existential evk)
+
+let pr_evar_info evi =
+ let open Evd in
+ let print_constr = print_kconstr in
+ let phyps =
+ try
+ let decls = match Filter.repr (evar_filter evi) with
+ | None -> List.map (fun c -> (c, true)) (evar_context evi)
+ | Some filter -> List.combine (evar_context evi) filter
+ in
+ prlist_with_sep spc pr_decl (List.rev decls)
+ with Invalid_argument _ -> str "Ill-formed filtered context" in
+ let pty = print_constr evi.evar_concl in
+ let pb =
+ match evi.evar_body with
+ | Evar_empty -> mt ()
+ | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ in
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "{" ++
+ prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+ | _ ->
+ mt ()
+ in
+ let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+ hov 2
+ (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
+ candidates ++ spc() ++ src)
+
+let compute_evar_dependency_graph sigma =
+ let open Evd in
+ (* Compute the map binding ev to the evars whose body depends on ev *)
+ let fold evk evi acc =
+ let fold_ev evk' acc =
+ let tab =
+ try EvMap.find evk' acc
+ with Not_found -> Evar.Set.empty
+ in
+ EvMap.add evk' (Evar.Set.add evk tab) acc
+ in
+ match evar_body evi with
+ | Evar_empty -> acc
+ | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+ in
+ Evd.fold fold sigma EvMap.empty
+
+let evar_dependency_closure n sigma =
+ let open Evd in
+ (** Create the DAG of depth [n] representing the recursive dependencies of
+ undefined evars. *)
+ let graph = compute_evar_dependency_graph sigma in
+ let rec aux n curr accu =
+ if Int.equal n 0 then Evar.Set.union curr accu
+ else
+ let fold evk accu =
+ try
+ let deps = EvMap.find evk graph in
+ Evar.Set.union deps accu
+ with Not_found -> accu
+ in
+ (** Consider only the newly added evars *)
+ let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
+ (** Merge the others *)
+ let accu = Evar.Set.union curr accu in
+ aux (n - 1) ncurr accu
+ in
+ let undef = EvMap.domain (undefined_map sigma) in
+ aux n undef Evar.Set.empty
+
+let evar_dependency_closure n sigma =
+ let open Evd in
+ let deps = evar_dependency_closure n sigma in
+ let map = EvMap.bind (fun ev -> find sigma ev) deps in
+ EvMap.bindings map
+
+let has_no_evar sigma =
+ try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true
+ with Exit -> false
+
+let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+
+let pr_evar_universe_context ctx =
+ let open UState in
+ let open Evd in
+ let prl = pr_uctx_level ctx in
+ if UState.is_empty ctx then mt ()
+ else
+ (str"UNIVERSES:"++brk(0,1)++
+ h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
+ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
+ str"UNDEFINED UNIVERSES:"++brk(0,1)++
+ h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
+
+let print_env_short env =
+ let print_constr = print_kconstr in
+ let pr_rel_decl = function
+ | RelDecl.LocalAssum (n,_) -> pr_name n
+ | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+ in
+ let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
+ let nc = List.rev (named_context env) in
+ let rc = List.rev (rel_context env) in
+ str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
+ str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
+
+let pr_evar_constraints sigma pbs =
+ let pr_evconstr (pbty, env, t1, t2) =
+ let env =
+ (** We currently allow evar instances to refer to anonymous de
+ Bruijn indices, so we protect the error printing code in this
+ case by giving names to every de Bruijn variable in the
+ rel_context of the conversion problem. MS: we should rather
+ stop depending on anonymous variables, they can be used to
+ indicate independency. Also, this depends on a strategy for
+ naming/renaming. *)
+ Namegen.make_all_name_different env sigma
+ in
+ print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+ print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+ in
+ prlist_with_sep fnl pr_evconstr pbs
+
+let pr_evar_map_gen with_univs pr_evars sigma =
+ let uvs = Evd.evar_universe_context sigma in
+ let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in
+ let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
+ and svs = if with_univs then pr_evar_universe_context uvs else mt ()
+ and cstrs =
+ if List.is_empty conv_pbs then mt ()
+ else
+ str "CONSTRAINTS:" ++ brk (0, 1) ++
+ pr_evar_constraints sigma conv_pbs ++ fnl ()
+ and metas =
+ if List.is_empty (Evd.meta_list sigma) then mt ()
+ else
+ str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
+ in
+ evs ++ svs ++ cstrs ++ metas
+
+let pr_evar_list sigma l =
+ let open Evd in
+ let pr (ev, evi) =
+ h 0 (str (string_of_existential ev) ++
+ str "==" ++ pr_evar_info evi ++
+ (if evi.evar_body == Evar_empty
+ then str " {" ++ pr_existential_key sigma ev ++ str "}"
+ else mt ()))
+ in
+ h 0 (prlist_with_sep fnl pr l)
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
+ (* Print all evars *)
+ let to_list d =
+ let open Evd in
+ (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+ let l = ref [] in
+ let fold_def evk evi () = match evi.evar_body with
+ | Evar_defined _ -> l := (evk, evi) :: !l
+ | Evar_empty -> ()
+ in
+ let fold_undef evk evi () = match evi.evar_body with
+ | Evar_empty -> l := (evk, evi) :: !l
+ | Evar_defined _ -> ()
+ in
+ Evd.fold fold_def d ();
+ Evd.fold fold_undef d ();
+ !l
+ in
+ str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
+| Some n ->
+ (* Print all evars *)
+ str"UNDEFINED EVARS:"++
+ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
+ brk(0,1)++
+ pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+
+let pr_evar_by_filter filter sigma =
+ let open Evd in
+ let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in
+ let elts = List.rev elts in
+ let is_def (_, evi) = match evi.evar_body with
+ | Evar_defined _ -> true
+ | Evar_empty -> false
+ in
+ let (defined, undefined) = List.partition is_def elts in
+ let filter (evk, evi) = filter evk evi in
+ let defined = List.filter filter defined in
+ let undefined = List.filter filter undefined in
+ let prdef =
+ if List.is_empty defined then mt ()
+ else str "DEFINED EVARS:" ++ brk (0, 1) ++
+ pr_evar_list sigma defined
+ in
+ let prundef =
+ if List.is_empty undefined then mt ()
+ else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
+ pr_evar_list sigma undefined
+ in
+ prdef ++ prundef
+
+let pr_evar_map ?(with_univs=true) depth sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
+
+let pr_evar_map_filter ?(with_univs=true) filter sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
+
+let pr_metaset metas =
+ str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]"
let pr_var_decl env decl =
let open NamedDecl in
@@ -109,9 +432,10 @@ let pr_var_decl env decl =
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
- let pb = print_constr_env env c in
+ let c = EConstr.of_constr c in
+ let pb = print_constr_env env Evd.empty c in
(str" := " ++ pb ++ cut () ) in
- let pt = print_constr_env env (get_type decl) in
+ let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
let ptyp = (str" : " ++ pt) in
(pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
@@ -121,9 +445,10 @@ let pr_rel_decl env decl =
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
- let pb = print_constr_env env c in
+ let c = EConstr.of_constr c in
+ let pb = print_constr_env env Evd.empty c in
(str":=" ++ spc () ++ pb ++ spc ()) in
- let ptyp = print_constr_env env (get_type decl) in
+ let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
match get_name decl with
| Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
| Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -159,6 +484,7 @@ let print_env env =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
let rel_list n m =
+ let open EConstr in
let rec reln l p =
if p>m then l else reln (mkRel(n+p)::l) (p+1)
in
@@ -166,6 +492,7 @@ let rel_list n m =
let push_rel_assum (x,t) env =
let open RelDecl in
+ let open EConstr in
push_rel (LocalAssum (x,t)) env
let push_rels_assum assums =
@@ -199,21 +526,17 @@ let lookup_rel_id id sign =
lookrec 1 sign
(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn decl c =
- let open RelDecl in
- match decl with
- | LocalAssum (na,t) -> mkProd (na, t, c)
- | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
-
+let mkProd_or_LetIn = EConstr.mkProd_or_LetIn
(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
let mkProd_wo_LetIn decl c =
+ let open EConstr in
let open RelDecl in
match decl with
| LocalAssum (na,t) -> mkProd (na, t, c)
- | LocalDef (_,b,_) -> subst1 b c
+ | LocalDef (_,b,_) -> Vars.subst1 b c
-let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
-let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+let it_mkProd init = List.fold_left (fun c (n,t) -> EConstr.mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t) -> EConstr.mkLambda (n, t, c)) init
let it_named_context_quantifier f ~init =
List.fold_left (fun c d -> f d c) init
@@ -221,9 +544,9 @@ let it_named_context_quantifier f ~init =
let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
-let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier EConstr.mkNamedProd_or_LetIn ~init
let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
-let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier EConstr.mkNamedLambda_or_LetIn ~init
let it_mkLambda_or_LetIn_from_no_LetIn c decls =
let open RelDecl in
@@ -236,37 +559,39 @@ let it_mkLambda_or_LetIn_from_no_LetIn c decls =
(* *)
(* strips head casts and flattens head applications *)
-let rec strip_head_cast c = match kind_of_term c with
+let rec strip_head_cast sigma c = match EConstr.kind sigma c with
| App (f,cl) ->
- let rec collapse_rec f cl2 = match kind_of_term f with
+ let rec collapse_rec f cl2 = match EConstr.kind sigma f with
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
| Cast (c,_,_) -> collapse_rec c cl2
- | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2)
+ | _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
in
collapse_rec f cl
- | Cast (c,_,_) -> strip_head_cast c
+ | Cast (c,_,_) -> strip_head_cast sigma c
| _ -> c
-let rec drop_extra_implicit_args c = match kind_of_term c with
+let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
(* Removed trailing extra implicit arguments, what improves compatibility
for constants with recently added maximal implicit arguments *)
- | App (f,args) when isEvar (Array.last args) ->
- drop_extra_implicit_args
+ | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
+ let open EConstr in
+ drop_extra_implicit_args sigma
(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
| _ -> c
(* Get the last arg of an application *)
-let last_arg c = match kind_of_term c with
+let last_arg sigma c = match EConstr.kind sigma c with
| App (f,cl) -> Array.last cl
| _ -> anomaly (Pp.str "last_arg")
(* Get the last arg of an application *)
-let decompose_app_vect c =
- match kind_of_term c with
+let decompose_app_vect sigma c =
+ match EConstr.kind sigma c with
| App (f,cl) -> (f, cl)
| _ -> (c,[||])
let adjust_app_list_size f1 l1 f2 l2 =
+ let open EConstr in
let len1 = List.length l1 and len2 = List.length l2 in
if Int.equal len1 len2 then (f1,l1,f2,l2)
else if len1 < len2 then
@@ -277,14 +602,15 @@ let adjust_app_list_size f1 l1 f2 l2 =
(applist (f1,extras), restl1, f2, l2)
let adjust_app_array_size f1 l1 f2 l2 =
+ let open EConstr in
let len1 = Array.length l1 and len2 = Array.length l2 in
if Int.equal len1 len2 then (f1,l1,f2,l2)
else if len1 < len2 then
let extras,restl2 = Array.chop (len2-len1) l2 in
- (f1, l1, appvect (f2,extras), restl2)
+ (f1, l1, mkApp (f2,extras), restl2)
else
let extras,restl1 = Array.chop (len1-len2) l1 in
- (appvect (f1,extras), restl1, f2, l2)
+ (mkApp (f1,extras), restl1, f2, l2)
(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
subterms of [c]; it carries an extra data [l] (typically a name
@@ -321,6 +647,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
(co-)fixpoint) *)
let fold_rec_types g (lna,typarray,_) e =
+ let open EConstr in
+ let open Vars in
let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
Array.fold_left (fun e assum -> g assum e) e ctxt
@@ -336,9 +664,10 @@ let map_left2 f a g b =
r, s
end
-let map_constr_with_binders_left_to_right g f l c =
+let map_constr_with_binders_left_to_right sigma g f l c =
let open RelDecl in
- match kind_of_term c with
+ let open EConstr in
+ match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c
| Cast (b,k,t) ->
@@ -400,9 +729,10 @@ let map_constr_with_binders_left_to_right g f l c =
else mkCoFix (ln,(lna,tl',bl'))
(* strong *)
-let map_constr_with_full_binders g f l cstr =
+let map_constr_with_full_binders sigma g f l cstr =
+ let open EConstr in
let open RelDecl in
- match kind_of_term cstr with
+ match EConstr.kind sigma cstr with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> cstr
| Cast (c,k, t) ->
@@ -411,16 +741,16 @@ let map_constr_with_full_binders g f l cstr =
if c==c' && t==t' then cstr else mkCast (c', k, t')
| Prod (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na,t)) l) c in
+ let c' = f (g (LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkProd (na, t', c')
| Lambda (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na,t)) l) c in
+ let c' = f (g (LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkLambda (na, t', c')
| LetIn (na,b,t,c) ->
let b' = f l b in
let t' = f l t in
- let c' = f (g (LocalDef (na,b,t)) l) c in
+ let c' = f (g (LocalDef (na, b, t)) l) c in
if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
| App (c,al) ->
let c' = f l c in
@@ -441,7 +771,7 @@ let map_constr_with_full_binders g f l cstr =
| Fix (ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
@@ -449,7 +779,7 @@ let map_constr_with_full_binders g f l cstr =
| CoFix(ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
@@ -462,30 +792,31 @@ let map_constr_with_full_binders g f l cstr =
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive *)
-let fold_constr_with_full_binders g f n acc c =
+let fold_constr_with_full_binders sigma g f n acc c =
let open RelDecl in
- match kind_of_term c with
+ let inj c = EConstr.Unsafe.to_constr c in
+ match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> acc
| Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-let fold_constr_with_binders g f n acc c =
- fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+let fold_constr_with_binders sigma g f n acc c =
+ fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c
(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
subterms of [c]; it carries an extra data [acc] which is processed by [g] at
@@ -520,29 +851,29 @@ let iter_constr_with_full_binders g f l c =
exception Occur
-let occur_meta c =
- let rec occrec c = match kind_of_term c with
+let occur_meta sigma c =
+ let rec occrec c = match EConstr.kind sigma c with
| Meta _ -> raise Occur
- | _ -> iter_constr occrec c
+ | _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
-let occur_existential c =
- let rec occrec c = match kind_of_term c with
+let occur_existential sigma c =
+ let rec occrec c = match EConstr.kind sigma c with
| Evar _ -> raise Occur
- | _ -> iter_constr occrec c
+ | _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
-let occur_meta_or_existential c =
- let rec occrec c = match kind_of_term c with
+let occur_meta_or_existential sigma c =
+ let rec occrec c = match EConstr.kind sigma c with
| Evar _ -> raise Occur
| Meta _ -> raise Occur
- | _ -> iter_constr occrec c
+ | _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
-let occur_evar n c =
- let rec occur_rec c = match kind_of_term c with
+let occur_evar sigma n c =
+ let rec occur_rec c = match EConstr.kind sigma c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
- | _ -> iter_constr occur_rec c
+ | _ -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -550,55 +881,55 @@ let occur_in_global env id constr =
let vars = vars_of_global env constr in
if Id.Set.mem id vars then raise Occur
-let occur_var env id c =
+let occur_var env sigma id c =
let rec occur_rec c =
- match kind_of_term c with
- | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c
- | _ -> iter_constr occur_rec c
+ match EConstr.kind sigma c with
+ | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
+ | _ -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
-let occur_var_in_decl env hyp decl =
+let occur_var_in_decl env sigma hyp decl =
let open NamedDecl in
match decl with
- | LocalAssum (_,typ) -> occur_var env hyp typ
+ | LocalAssum (_,typ) -> occur_var env sigma hyp typ
| LocalDef (_, body, typ) ->
- occur_var env hyp typ ||
- occur_var env hyp body
+ occur_var env sigma hyp typ ||
+ occur_var env sigma hyp body
-let local_occur_var id c =
- let rec occur c = match kind_of_term c with
+let local_occur_var sigma id c =
+ let rec occur c = match EConstr.kind sigma c with
| Var id' -> if Id.equal id id' then raise Occur
- | _ -> Constr.iter occur c
+ | _ -> EConstr.iter sigma occur c
in
try occur c; false with Occur -> true
(* returns the list of free debruijn indices in a term *)
-let free_rels m =
- let rec frec depth acc c = match kind_of_term c with
+let free_rels sigma m =
+ let rec frec depth acc c = match EConstr.kind sigma c with
| Rel n -> if n >= depth then Int.Set.add (n-depth+1) acc else acc
- | _ -> fold_constr_with_binders succ frec depth acc c
+ | _ -> fold_constr_with_binders sigma succ frec depth acc c
in
frec 1 Int.Set.empty m
(* collects all metavar occurrences, in left-to-right order, preserving
* repetitions and all. *)
-let collect_metas c =
+let collect_metas sigma c =
let rec collrec acc c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Meta mv -> List.add_set Int.equal mv acc
- | _ -> fold_constr collrec acc c
+ | _ -> EConstr.fold sigma collrec acc c
in
List.rev (collrec [] c)
(* collects all vars; warning: this is only visible vars, not dependencies in
all section variables; for the latter, use global_vars_set *)
-let collect_vars c =
- let rec aux vars c = match kind_of_term c with
+let collect_vars sigma c =
+ let rec aux vars c = match EConstr.kind sigma c with
| Var id -> Id.Set.add id vars
- | _ -> fold_constr aux vars c in
+ | _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
let vars_of_global_reference env gr =
@@ -608,54 +939,56 @@ let vars_of_global_reference env gr =
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
-let dependent_main noevar univs m t =
+let dependent_main noevar univs sigma m t =
+ let open EConstr in
let eqc x y =
- if univs then not (Option.is_empty (Universes.eq_constr_universes x y))
- else eq_constr_nounivs x y
+ if univs then not (Option.is_empty (eq_constr_universes sigma x y))
+ else eq_constr_nounivs sigma x y
in
let rec deprec m t =
if eqc m t then
raise Occur
else
- match kind_of_term m, kind_of_term t with
+ match EConstr.kind sigma m, EConstr.kind sigma t with
| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
CArray.Fun1.iter deprec m
(Array.sub lt
(Array.length lm) ((Array.length lt) - (Array.length lm)))
- | _, Cast (c,_,_) when noevar && isMeta c -> ()
+ | _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
| _, Evar _ when noevar -> ()
- | _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t
+ | _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
in
try deprec m t; false with Occur -> true
-let dependent = dependent_main false false
-let dependent_no_evar = dependent_main true false
+let dependent sigma c t = dependent_main false false sigma c t
+let dependent_no_evar sigma c t = dependent_main true false sigma c t
-let dependent_univs = dependent_main false true
-let dependent_univs_no_evar = dependent_main true true
+let dependent_univs sigma c t = dependent_main false true sigma c t
+let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
-let dependent_in_decl a decl =
+let dependent_in_decl sigma a decl =
let open NamedDecl in
match decl with
- | LocalAssum (_,t) -> dependent a t
- | LocalDef (_, body, t) -> dependent a body || dependent a t
+ | LocalAssum (_,t) -> dependent sigma a t
+ | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t
-let count_occurrences m t =
+let count_occurrences sigma m t =
+ let open EConstr in
let n = ref 0 in
let rec countrec m t =
- if eq_constr m t then
+ if EConstr.eq_constr sigma m t then
incr n
else
- match kind_of_term m, kind_of_term t with
+ match EConstr.kind sigma m, EConstr.kind sigma t with
| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
Array.iter (countrec m)
(Array.sub lt
(Array.length lm) ((Array.length lt) - (Array.length lm)))
- | _, Cast (c,_,_) when isMeta c -> ()
+ | _, Cast (c,_,_) when isMeta sigma c -> ()
| _, Evar _ -> ()
- | _ -> iter_constr_with_binders (lift 1) countrec m t
+ | _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
in
countrec m t;
!n
@@ -663,7 +996,7 @@ let count_occurrences m t =
(* Synonymous *)
let occur_term = dependent
-let pop t = lift (-1) t
+let pop t = EConstr.Vars.lift (-1) t
(***************************)
(* bindings functions *)
@@ -673,50 +1006,55 @@ type meta_type_map = (metavariable * types) list
type meta_value_map = (metavariable * constr) list
+let isMetaOf sigma mv c =
+ match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false
+
let rec subst_meta bl c =
match kind_of_term c with
| Meta i -> (try Int.List.assoc i bl with Not_found -> c)
| _ -> map_constr (subst_meta bl) c
-let rec strip_outer_cast c = match kind_of_term c with
- | Cast (c,_,_) -> strip_outer_cast c
+let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
+ | Cast (c,_,_) -> strip_outer_cast sigma c
| _ -> c
(* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
+let collapse_appl sigma c = match EConstr.kind sigma c with
| App (f,cl) ->
let rec collapse_rec f cl2 =
- match kind_of_term (strip_outer_cast f) with
+ match EConstr.kind sigma (strip_outer_cast sigma f) with
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
- | _ -> mkApp (f,cl2)
+ | _ -> EConstr.mkApp (f,cl2)
in
collapse_rec f cl
| _ -> c
(* First utilities for avoiding telescope computation for subst_term *)
-let prefix_application eq_fun (k,c) (t : constr) =
- let c' = collapse_appl c and t' = collapse_appl t in
- match kind_of_term c', kind_of_term t' with
+let prefix_application sigma eq_fun (k,c) t =
+ let open EConstr in
+ let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
+ match EConstr.kind sigma c', EConstr.kind sigma t' with
| App (f1,cl1), App (f2,cl2) ->
let l1 = Array.length cl1
and l2 = Array.length cl2 in
if l1 <= l2
- && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
else
None
| _ -> None
-let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
- let c' = collapse_appl c and t' = collapse_appl t in
- match kind_of_term c', kind_of_term t' with
+let my_prefix_application sigma eq_fun (k,c) by_c t =
+ let open EConstr in
+ let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
+ match EConstr.kind sigma c', EConstr.kind sigma t' with
| App (f1,cl1), App (f2,cl2) ->
let l1 = Array.length cl1
and l2 = Array.length cl2 in
if l1 <= l2
- && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
- Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+ && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
else
None
| _ -> None
@@ -725,35 +1063,37 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
works if [c] has rels *)
-let subst_term_gen eq_fun c t =
+let subst_term_gen sigma eq_fun c t =
+ let open EConstr in
+ let open Vars in
let rec substrec (k,c as kc) t =
- match prefix_application eq_fun kc t with
+ match prefix_application sigma eq_fun kc t with
| Some x -> x
| None ->
- if eq_fun c t then mkRel k
+ if eq_fun sigma c t then mkRel k
else
- map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+ EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
in
substrec (1,c) t
-let subst_term = subst_term_gen eq_constr
+let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t
(* Recognizing occurrences of a given subterm in a term :
[replace_term c1 c2 t] substitutes [c2] for all occurrences of
term [c1] in a term [t]; works if [c1] and [c2] have rels *)
-let replace_term_gen eq_fun c by_c in_t =
+let replace_term_gen sigma eq_fun c by_c in_t =
let rec substrec (k,c as kc) t =
- match my_prefix_application eq_fun kc by_c t with
+ match my_prefix_application sigma eq_fun kc by_c t with
| Some x -> x
| None ->
- (if eq_fun c t then (lift k by_c) else
- map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
+ (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else
+ EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
substrec kc t)
in
substrec (0,c) in_t
-let replace_term = replace_term_gen eq_constr
+let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
let vars_of_env env =
let s =
@@ -804,15 +1144,37 @@ let is_section_variable id =
try let _ = Global.lookup_named id in true
with Not_found -> false
-let isGlobalRef c =
- match kind_of_term c with
+let global_of_constr sigma c =
+ let open Globnames in
+ match EConstr.kind sigma c with
+ | Const (c, u) -> ConstRef c, u
+ | Ind (i, u) -> IndRef i, u
+ | Construct (c, u) -> ConstructRef c, u
+ | Var id -> VarRef id, EConstr.EInstance.empty
+ | _ -> raise Not_found
+
+let is_global sigma c t =
+ let open Globnames in
+ match c, EConstr.kind sigma t with
+ | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | IndRef i, Ind (i', _) -> eq_ind i i'
+ | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | VarRef id, Var id' -> Id.equal id id'
+ | _ -> false
+
+let isGlobalRef sigma c =
+ match EConstr.kind sigma c with
| Const _ | Ind _ | Construct _ | Var _ -> true
| _ -> false
-let is_template_polymorphic env f =
- match kind_of_term f with
- | Ind ind -> Environ.template_polymorphic_pind ind env
- | Const c -> Environ.template_polymorphic_pconstant c env
+let is_template_polymorphic env sigma f =
+ match EConstr.kind sigma f with
+ | Ind (ind, u) ->
+ if not (EConstr.EInstance.is_empty u) then false
+ else Environ.template_polymorphic_ind ind env
+ | Const (cst, u) ->
+ if not (EConstr.EInstance.is_empty u) then false
+ else Environ.template_polymorphic_constant cst env
| _ -> false
let base_sort_cmp pb s0 s1 =
@@ -822,21 +1184,33 @@ let base_sort_cmp pb s0 s1 =
| (Type u1, Type u2) -> true
| _ -> false
+let rec is_Prop sigma c = match EConstr.kind sigma c with
+ | Sort u ->
+ begin match EConstr.ESorts.kind sigma u with
+ | Prop Null -> true
+ | _ -> false
+ end
+ | Cast (c,_,_) -> is_Prop sigma c
+ | _ -> false
+
(* eq_constr extended with universe erasure *)
-let compare_constr_univ f cv_pb t1 t2 =
- match kind_of_term t1, kind_of_term t2 with
- Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+let compare_constr_univ sigma f cv_pb t1 t2 =
+ let open EConstr in
+ match EConstr.kind sigma t1, EConstr.kind sigma t2 with
+ Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
| Prod (_,t1,c1), Prod (_,t2,c2) ->
f Reduction.CONV t1 t2 && f cv_pb c1 c2
- | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
+ | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
-let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
+let constr_cmp sigma cv_pb t1 t2 =
+ let rec compare cv_pb t1 t2 = compare_constr_univ sigma compare cv_pb t1 t2 in
+ compare cv_pb t1 t2
-let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
+let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2
(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
App(c,[||]) -> ([],c) *)
-let split_app c = match kind_of_term c with
+let split_app sigma c = match EConstr.kind sigma c with
App(c,l) ->
let len = Array.length l in
if Int.equal len 0 then ([],c) else
@@ -845,28 +1219,30 @@ let split_app c = match kind_of_term c with
c::(Array.to_list prev), last
| _ -> assert false
-type subst = (Context.Rel.t * constr) Evar.Map.t
+type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t
exception CannotFilter
-let filtering env cv_pb c1 c2 =
+let filtering sigma env cv_pb c1 c2 =
+ let open EConstr in
+ let open Vars in
let evm = ref Evar.Map.empty in
let define cv_pb e1 ev c1 =
try let (e2,c2) = Evar.Map.find ev !evm in
let shift = List.length e1 - List.length e2 in
- if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+ if constr_cmp sigma cv_pb c1 (lift shift c2) then () else raise CannotFilter
with Not_found ->
evm := Evar.Map.add ev (e1,c1) !evm
in
let rec aux env cv_pb c1 c2 =
- match kind_of_term c1, kind_of_term c2 with
+ match EConstr.kind sigma c1, EConstr.kind sigma c2 with
| App _, App _ ->
- let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+ let ((p1,l1),(p2,l2)) = (split_app sigma c1),(split_app sigma c2) in
let () = aux env cv_pb l1 l2 in
begin match p1, p2 with
| [], [] -> ()
| (h1 :: p1), (h2 :: p2) ->
- aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+ aux env cv_pb (applist (h1, p1)) (applist (h2, p2))
| _ -> assert false
end
| Prod (n,t1,c1), Prod (_,t2,c2) ->
@@ -875,52 +1251,52 @@ let filtering env cv_pb c1 c2 =
| _, Evar (ev,_) -> define cv_pb env ev c1
| Evar (ev,_), _ -> define cv_pb env ev c2
| _ ->
- if compare_constr_univ
+ if compare_constr_univ sigma
(fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
else raise CannotFilter
(* TODO: le reste des binders *)
in
aux env cv_pb c1 c2; !evm
-let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
- let rec prodec_rec i l c = match kind_of_term c with
+let decompose_prod_letin sigma c =
+ let rec prodec_rec i l c = match EConstr.kind sigma c with
| Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
| LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
| Cast (c,_,_) -> prodec_rec i l c
| _ -> i,l,c in
- prodec_rec 0 []
+ prodec_rec 0 [] c
(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
* gives n (casts are ignored) *)
-let nb_lam =
- let rec nbrec n c = match kind_of_term c with
+let nb_lam sigma c =
+ let rec nbrec n c = match EConstr.kind sigma c with
| Lambda (_,_,c) -> nbrec (n+1) c
| Cast (c,_,_) -> nbrec n c
| _ -> n
in
- nbrec 0
+ nbrec 0 c
(* similar to nb_lam, but gives the number of products instead *)
-let nb_prod =
- let rec nbrec n c = match kind_of_term c with
+let nb_prod sigma c =
+ let rec nbrec n c = match EConstr.kind sigma c with
| Prod (_,_,c) -> nbrec (n+1) c
| Cast (c,_,_) -> nbrec n c
| _ -> n
in
- nbrec 0
+ nbrec 0 c
-let nb_prod_modulo_zeta x =
+let nb_prod_modulo_zeta sigma x =
let rec count n c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
Prod(_,_,t) -> count (n+1) t
- | LetIn(_,a,_,t) -> count n (subst1 a t)
+ | LetIn(_,a,_,t) -> count n (EConstr.Vars.subst1 a t)
| Cast(c,_,_) -> count n c
| _ -> n
in count 0 x
-let align_prod_letin c a : Context.Rel.t * constr =
- let (lc,_,_) = decompose_prod_letin c in
- let (la,l,a) = decompose_prod_letin a in
+let align_prod_letin sigma c a =
+ let (lc,_,_) = decompose_prod_letin sigma c in
+ let (la,l,a) = decompose_prod_letin sigma a in
if not (la >= lc) then invalid_arg "align_prod_letin";
let (l1,l2) = Util.List.chop lc l in
l2,it_mkProd_or_LetIn a l1
@@ -929,21 +1305,23 @@ let align_prod_letin c a : Context.Rel.t * constr =
(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
(* Remplace 2 earlier buggish versions *)
-let rec eta_reduce_head c =
- match kind_of_term c with
+let rec eta_reduce_head sigma c =
+ let open EConstr in
+ let open Vars in
+ match EConstr.kind sigma c with
| Lambda (_,c1,c') ->
- (match kind_of_term (eta_reduce_head c') with
+ (match EConstr.kind sigma (eta_reduce_head sigma c') with
| App (f,cl) ->
let lastn = (Array.length cl) - 1 in
if lastn < 0 then anomaly (Pp.str "application without arguments")
else
- (match kind_of_term cl.(lastn) with
+ (match EConstr.kind sigma cl.(lastn) with
| Rel 1 ->
let c' =
if Int.equal lastn 0 then f
else mkApp (f, Array.sub cl 0 lastn)
in
- if noccurn 1 c'
+ if noccurn sigma 1 c'
then lift (-1) c'
else c
| _ -> c)
@@ -954,7 +1332,7 @@ let rec eta_reduce_head c =
(* iterator on rel context *)
let process_rel_context f env =
let sign = named_context_val env in
- let rels = rel_context env in
+ let rels = EConstr.rel_context env in
let env0 = reset_with_named_context sign env in
Context.Rel.fold_outside f rels ~init:env0
@@ -1002,6 +1380,14 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
let mem_named_context_val id ctxt =
try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
+let map_rel_decl f = function
+| RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
+| RelDecl.LocalDef (id, b, t) -> RelDecl.LocalDef (id, f b, f t)
+
+let map_named_decl f = function
+| NamedDecl.LocalAssum (id, t) -> NamedDecl.LocalAssum (id, f t)
+| NamedDecl.LocalDef (id, b, t) -> NamedDecl.LocalDef (id, f b, f t)
+
let compact_named_context sign =
let compact l decl =
match decl, l with
@@ -1031,28 +1417,59 @@ let clear_named_body id env =
| d -> push_named d in
fold_named_context aux env ~init:(reset_context env)
-let global_vars env ids = Id.Set.elements (global_vars_set env ids)
+let global_vars_set env sigma constr =
+ let rec filtrec acc c =
+ let acc = match EConstr.kind sigma c with
+ | Var _ | Const _ | Ind _ | Construct _ ->
+ Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
+ | _ -> acc
+ in
+ EConstr.fold sigma filtrec acc c
+ in
+ filtrec Id.Set.empty constr
+
+let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids)
-let global_vars_set_of_decl env = function
- | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+let global_vars_set_of_decl env sigma = function
+ | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma t
| NamedDecl.LocalDef (_,c,t) ->
- Id.Set.union (global_vars_set env t)
- (global_vars_set env c)
+ Id.Set.union (global_vars_set env sigma t)
+ (global_vars_set env sigma c)
-let dependency_closure env sign hyps =
+let dependency_closure env sigma sign hyps =
if Id.Set.is_empty hyps then [] else
let (_,lh) =
Context.Named.fold_inside
(fun (hs,hl) d ->
let x = NamedDecl.get_id d in
if Id.Set.mem x hs then
- (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
+ (Id.Set.union (global_vars_set_of_decl env sigma d) (Id.Set.remove x hs),
x::hl)
else (hs,hl))
~init:(hyps,[])
sign in
List.rev lh
+let global_app_of_constr sigma c =
+ let open Univ in
+ let open Globnames in
+ match EConstr.kind sigma c with
+ | Const (c, u) -> (ConstRef c, u), None
+ | Ind (i, u) -> (IndRef i, u), None
+ | Construct (c, u) -> (ConstructRef c, u), None
+ | Var id -> (VarRef id, EConstr.EInstance.empty), None
+ | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c
+ | _ -> raise Not_found
+
+let prod_applist sigma c l =
+ let open EConstr in
+ let rec app subst c l =
+ match EConstr.kind sigma c, l with
+ | Prod(_,_,c), arg::l -> app (arg::subst) c l
+ | _, [] -> Vars.substl subst c
+ | _ -> anomaly (Pp.str "Not enough prod's") in
+ app [] c l
+
(* Combinators on judgments *)
let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
@@ -1071,6 +1488,7 @@ let context_chop k ctx =
(* Do not skip let-in's *)
let env_rel_context_chop k env =
+ let open EConstr in
let rels = rel_context env in
let ctx1,ctx2 = List.chop k rels in
push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
@@ -1084,6 +1502,7 @@ let impossible_default_case = ref None
let set_impossible_default_clause c = impossible_default_case := Some c
let coq_unit_judge =
+ let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
let na1 = Name (Id.of_string "A") in
let na2 = Name (Id.of_string "H") in
fun () ->
diff --git a/engine/termops.mli b/engine/termops.mli
index 78826f79a..fe6dfb0ce 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -13,63 +13,54 @@ open Pp
open Names
open Term
open Environ
+open EConstr
(** printers *)
val print_sort : sorts -> std_ppcmds
val pr_sort_family : sorts_family -> std_ppcmds
-val pr_fix : (constr -> std_ppcmds) -> fixpoint -> std_ppcmds
-
-(** debug printer: do not use to display terms to the casual user... *)
-val set_print_constr : (env -> constr -> std_ppcmds) -> unit
-val print_constr : constr -> std_ppcmds
-val print_constr_env : env -> constr -> std_ppcmds
-val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
-val print_rel_context : env -> std_ppcmds
-val print_env : env -> std_ppcmds
+val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
(** about contexts *)
val push_rel_assum : Name.t * types -> env -> env
-val push_rels_assum : (Name.t * types) list -> env -> env
-val push_named_rec_types : Name.t array * types array * 'a -> env -> env
+val push_rels_assum : (Name.t * Constr.types) list -> env -> env
+val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env
-val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
+val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
(** Associates the contents of an identifier in a [rel_context]. Raise
[Not_found] if there is no such identifier. *)
(** Functions that build argument lists matching a block of binders or a context.
[rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
*)
-val rel_vect : int -> int -> constr array
+val rel_vect : int -> int -> Constr.constr array
val rel_list : int -> int -> constr list
(** iterators/destructors on terms *)
-val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> types -> types
val it_mkProd : types -> (Name.t * types) list -> types
val it_mkLambda : constr -> (Name.t * types) list -> constr
-val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
-val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
-val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
-val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
-val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
+val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
(* Ad hoc version reinserting letin, assuming the body is defined in
the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr
+val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
(** {6 Generic iterators on constr} *)
-val map_constr_with_named_binders :
- (Name.t -> 'a -> 'a) ->
- ('a -> constr -> constr) -> 'a -> constr -> constr
val map_constr_with_binders_left_to_right :
- (Context.Rel.Declaration.t -> 'a -> 'a) ->
+ Evd.evar_map ->
+ (rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) ->
'a -> constr -> constr
val map_constr_with_full_binders :
- (Context.Rel.Declaration.t -> 'a -> 'a) ->
+ Evd.evar_map ->
+ (rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -79,57 +70,58 @@ val map_constr_with_full_binders :
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive *)
-val fold_constr_with_binders :
+val fold_constr_with_binders : Evd.evar_map ->
('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
-val fold_constr_with_full_binders :
+val fold_constr_with_full_binders : Evd.evar_map ->
(Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
'a -> 'b -> constr -> 'b
val iter_constr_with_full_binders :
- (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
- constr -> unit
+ (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a ->
+ Constr.constr -> unit
(**********************************************************************)
-val strip_head_cast : constr -> constr
-val drop_extra_implicit_args : constr -> constr
+val strip_head_cast : Evd.evar_map -> constr -> constr
+val drop_extra_implicit_args : Evd.evar_map -> constr -> constr
(** occur checks *)
exception Occur
-val occur_meta : types -> bool
-val occur_existential : types -> bool
-val occur_meta_or_existential : types -> bool
-val occur_evar : existential_key -> types -> bool
-val occur_var : env -> Id.t -> types -> bool
+val occur_meta : Evd.evar_map -> constr -> bool
+val occur_existential : Evd.evar_map -> constr -> bool
+val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_evar : Evd.evar_map -> existential_key -> constr -> bool
+val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_in_decl :
- env ->
- Id.t -> Context.Named.Declaration.t -> bool
+ env -> Evd.evar_map ->
+ Id.t -> named_declaration -> bool
(** As {!occur_var} but assume the identifier not to be a section variable *)
-val local_occur_var : Id.t -> types -> bool
+val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
-val free_rels : constr -> Int.Set.t
+val free_rels : Evd.evar_map -> constr -> Int.Set.t
(** [dependent m t] tests whether [m] is a subterm of [t] *)
-val dependent : constr -> constr -> bool
-val dependent_no_evar : constr -> constr -> bool
-val dependent_univs : constr -> constr -> bool
-val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
-val count_occurrences : constr -> constr -> int
-val collect_metas : constr -> int list
-val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+val dependent : Evd.evar_map -> constr -> constr -> bool
+val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool
+val dependent_univs : Evd.evar_map -> constr -> constr -> bool
+val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool
+val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
+val count_occurrences : Evd.evar_map -> constr -> constr -> int
+val collect_metas : Evd.evar_map -> constr -> int list
+val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
-val occur_term : constr -> constr -> bool (** Synonymous
- of dependent
- Substitution of metavariables *)
-type meta_value_map = (metavariable * constr) list
-val subst_meta : meta_value_map -> constr -> constr
+val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
+
+(* Substitution of metavariables *)
+type meta_value_map = (metavariable * Constr.constr) list
+val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
+val isMetaOf : Evd.evar_map -> metavariable -> constr -> bool
(** Type assignment for metavariables *)
-type meta_type_map = (metavariable * types) list
+type meta_type_map = (metavariable * Constr.types) list
(** [pop c] lifts by -1 the positive indexes in [c] *)
val pop : constr -> constr
@@ -140,36 +132,38 @@ val pop : constr -> constr
(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
as equality *)
-val subst_term_gen :
- (constr -> constr -> bool) -> constr -> constr -> constr
+val subst_term_gen : Evd.evar_map ->
+ (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr
(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
as equality *)
val replace_term_gen :
- (constr -> constr -> bool) ->
+ Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) ->
constr -> constr -> constr -> constr
(** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : constr -> constr -> constr
+val subst_term : Evd.evar_map -> constr -> constr -> constr
(** [replace_term d e c] replaces [d] by [e] in [c] *)
-val replace_term : constr -> constr -> constr -> constr
+val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr
(** Alternative term equalities *)
val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
-val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
+val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) ->
Reduction.conv_pb -> constr -> constr -> bool
-val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
-val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
+val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool
+val eq_constr : Evd.evar_map -> constr -> constr -> bool (* FIXME rename: erases universes*)
-val eta_reduce_head : constr -> constr
+val eta_reduce_head : Evd.evar_map -> constr -> constr
(** Flattens application lists *)
-val collapse_appl : constr -> constr
+val collapse_appl : Evd.evar_map -> constr -> constr
+
+val prod_applist : Evd.evar_map -> constr -> constr list -> constr
(** Remove recursively the casts around a term i.e.
[strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
+val strip_outer_cast : Evd.evar_map -> constr -> constr
exception CannotFilter
@@ -179,27 +173,27 @@ exception CannotFilter
(context,term), or raises [CannotFilter].
Warning: Outer-kernel sort subtyping are taken into account: c1 has
to be smaller than c2 wrt. sorts. *)
-type subst = (Context.Rel.t * constr) Evar.Map.t
-val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
+type subst = (rel_context * constr) Evar.Map.t
+val filtering : Evd.evar_map -> rel_context -> Reduction.conv_pb -> constr -> constr -> subst
-val decompose_prod_letin : constr -> int * Context.Rel.t * constr
-val align_prod_letin : constr -> constr -> Context.Rel.t * constr
+val decompose_prod_letin : Evd.evar_map -> constr -> int * rel_context * constr
+val align_prod_letin : Evd.evar_map -> constr -> constr -> rel_context * constr
(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
gives {% $ %}n{% $ %} (casts are ignored) *)
-val nb_lam : constr -> int
+val nb_lam : Evd.evar_map -> constr -> int
(** Similar to [nb_lam], but gives the number of products instead *)
-val nb_prod : constr -> int
+val nb_prod : Evd.evar_map -> constr -> int
(** Similar to [nb_prod], but zeta-contracts let-in on the way *)
-val nb_prod_modulo_zeta : constr -> int
+val nb_prod_modulo_zeta : Evd.evar_map -> constr -> int
(** Get the last arg of a constr intended to be an application *)
-val last_arg : constr -> constr
+val last_arg : Evd.evar_map -> constr -> constr
(** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : constr -> constr * constr array
+val decompose_app_vect : Evd.evar_map -> constr -> constr * constr array
val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
(constr * constr list * constr * constr list)
@@ -212,8 +206,8 @@ val add_name : Name.t -> names_context -> names_context
val lookup_name_of_rel : int -> names_context -> Name.t
val lookup_rel_of_name : Id.t -> names_context -> int
val empty_names_context : names_context
-val ids_of_rel_context : Context.Rel.t -> Id.t list
-val ids_of_named_context : Context.Named.t -> Id.t list
+val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Id.t list
+val ids_of_named_context : ('c, 't) Context.Named.pt -> Id.t list
val ids_of_context : env -> Id.t list
val names_of_rel_context : env -> names_context
@@ -225,51 +219,89 @@ val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
(* [env_rel_context_chop n env] extracts out the [n] top declarations
of the rel_context part of [env], counting both local definitions and
hypotheses *)
-val env_rel_context_chop : int -> env -> env * Context.Rel.t
+val env_rel_context_chop : int -> env -> env * rel_context
(** Set of local names *)
val vars_of_env: env -> Id.Set.t
val add_vname : Id.Set.t -> Name.t -> Id.Set.t
(** other signature iterators *)
-val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
-val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list
+val process_rel_context : (rel_declaration -> env -> env) -> env -> env
+val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
-val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t
+val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
val map_rel_context_in_env :
- (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t
+ (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
val map_rel_context_with_binders :
- (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t
+ (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
val fold_named_context_both_sides :
('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
Context.Named.t -> init:'a -> 'a
val mem_named_context_val : Id.t -> named_context_val -> bool
val compact_named_context : Context.Named.t -> Context.Compacted.t
+val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
+val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
+
val clear_named_body : Id.t -> env -> env
-val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
+val global_vars : env -> Evd.evar_map -> constr -> Id.t list
+val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
+val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
+val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
(** Gives an ordered list of hypotheses, closed by dependencies,
containing a given set *)
-val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list
(** Test if an identifier is the basename of a global reference *)
val is_section_variable : Id.t -> bool
-val isGlobalRef : constr -> bool
+val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
+
+val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
+
+val isGlobalRef : Evd.evar_map -> constr -> bool
+
+val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
-val is_template_polymorphic : env -> constr -> bool
+val is_Prop : Evd.evar_map -> constr -> bool
(** Combinators on judgments *)
-val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
(** {6 Functions to deal with impossible cases } *)
-val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit
+val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
+
+(** {5 Debug pretty-printers} *)
+
+open Evd
+
+val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
+val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
+ evar_map -> Pp.std_ppcmds
+val pr_metaset : Metaset.t -> Pp.std_ppcmds
+val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+
+(** debug printer: do not use to display terms to the casual user... *)
+
+val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
+val print_constr : constr -> std_ppcmds
+val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
+val print_named_context : env -> std_ppcmds
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
+val print_rel_context : env -> std_ppcmds
+val print_env : env -> std_ppcmds
diff --git a/engine/universes.ml b/engine/universes.ml
index 30a9ef163..ad5ff827b 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -445,15 +445,6 @@ let global_of_constr c =
| Var id -> VarRef id, Instance.empty
| _ -> raise Not_found
-let global_app_of_constr c =
- match kind_of_term c with
- | Const (c, u) -> (ConstRef c, u), None
- | Ind (i, u) -> (IndRef i, u), None
- | Construct (c, u) -> (ConstructRef c, u), None
- | Var id -> (VarRef id, Instance.empty), None
- | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
- | _ -> raise Not_found
-
open Declarations
let type_of_reference env r =
diff --git a/engine/universes.mli b/engine/universes.mli
index 725c21d29..932de941a 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -76,8 +76,8 @@ val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
{!eq_constr_univs_infer} taking kind-of-term functions, to expose
subterms of [m] and [n], arguments. *)
val eq_constr_univs_infer_with :
- (constr -> (constr,types) kind_of_term) ->
- (constr -> (constr,types) kind_of_term) ->
+ (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+ (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
@@ -130,8 +130,6 @@ val fresh_universe_context_set_instance : universe_context_set ->
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> Globnames.global_reference puniverses
-val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
-
val constr_of_global_univ : Globnames.global_reference puniverses -> constr
val extend_context : 'a in_universe_context_set -> universe_context_set ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 09:55:58 +0000