aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml235
-rw-r--r--engine/eConstr.mli41
-rw-r--r--engine/engine.mllib2
-rw-r--r--engine/evarutil.ml80
-rw-r--r--engine/evarutil.mli31
-rw-r--r--engine/evd.ml211
-rw-r--r--engine/evd.mli74
-rw-r--r--engine/ftactic.ml4
-rw-r--r--engine/logic_monad.ml2
-rw-r--r--engine/logic_monad.mli5
-rw-r--r--engine/namegen.ml79
-rw-r--r--engine/namegen.mli16
-rw-r--r--engine/nameops.ml8
-rw-r--r--engine/nameops.mli4
-rw-r--r--engine/proofview.ml110
-rw-r--r--engine/proofview.mli35
-rw-r--r--engine/proofview_monad.ml40
-rw-r--r--engine/proofview_monad.mli6
-rw-r--r--engine/termops.ml347
-rw-r--r--engine/termops.mli33
-rw-r--r--engine/uState.ml352
-rw-r--r--engine/uState.mli30
-rw-r--r--engine/univGen.ml236
-rw-r--r--engine/univGen.mli34
-rw-r--r--engine/univMinim.ml37
-rw-r--r--engine/univNames.ml88
-rw-r--r--engine/univNames.mli6
-rw-r--r--engine/univops.ml28
-rw-r--r--engine/univops.mli6
29 files changed, 1061 insertions, 1119 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..981f9454e4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -48,9 +48,10 @@ type 'a puniverses = 'a * EInstance.t
let in_punivs a = (a, EInstance.empty)
+let mkSProp = of_kind (Sort (ESorts.make Sorts.sprop))
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 mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u)))
let mkRel n = of_kind (Rel n)
let mkVar id = of_kind (Var id)
let mkMeta n = of_kind (Meta n)
@@ -72,9 +73,20 @@ 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 mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
+let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
+let mkInt i = of_kind (Int i)
+
+let mkRef (gr,u) = let open GlobRef in match gr with
+ | ConstRef c -> mkConstU (c,u)
+ | IndRef ind -> mkIndU (ind,u)
+ | ConstructRef c -> mkConstructU (c,u)
+ | VarRef x -> mkVar x
+
+let type1 = mkSort Sorts.type1
let applist (f, arg) = mkApp (f, Array.of_list arg)
+let applistc 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
@@ -93,6 +105,14 @@ 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 rec isType sigma c = match kind sigma c with
+ | Sort s -> (match ESorts.kind sigma s with
+ | Sorts.Type _ -> true
+ | _ -> false )
+ | Cast (c,_,_) -> isType sigma c
+ | _ -> false
+
let isVarId sigma id c =
match kind sigma c with Var id' -> Id.equal id id' | _ -> false
let isRelN sigma n c =
@@ -166,6 +186,13 @@ let destProj sigma c = match kind sigma c with
| Proj (p, c) -> (p, c)
| _ -> raise DestKO
+let destRef sigma c = let open GlobRef in match kind sigma c with
+ | Var x -> VarRef x, EInstance.empty
+ | Const (c,u) -> ConstRef c, u
+ | Ind (ind,u) -> IndRef ind, u
+ | Construct (c,u) -> ConstructRef c, u
+ | _ -> raise DestKO
+
let decompose_app sigma c =
match kind sigma c with
| App (f,cl) -> (f, Array.to_list cl)
@@ -275,6 +302,8 @@ let decompose_prod_n_assum sigma n c =
let existential_type = Evd.existential_type
+let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
+
let map_under_context f n c =
let f c = unsafe_to_constr (f (of_constr c)) in
of_constr (Constr.map_under_context f n (unsafe_to_constr c))
@@ -285,143 +314,27 @@ let map_return_predicate f ci p =
let f c = unsafe_to_constr (f (of_constr c)) in
of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
-let map_gen userview 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.Smart.map 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.Smart.map f l in
- if l'==l then c
- else mkEvar (e, l')
- | Case (ci,p,b,bl) when userview ->
- let b' = f b in
- let p' = map_return_predicate f ci p in
- let bl' = map_branches f ci bl in
- if b'==b && p'==p && bl'==bl then c
- else mkCase (ci, p', b', bl')
- | Case (ci,p,b,bl) ->
- let b' = f b in
- let p' = f p in
- let bl' = Array.Smart.map 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.Smart.map f tl in
- let bl' = Array.Smart.map f bl in
- if tl'==tl && bl'==bl then c
- else mkFix (ln,(lna,tl',bl'))
- | CoFix(ln,(lna,tl,bl)) ->
- let tl' = Array.Smart.map f tl in
- let bl' = Array.Smart.map f bl in
- if tl'==tl && bl'==bl then c
- else mkCoFix (ln,(lna,tl',bl'))
-
-let map_user_view = map_gen true
-let map = map_gen false
-
-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' = Array.Fun1.Smart.map 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' = Array.Fun1.Smart.map 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' = Array.Fun1.Smart.map 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' = Array.Fun1.Smart.map f l tl in
- let l' = iterate g (Array.length tl) l in
- let bl' = Array.Fun1.Smart.map f l' bl in
- if tl' == tl && bl' == bl then c0
- else mkFix (ln,(lna,tl',bl'))
- | CoFix(ln,(lna,tl,bl)) ->
- let tl' = Array.Fun1.Smart.map f l tl in
- let l' = iterate g (Array.length tl) l in
- let bl' = Array.Fun1.Smart.map 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 map_user_view sigma f c =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+
+let map sigma f c =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map f (unsafe_to_constr (whd_evar sigma c)))
+
+let map_with_binders sigma g f l c =
+ let f l c = unsafe_to_constr (f l (of_constr c)) in
+ of_constr (Constr.map_with_binders g f l (unsafe_to_constr (whd_evar sigma c)))
+
+let iter sigma f c =
+ let f c = f (of_constr c) in
+ Constr.iter f (unsafe_to_constr (whd_evar sigma c))
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 _) -> ()
+ | Construct _ | Int _) -> ()
| 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
@@ -432,31 +345,20 @@ let iter_with_full_binders sigma g f n c =
| 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
+ let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i 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
+ let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i 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 f l c = f l (of_constr c) in
+ Constr.iter_with_binders g f n (unsafe_to_constr (whd_evar sigma 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 fold sigma f acc c =
+ let f acc c = f acc (of_constr c) in
+ Constr.fold f acc (unsafe_to_constr (whd_evar sigma c))
let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
(c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
@@ -507,25 +409,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
let open UnivProblem in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
- cstrs
- | Declarations.Polymorphic_ind _ ->
- enforce_eq_instances_univs false u1 u2 cstrs
- | Declarations.Cumulative_ind cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> enforce_eq_instances_univs false u1 u2 cstrs
+ | Some variances ->
let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
- let variances = Univ.ACumulativityInfo.variance cumi in
compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
let open UnivProblem in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- cstrs
- | Declarations.Polymorphic_ind _ ->
- enforce_eq_instances_univs false u1 u2 cstrs
- | Declarations.Cumulative_ind cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> enforce_eq_instances_univs false u1 u2 cstrs
+ | Some _ ->
let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
if not (Int.equal num_cnstr_args nargs)
then enforce_eq_instances_univs false u1 u2 cstrs
@@ -691,7 +585,7 @@ let to_rel_decl = unsafe_to_rel_decl
type substl = t list
(** Operations that commute with evar-normalization *)
-let lift n c = of_constr (Vars.lift n (to_constr c))
+let lift = lift
let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
@@ -710,6 +604,7 @@ 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
@@ -774,9 +669,9 @@ let mkLambda_or_LetIn decl c =
| 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 id typ c = mkProd (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLambda id typ c = mkLambda (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (map_annot Name.mk_name id, c1, t, Vars.subst_var id.binder_name c2)
let mkNamedProd_or_LetIn decl c =
let open Context.Named.Declaration in
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..25ceffbd04 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
For getting the evar-normal form of a term with evars see
{!Evarutil.nf_evar}. *)
+val to_constr_opt : Evd.evar_map -> t -> Constr.t option
+(** Same as [to_constr], but returns [None] if some unresolved evars remain *)
+
val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
(** {5 Constructors} *)
@@ -101,13 +104,14 @@ val mkVar : Id.t -> t
val mkMeta : metavariable -> t
val mkEvar : t pexistential -> t
val mkSort : Sorts.t -> t
+val mkSProp : t
val mkProp : t
val mkSet : t
val mkType : Univ.Universe.t -> 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 mkProd : Name.t Context.binder_annot * t * t -> t
+val mkLambda : Name.t Context.binder_annot * t * t -> t
+val mkLetIn : Name.t Context.binder_annot * t * t * t -> t
val mkApp : t * t array -> t
val mkConst : Constant.t -> t
val mkConstU : Constant.t * EInstance.t -> t
@@ -120,18 +124,25 @@ 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 mkArrow : t -> Sorts.relevance -> t -> t
+val mkArrowR : t -> t -> t
+val mkInt : Uint63.t -> t
+
+val mkRef : GlobRef.t * EInstance.t -> t
+
+val type1 : t
val applist : t * t list -> t
+val applistc : 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 : Id.t Context.binder_annot -> types -> constr -> constr
+val mkNamedLetIn : Id.t Context.binder_annot -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t Context.binder_annot -> types -> types -> types
val mkNamedLambda_or_LetIn : named_declaration -> types -> types
val mkNamedProd_or_LetIn : named_declaration -> types -> types
@@ -155,6 +166,8 @@ val isCoFix : Evd.evar_map -> t -> bool
val isCase : Evd.evar_map -> t -> bool
val isProj : Evd.evar_map -> t -> bool
+val isType : Evd.evar_map -> constr -> bool
+
type arity = rel_context * ESorts.t
val destArity : Evd.evar_map -> types -> arity
val isArity : Evd.evar_map -> t -> bool
@@ -167,9 +180,9 @@ 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 destProd : Evd.evar_map -> t -> Name.t Context.binder_annot * types * types
+val destLambda : Evd.evar_map -> t -> Name.t Context.binder_annot * types * t
+val destLetIn : Evd.evar_map -> t -> Name.t Context.binder_annot * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t pexistential
@@ -180,10 +193,12 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
val decompose_app : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)
-val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_lam : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t
(** Pops lambda abstractions and letins until there are no more, skipping casts. *)
val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
@@ -199,10 +214,10 @@ val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
@raise UserError if the term doesn't have enough lambdas/letins. *)
val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
-val compose_lam : (Name.t * t) list -> t -> t
+val compose_lam : (Name.t Context.binder_annot * 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 : Evd.evar_map -> t -> (Name.t Context.binder_annot * 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
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
UnivProblem
UnivMinim
Universes
-Univops
UState
+Univops
Nameops
Evar_kinds
Evd
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fc2189f870..96beb72a56 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -11,6 +11,7 @@
open CErrors
open Util
open Names
+open Context
open Constr
open Environ
open Evd
@@ -50,6 +51,18 @@ let new_global evd x =
(* Expanding/testing/exposing existential variables *)
(****************************************************)
+let finalize ?abort_on_undefined_evars sigma f =
+ let sigma = minimize_universes sigma in
+ let uvars = ref Univ.LSet.empty in
+ let v = f (fun c ->
+ let varsc = EConstr.universes_of_constr sigma c in
+ let c = EConstr.to_constr ?abort_on_undefined_evars sigma c in
+ uvars := Univ.LSet.union !uvars varsc;
+ c)
+ in
+ let sigma = restrict_universe_context sigma !uvars in
+ sigma, v
+
(* flush_and_check_evars fails if an existential is undefined *)
exception Uninstantiated_evar of Evar.t
@@ -143,7 +156,7 @@ let is_ground_env = memo is_ground_env
exception NoHeadEvar
let head_evar sigma c =
- (** FIXME: this breaks if using evar-insensitive code *)
+ (* FIXME: this breaks if using evar-insensitive code *)
let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind c with
| Evar (evk,_) -> evk
@@ -276,7 +289,7 @@ let empty_csubst = {
}
let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
- (** Safe because this is a substitution *)
+ (* 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 ->
@@ -306,7 +319,7 @@ let update_var src tgt subst =
in
match cur with
| None ->
- (** Missing keys stand for identity substitution [src ↦ src] *)
+ (* Missing keys stand for identity substitution [src ↦ src] *)
let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
{ subst with csubst_var; csubst_rev }
@@ -325,6 +338,7 @@ type naming_mode =
| KeepUserNameAndRenameExistingEvenSectionNames
| KeepExistingNames
| FailIfConflict
+ | ProgramNaming
let push_rel_decl_to_named_context
?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
@@ -352,15 +366,16 @@ let push_rel_decl_to_named_context
using this function. For now, we only attempt to preserve the
old behaviour of Program, but ultimately, one should do something
about this whole name generation problem. *)
- if Flags.is_program_mode () then next_name_away na avoid
+ if hypnaming = ProgramNaming then next_name_away na avoid
else
- (** id_of_name_using_hdchar only depends on the rel context which is empty
- here *)
+ (* 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 sigma (RelDecl.get_type decl) na) avoid
in
match extract_if_neq id na with
| Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames ||
- hypnaming = KeepUserNameAndRenameExistingButSectionNames &&
+ (hypnaming = KeepUserNameAndRenameExistingButSectionNames ||
+ hypnaming = ProgramNaming) &&
not (is_section_variable id0) ->
(* spiwack: if [id<>id0], rather than introducing a new
binding named [id], we will keep [id0] (the name given
@@ -405,12 +420,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar_full evd evi =
- let (evd, evk) = Evd.new_evar evd evi in
+let new_pure_evar_full evd ?typeclass_candidate evi =
+ let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
let evd = Evd.declare_future_goal evk evd in
(evd, evk)
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
+ ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ =
let default_naming = IntroAnonymous in
let naming = Option.default default_naming naming in
let name = match naming with
@@ -426,35 +442,38 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
evar_concl = typ;
evar_body = Evar_empty;
evar_filter = filter;
+ evar_abstract_arguments = abstract_arguments;
evar_source = src;
- evar_candidates = candidates;
- evar_extra = store; }
+ evar_candidates = candidates }
in
- let (evd, newevk) = Evd.new_evar evd ?name evi in
+ let typeclass_candidate = if principal then Some false else typeclass_candidate in
+ let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
let evd =
if principal then Evd.declare_principal_goal newevk evd
else Evd.declare_future_goal newevk evd
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
+ ?principal sign evd typ instance =
let open EConstr in
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+ let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
evd, mkEvar (newevk,Array.of_list instance)
-let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
let instance =
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+ new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance
(* [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 ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
+ ?principal ?hypnaming env evd typ =
let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
let map c = csubst_subst subst c in
let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -462,11 +481,12 @@ let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env e
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
+ new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+ ?typeclass_candidate ?principal instance
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
- let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
+ let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
evd', (e, s)
let new_Type ?(rigid=Evd.univ_flexible) evd =
@@ -527,8 +547,8 @@ let restrict_evar evd evk filter ?src candidates =
| Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
| _ ->
let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
- (** Mark new evar as future goal, removing previous one,
- circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+ (* Mark new evar as future goal, removing previous one,
+ circumventing Proofview.advance but making Proof.run_tactic catch these. *)
let future_goals = Evd.save_future_goals evd in
let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
let evd = Evd.restore_future_goals evd future_goals in
@@ -549,7 +569,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
if Id.Set.mem id' ids then
raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
in
- Id.Set.iter check (Environ.vars_of_global env c)
+ Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
in
c
@@ -579,7 +599,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
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 ()) !evdref id h
+ if occur_var_in_decl env !evdref id h
then raise (Depends id)
in
let () = Id.Map.iter check ri in
@@ -714,7 +734,7 @@ let rec advance sigma evk =
match evi.evar_body with
| Evar_empty -> Some evk
| Evar_defined v ->
- match is_restricted_evar evi with
+ match is_restricted_evar sigma evk with
| Some evk -> advance sigma evk
| None -> None
@@ -762,13 +782,13 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
in
NamedDecl.fold_constr fold decl accu
| Some cache ->
- let id = NamedDecl.get_id decl in
+ let id = NamedDecl.get_annot decl in
let r =
- try Id.Map.find id cache.cache
+ try Id.Map.find id.binder_name cache.cache
with Not_found ->
- (** Dummy value *)
+ (* Dummy value *)
let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
- let () = cache.cache <- Id.Map.add id r cache.cache in
+ let () = cache.cache <- Id.Map.add id.binder_name r cache.cache in
r
in
let (decl', evs) = !r in
@@ -817,7 +837,7 @@ let occur_evar_upto sigma n c =
let judge_of_new_Type evd =
let open EConstr in
let (evd', s) = new_univ_variable univ_rigid evd in
- (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) })
+ (evd', { uj_val = mkType s; uj_type = mkType (Univ.super s) })
let subterm_source evk ?where (loc,k) =
let evk = match k with
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 11e07175e3..bb0da44103 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -27,8 +27,9 @@ val mk_new_meta : unit -> constr
val new_evar_from_context :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
+ ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * EConstr.t
@@ -37,22 +38,25 @@ type naming_mode =
| KeepUserNameAndRenameExistingEvenSectionNames
| KeepExistingNames
| FailIfConflict
+ | ProgramNaming
val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
+ ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?candidates:constr list -> ?store:Store.t ->
+ ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
+val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
@@ -76,8 +80,10 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
- ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
+ ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+ ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
+ ?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types ->
constr list -> evar_map * constr
@@ -177,6 +183,19 @@ val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
exception Uninstantiated_evar of Evar.t
val flush_and_check_evars : evar_map -> constr -> Constr.constr
+(** [finalize env sigma f] combines universe minimisation,
+ evar-and-universe normalisation and universe restriction.
+
+ It minimizes universes in [sigma], calls [f] a normalisation
+ function with respect to the updated [sigma] and restricts the
+ local universes of [sigma] to those encountered while running [f].
+
+ Note that the normalizer passed to [f] holds some imperative state
+ in its closure. *)
+val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
+ ((EConstr.t -> Constr.t) -> 'a) ->
+ evar_map * 'a
+
(** {6 Term manipulation up to instantiation} *)
(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..b89222cf8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -89,8 +89,8 @@ struct
| Some f2 -> normalize (CList.filter_with f1 f2)
let apply_subfilter_array filter subfilter =
- (** In both cases we statically know that the argument will contain at
- least one [false] *)
+ (* In both cases we statically know that the argument will contain at
+ least one [false] *)
match filter with
| None -> Some (Array.to_list subfilter)
| Some f ->
@@ -126,6 +126,19 @@ struct
end
+module Abstraction = struct
+
+ type abstraction =
+ | Abstract
+ | Imitate
+
+ type t = abstraction list
+
+ let identity = []
+
+ let abstract_last l = Abstract :: l
+end
+
(* The kinds of existential variables are now defined in [Evar_kinds] *)
(* The type of mappings for existential variables *)
@@ -143,19 +156,18 @@ type evar_info = {
evar_hyps : named_context_val;
evar_body : evar_body;
evar_filter : Filter.t;
+ evar_abstract_arguments : Abstraction.t;
evar_source : Evar_kinds.t Loc.located;
- evar_candidates : constr list option; (* if not None, list of allowed instances *)
- evar_extra : Store.t }
+ evar_candidates : constr list option; (* if not None, list of allowed instances *)}
let make_evar hyps ccl = {
evar_concl = ccl;
evar_hyps = hyps;
evar_body = Evar_empty;
evar_filter = Filter.identity;
+ evar_abstract_arguments = Abstraction.identity;
evar_source = Loc.tag @@ Evar_kinds.InternalHole;
- evar_candidates = None;
- evar_extra = Store.empty
-}
+ evar_candidates = None; }
let instance_mismatch () =
anomaly (Pp.str "Signature and its instance do not match.")
@@ -398,7 +410,7 @@ let rename evk id (evtoid, idtoev) =
let reassign_name_defined evk evk' (evtoid, idtoev as names) =
let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
match id with
- | None -> names (** evk' must not be defined *)
+ | None -> names (* evk' must not be defined *)
| Some id ->
(EvMap.add evk' id (EvMap.remove evk evtoid),
Id.Map.add id evk' (Id.Map.remove id idtoev))
@@ -413,8 +425,13 @@ end
type goal_kind = ToShelve | ToGiveUp
+type evar_flags =
+ { obligation_evars : Evar.Set.t;
+ restricted_evars : Evar.t Evar.Map.t;
+ typeclass_evars : Evar.Set.t }
+
type evar_map = {
- (** Existential variables *)
+ (* Existential variables *)
defn_evars : evar_info EvMap.t;
undf_evars : evar_info EvMap.t;
evar_names : EvNames.t;
@@ -425,6 +442,7 @@ type evar_map = {
last_mods : Evar.Set.t;
(** Metas *)
metas : clbinding Metamap.t;
+ evar_flags : evar_flags;
(** Interactive proofs *)
effects : Safe_typing.private_constants;
future_goals : Evar.t list; (** list of newly created evars, to be
@@ -441,20 +459,84 @@ type evar_map = {
extras : Store.t;
}
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
(*** Lifting primitive from Evar.Map. ***)
let rename evk id evd =
{ evd with evar_names = EvNames.rename evk id evd.evar_names }
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
| Evar_empty ->
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 }
+ let evar_flags =
+ if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+ let flags = d.evar_flags in
+ { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+ else d.evar_flags
+ in
+ { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
| Evar_defined _ ->
let evar_names = EvNames.remove_name_defined e d.evar_names in
{ d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+ associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
+
+(*** Evar flags: typeclasses, restricted or obligation flag *)
+
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
+
+let set_typeclass_evars evd tcs =
+ let flags = evd.evar_flags in
+ { evd with evar_flags = { flags with typeclass_evars = tcs } }
+
+let is_typeclass_evar evd evk =
+ let flags = evd.evar_flags in
+ Evar.Set.mem evk flags.typeclass_evars
+
+let get_obligation_evars evd = evd.evar_flags.obligation_evars
+
+let set_obligation_evar evd evk =
+ let flags = evd.evar_flags in
+ let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
+ { evd with evar_flags }
+
+let is_obligation_evar evd evk =
+ let flags = evd.evar_flags in
+ Evar.Set.mem evk flags.obligation_evars
+
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+ let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+ let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+ if not (evk_obligation || evk_typeclass) then evar_flags
+ else
+ let typeclass_evars =
+ if evk_typeclass then
+ let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+ Evar.Set.add evk' typeclass_evars
+ else evar_flags.typeclass_evars
+ in
+ let obligation_evars =
+ if evk_obligation then
+ let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+ Evar.Set.add evk' obligation_evars
+ else evar_flags.obligation_evars
+ in
+ { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
+let remove_evar_flags evk evar_flags =
+ { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
+ obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
+ (* Restriction information is kept. *)
+ restricted_evars = evar_flags.restricted_evars }
(** New evars *)
@@ -464,9 +546,9 @@ let evar_counter_summary_name = "evar counter"
let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
let evk = new_untyped_evar () in
- let evd = add_with_name evd ?name evk evi in
+ let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
(evd, evk)
let remove d e =
@@ -478,7 +560,9 @@ let remove d e =
in
let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
let future_goals_status = EvMap.remove e d.future_goals_status in
- { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
+ let evar_flags = remove_evar_flags e d.evar_flags in
+ { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+ evar_flags }
let find d e =
try EvMap.find e d.undf_evars
@@ -532,19 +616,19 @@ let is_defined d e = EvMap.mem e d.defn_evars
let is_undefined d e = EvMap.mem e d.undf_evars
-let existential_value d (n, args) =
- let info = find d n in
- match evar_body info with
- | Evar_defined c ->
- instantiate_evar_array info c args
- | Evar_empty ->
- raise NotInstantiatedEvar
+let existential_opt_value d (n, args) =
+ match EvMap.find_opt n d.defn_evars with
+ | None -> None
+ | Some info ->
+ match evar_body info with
+ | Evar_defined c -> Some (instantiate_evar_array info c args)
+ | Evar_empty -> None (* impossible but w/e *)
-let existential_value0 = existential_value
+let existential_value d ev = match existential_opt_value d ev with
+ | None -> raise NotInstantiatedEvar
+ | Some v -> v
-let existential_opt_value d ev =
- try Some (existential_value d ev)
- with NotInstantiatedEvar -> None
+let existential_value0 = existential_value
let existential_opt_value0 = existential_opt_value
@@ -583,12 +667,18 @@ let cmap f evd =
let create_evar_defs sigma = { sigma with
conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
+let empty_evar_flags =
+ { obligation_evars = Evar.Set.empty;
+ restricted_evars = Evar.Map.empty;
+ typeclass_evars = Evar.Set.empty }
+
let empty = {
defn_evars = EvMap.empty;
undf_evars = EvMap.empty;
universes = UState.empty;
conv_pbs = [];
last_mods = Evar.Set.empty;
+ evar_flags = empty_evar_flags;
metas = Metamap.empty;
effects = Safe_typing.empty_private_constants;
evar_names = EvNames.empty; (* id<->key for undefined evars *)
@@ -634,9 +724,7 @@ let evar_source evk d = (find d evk).evar_source
let evar_ident evk evd = EvNames.ident evk evd.evar_names
let evar_key id evd = EvNames.key id evd.evar_names
-let restricted = Store.field ()
-
-let define_aux ?dorestrict def undef evk body =
+let define_aux def undef evk body =
let oldinfo =
try EvMap.find evk undef
with Not_found ->
@@ -646,24 +734,39 @@ let define_aux ?dorestrict def undef evk body =
anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
in
let () = assert (oldinfo.evar_body == Evar_empty) in
- let evar_extra = match dorestrict with
- | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
- | None -> oldinfo.evar_extra in
- let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
+ let newinfo = { oldinfo with evar_body = Evar_defined body } in
EvMap.add evk newinfo def, EvMap.remove evk undef
(* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods
in
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
- { evd with defn_evars; undf_evars; last_mods; evar_names }
+ { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+ let evar_flags = remove_evar_flags evk evd.evar_flags in
+ define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+ let evk' = fst (destEvar body) in
+ let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+ define_gen evk body evd evar_flags
+
+let is_restricted_evar evd evk =
+ try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+ with Not_found -> None
-let is_restricted_evar evi =
- Store.get evi.evar_extra restricted
+let declare_restricted_evar evar_flags evk evk' =
+ { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
+
+(* In case of restriction, we declare the restriction and inherit the obligation
+ and typeclass flags. *)
let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
@@ -679,9 +782,11 @@ let restrict evk filter ?candidates ?src evd =
let ctxt = Filter.filter_list filter (evar_context evar_info) in
let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
let body = mkEvar(evk',id_inst) in
- let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
+ let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+ let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
+ let evar_flags = inherit_evar_flags evar_flags evk evk' in
{ evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
- defn_evars; last_mods; evar_names }, evk'
+ defn_evars; last_mods; evar_names; evar_flags }, evk'
let downcast evk ccl evd =
let evar_info = EvMap.find evk evd.undf_evars in
@@ -762,8 +867,9 @@ let universe_context_set d = UState.context_set d.universes
let to_universe_context evd = UState.context evd.universes
-let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
-let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
+
+let const_univ_entry = univ_entry
let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
@@ -792,7 +898,7 @@ let new_univ_variable ?loc ?name rigid evd =
let new_sort_variable ?loc ?name rigid d =
let (d', u) = new_univ_variable ?loc rigid ?name d in
- (d', Type u)
+ (d', Sorts.sort_of_univ u)
let add_global_univ d u =
{ d with universes = UState.add_global_univ d.universes u }
@@ -801,6 +907,9 @@ let make_flexible_variable evd ~algebraic u =
{ evd with universes =
UState.make_flexible_variable evd.universes ~algebraic u }
+let make_nonalgebraic_variable evd u =
+ { evd with universes = UState.make_nonalgebraic_variable evd.universes u }
+
(****************************************)
(* Operations on constants *)
(****************************************)
@@ -818,7 +927,7 @@ let fresh_constructor_instance ?loc env evd c =
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
- with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+ with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
let is_sort_variable evd s = UState.is_sort_variable evd.universes s
@@ -853,10 +962,10 @@ let normalize_universe_instance evd l =
let normalize_sort evars s =
match s with
- | Prop | Set -> s
+ | SProp | Prop | Set -> s
| Type u ->
let u' = normalize_universe evars u in
- if u' == u then s else Type u'
+ if u' == u then s else Sorts.sort_of_univ u'
(* FIXME inefficient *)
let set_eq_sort env d s1 s2 =
@@ -1019,6 +1128,7 @@ let set_metas evd metas = {
universes = evd.universes;
conv_pbs = evd.conv_pbs;
last_mods = evd.last_mods;
+ evar_flags = evd.evar_flags;
metas;
effects = evd.effects;
evar_names = evd.evar_names;
@@ -1247,14 +1357,14 @@ module MiniEConstr = struct
| None -> c
end
| App (f, args) when isEvar f ->
- (** Enforce smart constructor invariant on applications *)
+ (* 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. *)
+ (* Enforce smart constructor invariant on casts. *)
let ev = destEvar c0 in
begin match safe_evar_value sigma ev with
| None -> c
@@ -1282,6 +1392,13 @@ module MiniEConstr = struct
in
UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
+ let to_constr_opt sigma c =
+ let evar_value ev = Some (existential_value sigma ev) in
+ try
+ Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c)
+ with NotInstantiatedEvar ->
+ None
+
let of_named_decl d = d
let unsafe_to_named_decl d = d
let of_rel_decl d = d
diff --git a/engine/evd.mli b/engine/evd.mli
index 1a5614988d..b0fcddb068 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -77,20 +77,28 @@ sig
end
+module Abstraction : sig
+ type abstraction =
+ | Abstract
+ | Imitate
+
+ type t = abstraction list
+
+ val identity : t
+
+ val abstract_last : t -> t
+end
+
(** {6 Evar infos} *)
type evar_body =
| Evar_empty
| Evar_defined of econstr
-
-module Store : Store.S
-(** Datatype used to store additional information in evar maps. *)
-
type evar_info = {
evar_concl : econstr;
(** Type of the evar. *)
- evar_hyps : named_context_val; (** TODO econstr? *)
+ evar_hyps : named_context_val; (* TODO econstr? *)
(** Context of the evar. *)
evar_body : evar_body;
(** Optional content of the evar. *)
@@ -98,12 +106,14 @@ type evar_info = {
(** Boolean mask over {!evar_hyps}. Should have the same length.
When filtered out, the corresponding variable is not allowed to occur
in the solution *)
+ evar_abstract_arguments : Abstraction.t;
+ (** Boolean information over {!evar_hyps}, telling if an hypothesis instance
+ can be imitated or should stay abstract in HO unification problems
+ and inversion (see [second_order_matching_with_args] for its use). *)
evar_source : Evar_kinds.t located;
(** Information about the evar. *)
evar_candidates : econstr list option;
(** List of possible solutions when known that it is a finite list *)
- evar_extra : Store.t
- (** Extra store, used for clever hacks. *)
}
val make_evar : named_context_val -> etypes -> evar_info
@@ -145,7 +155,7 @@ val has_undefined : evar_map -> bool
there are uninstantiated evars in [sigma]. *)
val new_evar : evar_map ->
- ?name:Id.t -> evar_info -> evar_map * Evar.t
+ ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Creates a fresh evar mapping to the given information. *)
val add : evar_map -> Evar.t -> evar_info -> evar_map
@@ -182,7 +192,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
(** Same as {!raw_map}, but restricted to undefined evars. For efficiency
reasons. *)
-val define : Evar.t-> econstr -> evar_map -> evar_map
+val define : Evar.t -> econstr -> evar_map -> evar_map
(** Set the body of an evar to the given constr. It is expected that:
{ul
{- The evar is already present in the evarmap.}
@@ -190,6 +200,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map
{- All the evars present in the constr should be present in the evar map.}
} *)
+val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map
+(** Same as [define ev body evd], except the body must be an existential variable [ev'].
+ This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *)
+
val cmap : (econstr -> econstr) -> evar_map -> evar_map
(** Map the function on all terms in the evar map. *)
@@ -210,6 +224,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
val drop_all_defined : evar_map -> evar_map
+val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t
+
(** {6 Instantiating partial terms} *)
exception NotInstantiatedEvar
@@ -247,9 +263,30 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
possibly limiting the instances to a set of candidates (candidates
are filtered according to the filter) *)
-val is_restricted_evar : evar_info -> Evar.t option
+val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
(** Tell if an evar comes from restriction of another evar, and if yes, which *)
+val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
+(** Mark the given set of evars as available for resolution.
+
+ Precondition: they should indeed refer to undefined typeclass evars.
+ *)
+
+val get_typeclass_evars : evar_map -> Evar.Set.t
+(** The set of undefined typeclass evars *)
+
+val is_typeclass_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared resolvable for typeclass resolution *)
+
+val get_obligation_evars : evar_map -> Evar.Set.t
+(** The set of obligation evars *)
+
+val set_obligation_evar : evar_map -> Evar.t -> evar_map
+(** Declare an evar as an obligation *)
+
+val is_obligation_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared as an obligation *)
+
val downcast : Evar.t-> etypes -> evar_map -> evar_map
(** Change the type of an undefined evar to a new type assumed to be a
subtype of its current type; subtyping must be ensured by caller *)
@@ -357,6 +394,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
*)
+module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
+
val get_extra_data : evar_map -> Store.t
val set_extra_data : Store.t -> evar_map -> evar_map
@@ -522,6 +562,7 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
+
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
@@ -537,9 +578,13 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid
val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map
(** See [UState.make_flexible_variable] *)
+val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
+(** See [UState.make_nonalgebraic_variable]. *)
+
val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
not a local sort variable declared in [evm] *)
+
val is_flexible_level : evar_map -> Univ.Level.t -> bool
(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
@@ -568,12 +613,12 @@ val universes : evar_map -> UGraph.t
[Univ.ContextSet.to_context]. *)
val to_universe_context : evar_map -> Univ.UContext.t
-val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-(** NB: [ind_univ_entry] cannot create cumulative entries. *)
-val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
-val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
@@ -660,6 +705,7 @@ module MiniEConstr : sig
val of_constr_array : Constr.t array -> t array
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
+ val to_constr_opt : evar_map -> t -> Constr.t option
val unsafe_to_constr : t -> Constr.t
val unsafe_to_constr_array : t array -> Constr.t array
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index b371884ba4..ac0344148a 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
| Depends l ->
let f arg = f arg >>= function
| Uniform x ->
- (** We dispatch the uniform result on each goal under focus, as we know
- that the [m] argument was actually dependent. *)
+ (* We dispatch the uniform result on each goal under focus, as we know
+ that the [m] argument was actually dependent. *)
Proofview.Goal.goals >>= fun goals ->
let ans = List.map (fun g -> (g,x)) goals in
Proofview.tclUNIT ans
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4afa817b27..e0c24f049f 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 545334ce9a..3e57baab26 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
@@ -51,8 +53,10 @@ module NonLogical : sig
val ref : 'a -> 'a ref t
(** [Pervasives.(:=)] *)
+
val (:=) : 'a ref -> 'a -> unit t
(** [Pervasives.(!)] *)
+
val (!) : 'a ref -> 'a t
val read_line : string t
@@ -67,6 +71,7 @@ module NonLogical : sig
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
val raise : ?info:Exninfo.info -> exn -> 'a t
+
(** [try ... with ...] but restricted to {!Exception}. *)
val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
val timeout : int -> 'a t -> 'a t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ce759a3fb..10ece55a63 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -18,10 +18,10 @@ open Util
open Names
open Term
open Constr
+open Context
open Environ
open EConstr
open Vars
-open Nametab
open Nameops
open Libnames
open Globnames
@@ -82,14 +82,14 @@ let is_imported_ref = function
let is_global id =
try
- let ref = locate (qualid_of_ident id) in
+ let ref = Nametab.locate (qualid_of_ident id) in
not (is_imported_ref ref)
with Not_found ->
false
let is_constructor id =
try
- match locate (qualid_of_ident id) with
+ match Nametab.locate (qualid_of_ident id) with
| ConstructRef _ -> true
| _ -> false
with Not_found ->
@@ -116,10 +116,10 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
| Cast (c,_,_) | App (c,_) -> hdrec c
| Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
| Const _ | Ind _ | Construct _ | Var _ as c ->
- Some (basename_of_global (global_of_constr c))
+ Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
- Some (match lna.(i) with Name id -> id | _ -> assert false)
- | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+ Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
+ | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
in
hdrec c
@@ -137,6 +137,7 @@ let lowercase_first_char id = (* First character of a constr *)
s ^ Unicode.lowercase_first_char s'
let sort_hdchar = function
+ | SProp -> "P"
| Prop -> "P"
| Set -> "S"
| Type _ -> "T"
@@ -148,22 +149,23 @@ let hdchar env sigma c =
| Cast (c,_,_) | App (c,_) -> hdrec k c
| Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
| Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
- | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
- | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
| Var id -> lowercase_first_char id
| 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 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)
+ try match let d = lookup_rel (n-k) env in get_name d, get_type d with
+ | Name id, _ -> lowercase_first_char id
+ | Anonymous, t -> hdrec 0 (lift (n-k) t)
with Not_found -> "y")
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
- let id = match lna.(i) with Name id -> id | _ -> assert false in
+ let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
lowercase_first_char id
| Evar _ (* We could do better... *)
| Meta _ | Case (_, _, _, _) -> "y"
+ | Int _ -> "i"
in
hdrec 0 c
@@ -175,18 +177,20 @@ let named_hd env sigma a = function
| Anonymous -> Name (Id.of_string (hdchar env sigma a))
| x -> x
-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 mkProd_name env sigma (n,a,b) = mkProd (map_annot (named_hd env sigma a) n, a, b)
+let mkLambda_name env sigma (n,a,b) = mkLambda (map_annot (named_hd env sigma a) n, a, b)
let lambda_name = mkLambda_name
let prod_name = mkProd_name
-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 prod_create env sigma (r,a,b) =
+ mkProd (make_annot (named_hd env sigma a Anonymous) r, a, b)
+let lambda_create env sigma (r,a,b) =
+ mkLambda (make_annot (named_hd env sigma a Anonymous) r, a, b)
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)
+ | LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env sigma t) na, t)
+ | LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env sigma c) na, c, t)
let name_context env sigma hyps =
snd
@@ -209,25 +213,18 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
(* Introduce a mode where auto-generated names are mangled
to test dependence of scripts on auto-generated names *)
-let mangle_names = ref false
-
-let _ = Goptions.(
- declare_bool_option
- { optdepr = false;
- optname = "mangle auto-generated names";
- optkey = ["Mangle";"Names"];
- optread = (fun () -> !mangle_names);
- optwrite = (:=) mangle_names; })
+let get_mangle_names =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~name:"mangle auto-generated names"
+ ~key:["Mangle";"Names"]
+ ~value:false
let mangle_names_prefix = ref (Id.of_string "_0")
-let set_prefix x = mangle_names_prefix := forget_subscript x
-let set_mangle_names_mode x = begin
- set_prefix x;
- mangle_names := true
- end
+let set_prefix x = mangle_names_prefix := forget_subscript x
-let _ = Goptions.(
+let () = Goptions.(
declare_string_option
{ optdepr = false;
optname = "mangled names prefix";
@@ -239,7 +236,7 @@ let _ = Goptions.(
with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")))
end })
-let mangle_id id = if !mangle_names then !mangle_names_prefix else id
+let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id
(* Looks for next "good" name by lifting subscript *)
@@ -267,7 +264,7 @@ let visible_ids sigma (nenv, c) =
begin
try
let gseen = GlobRef.Set_env.add g gseen in
- let short = shortest_qualid_of_global Id.Set.empty g in
+ let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
let dir, id = repr_qualid short in
let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
accu := (gseen, vseen, ids)
@@ -336,7 +333,7 @@ let next_name_away_in_goal na avoid =
let next_global_ident_away id avoid =
let id = if Id.Set.mem id avoid then restart_subscript id else id in
- let bad id = Id.Set.mem id avoid || is_global id in
+ let bad id = Id.Set.mem id avoid || Global.exists_objlabel (Label.of_id id) in
next_ident_away_from id bad
(* 4- Looks for next fresh name outside a list; if name already used,
@@ -366,7 +363,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 sigma =
- (** FIXME: this is inefficient, but only used in printing *)
+ (* FIXME: this is inefficient, but only used in printing *)
let avoid = ref (ids_of_named_context_val (named_context_val env)) in
let sign = named_context_val env in
let rels = rel_context env in
@@ -463,13 +460,13 @@ let rename_bound_vars_as_displayed sigma avoid env c =
| Prod (na,c1,c2) ->
let na',avoid' =
compute_displayed_name_in sigma
- (RenamingElsewhereFor (env,c2)) avoid na c2 in
- mkProd (na', c1, rename avoid' (na' :: env) c2)
+ (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
+ mkProd ({na with binder_name=na'}, c1, rename avoid' (na' :: env) c2)
| LetIn (na,c1,t,c2) ->
let na',avoid' =
compute_displayed_let_name_in sigma
- (RenamingElsewhereFor (env,c2)) avoid na c2 in
- mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
+ (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
+ mkLetIn ({na with binder_name=na'},c1,t, rename avoid' (na' :: env) c2)
| Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
| _ -> c
in
diff --git a/engine/namegen.mli b/engine/namegen.mli
index a53c3a0d1f..240fd8fa81 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -44,15 +44,15 @@ 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 -> evar_map -> Name.t * types * types -> types
-val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr
+val mkProd_name : env -> evar_map -> Name.t Context.binder_annot * types * types -> types
+val mkLambda_name : env -> evar_map -> Name.t Context.binder_annot * types * constr -> constr
(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> evar_map -> Name.t * types * types -> types
-val lambda_name : env -> evar_map -> Name.t * types * constr -> constr
+val prod_name : env -> evar_map -> Name.t Context.binder_annot * types * types -> types
+val lambda_name : env -> evar_map -> Name.t Context.binder_annot * types * constr -> constr
-val prod_create : env -> evar_map -> types * types -> constr
-val lambda_create : env -> evar_map -> types * constr -> constr
+val prod_create : env -> evar_map -> Sorts.relevance * types * types -> constr
+val lambda_create : env -> evar_map -> Sorts.relevance * types * constr -> constr
val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration
val name_context : env -> evar_map -> rel_context -> rel_context
@@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed :
val compute_displayed_name_in_gen :
(evar_map -> int -> 'a -> bool) ->
evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
-
-val set_mangle_names_mode : Id.t -> unit
-(** Turn on mangled names mode and with the given prefix.
- @raise UserError if the argument is invalid as an identifier. *)
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 735a59fe51..2047772cfe 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -69,7 +69,7 @@ let root_of_id id =
[bar0] ↦ [bar1]
[bar00] ↦ [bar01]
[bar1] ↦ [bar2]
- [bar01] ↦ [bar01]
+ [bar01] ↦ [bar02]
[bar9] ↦ [bar10]
[bar09] ↦ [bar10]
[bar99] ↦ [bar100]
@@ -132,6 +132,7 @@ sig
val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
val get_id : t -> Id.t
val pick : t -> t -> t
+ val pick_annot : t Context.binder_annot -> t Context.binder_annot -> t Context.binder_annot
val cons : t -> Id.t list -> Id.t list
val to_option : Name.t -> Id.t option
@@ -176,6 +177,11 @@ struct
| Name _ -> na1
| Anonymous -> na2
+ let pick_annot na1 na2 =
+ let open Context in
+ match na1.binder_name with
+ | Name _ -> na1 | Anonymous -> na2
+
let cons na l =
match na with
| Anonymous -> l
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 8a93fad8cc..0e75fed045 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -16,6 +16,7 @@ val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
val atompart_of_id : Id.t -> string (** remove trailing digits *)
+
val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
val add_suffix : Id.t -> string -> Id.t
@@ -83,6 +84,9 @@ module Name : sig
(** [pick na na'] returns [Anonymous] if both names are [Anonymous].
Pick one of [na] or [na'] otherwise. *)
+ val pick_annot : Name.t Context.binder_annot -> Name.t Context.binder_annot ->
+ Name.t Context.binder_annot
+
val cons : Name.t -> Id.t list -> Id.t list
(** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 12d31e5f46..2d693e0259 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -39,7 +39,7 @@ let proofview p =
let compact el ({ solution } as pv) =
let nf c = Evarutil.nf_evar solution c in
- let nf0 c = EConstr.(to_constr solution (of_constr c)) in
+ let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (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
@@ -60,19 +60,14 @@ type telescope =
| TNil of Evd.evar_map
| TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
-let typeclass_resolvable = Evd.Store.field ()
-
let dependent_init =
- (* Goals are created with a store which marks them as unresolvable
- for type classes. *)
- let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
(* Goals don't have a source location. *)
let src = Loc.tag @@ Evar_kinds.GoalEvar in
(* Main routine *)
let rec aux = function
| TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
| TCons (env, sigma, typ, t) ->
- let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in
+ let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
let (gl, _) = EConstr.destEvar sigma econstr in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
let entry = (econstr, typ) :: ret in
@@ -228,9 +223,9 @@ module Proof = Logical
type +'a tactic = 'a Proof.t
(** Applies a tactic to the current proofview. *)
-let apply env t sp =
+let apply ~name ~poly env t sp =
let open Logic_monad in
- let ans = Proof.repr (Proof.run t false (sp,env)) in
+ let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in
let ans = Logic_monad.NonLogical.run ans in
match ans with
| Nil (e, info) -> iraise (TacticFailure e, info)
@@ -641,7 +636,7 @@ let shelve =
let open Proof in
Comb.get >>= fun initial ->
Comb.set [] >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >>
Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
let shelve_goals l =
@@ -649,7 +644,7 @@ let shelve_goals l =
Comb.get >>= fun initial ->
let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
Comb.set comb >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >>
Shelf.modify (fun gls -> gls @ l)
(** [depends_on sigma src tgt] checks whether the goal [src] appears
@@ -665,9 +660,9 @@ let unifiable_delayed g l =
let free_evars sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
(ev, fevs)
@@ -677,9 +672,9 @@ let free_evars sigma l =
let free_evars_with_state sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let ev = drop_state ev in
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
@@ -715,7 +710,7 @@ let shelve_unifiable_informative =
Pv.get >>= fun initial ->
let (u,n) = partition_unifiable initial.solution initial.comb in
Comb.set n >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >>
let u = CList.map drop_state u in
Shelf.modify (fun gls -> gls @ u) >>
tclUNIT u
@@ -745,26 +740,28 @@ let unshelve l p =
let l = undefined p.solution l in
{ p with comb = p.comb@l }
-let mark_in_evm ~goal evd content =
- let info = Evd.find evd content in
- let info =
+let mark_in_evm ~goal evd evars =
+ let evd =
if goal then
- { info with Evd.evar_source = match info.Evd.evar_source with
- (* Two kinds for goal evars:
- - GoalEvar (morally not dependent)
- - VarInstance (morally dependent of some name).
- This is a heuristic for naming these evars. *)
- | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
- Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
- | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
- | loc,_ -> loc,Evar_kinds.GoalEvar }
- else info
- in
- let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
- | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
- | Some () -> info
+ let mark evd content =
+ let info = Evd.find evd content in
+ let info =
+ { info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
+ | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+ | loc,_ -> loc,Evar_kinds.GoalEvar }
+ in Evd.add evd content info
+ in CList.fold_left mark evd evars
+ else evd
in
- Evd.add evd content info
+ let tcs = Evd.get_typeclass_evars evd in
+ let evset = Evar.Set.of_list evars in
+ Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset)
let with_shelf tac =
let open Proof in
@@ -781,7 +778,7 @@ let with_shelf tac =
let sigma = Evd.restore_future_goals sigma fgoals in
(* Ensure we mark and return only unsolved goals *)
let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
- let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+ let sigma = mark_in_evm ~goal:false sigma gls' in
let npv = { npv with shelf; solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
@@ -797,7 +794,7 @@ let goodmod p m =
let cycle n =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.(str"cycle "++int n))) >>
Comb.modify begin fun initial ->
let l = CList.length initial in
let n' = goodmod n l in
@@ -807,7 +804,7 @@ let cycle n =
let swap i j =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
Comb.modify begin fun initial ->
let l = CList.length initial in
let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -822,7 +819,7 @@ let swap i j =
let revgoals =
let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"revgoals")) >>
Comb.modify CList.rev
let numgoals =
@@ -861,7 +858,7 @@ let give_up =
Comb.get >>= fun initial ->
Comb.set [] >>
mark_as_unsafe >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"give_up")) >>
Giveup.put (CList.map drop_state initial)
@@ -879,9 +876,9 @@ module Progress = struct
let eq_named_declaration d1 d2 =
match d1, d2 with
| LocalAssum (i1,t1), LocalAssum (i2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
+ Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
| LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
+ Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
&& eq_constr sigma1 sigma2 t1 t2
| _ ->
false
@@ -996,7 +993,10 @@ let tclTIME s t =
tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
in aux 0 t
-
+let tclProofInfo =
+ let open Proof in
+ Logical.current >>= fun P.{name; poly} ->
+ tclUNIT (name, poly)
(** {7 Unsafe primitives} *)
@@ -1035,7 +1035,7 @@ module Unsafe = struct
let reset_future_goals p =
{ p with solution = Evd.reset_future_goals p.solution }
- let mark_as_goal evd content =
+ let mark_as_goals evd content =
mark_in_evm ~goal:true evd content
let advance = Evarutil.advance
@@ -1043,9 +1043,7 @@ module Unsafe = struct
let undefined = undefined
let mark_as_unresolvable p gl =
- { p with solution = mark_in_evm ~goal:false p.solution gl }
-
- let typeclass_resolvable = typeclass_resolvable
+ { p with solution = mark_in_evm ~goal:false p.solution [gl] }
end
@@ -1065,10 +1063,6 @@ let goal_nf_evar sigma gl =
let sigma = Evd.add sigma gl evi in
(gl, sigma)
-let goal_extra evars gl =
- let evi = Evd.find evars gl in
- evi.Evd.evar_extra
-
let catchable_exception = function
| Logic_monad.Exception _ -> false
@@ -1093,7 +1087,6 @@ module Goal = struct
let sigma {sigma} = sigma
let hyps {env} = EConstr.named_context env
let concl {concl} = concl
- let extra {sigma; self} = goal_extra sigma self
let gmake_with info env sigma goal state =
{ env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
@@ -1167,7 +1160,7 @@ module Goal = struct
let sigma = step.solution in
let map goal =
match cleared_alias sigma goal with
- | None -> None (** ppedrot: Is this check really necessary? *)
+ | None -> None (* ppedrot: Is this check really necessary? *)
| Some goal ->
let gl =
Env.get >>= fun env ->
@@ -1198,9 +1191,9 @@ module Trace = struct
let log m = InfoL.leaf (Info.Msg m)
let name_tactic m t = InfoL.tag (Info.Tactic m) t
- let pr_info ?(lvl=0) info =
+ let pr_info env sigma ?(lvl=0) info =
assert (lvl >= 0);
- Info.(print (collapse lvl info))
+ Info.(print env sigma (collapse lvl info))
end
@@ -1244,7 +1237,7 @@ module V82 = struct
let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in
let sgs = CList.flatten goalss in
let sgs = undefined evd sgs in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
+ InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
Pv.set { ps with solution = evd; comb = sgs; }
with e when catchable_exception e ->
let (e, info) = CErrors.push e in
@@ -1285,7 +1278,8 @@ module V82 = struct
let of_tactic t gls =
try
let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
- let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
+ let name, poly = Names.Id.of_string "legacy_pe", false in
+ let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
with Logic_monad.TacticFailure e as src ->
let (_, info) = CErrors.push src in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0bb3229a9b..680a93f0cc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -156,10 +156,15 @@ type +'a tactic
tactic has given up. In case of multiple success the first one is
selected. If there is no success, fails with
{!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
- * proofview
- * (bool*Evar.t list*Evar.t list)
- * Proofview_monad.Info.tree
+val apply
+ : name:Names.Id.t
+ -> poly:bool
+ -> Environ.env
+ -> 'a tactic
+ -> proofview
+ -> 'a * proofview
+ * (bool*Evar.t list*Evar.t list)
+ * Proofview_monad.Info.tree
(** {7 Monadic primitives} *)
@@ -398,6 +403,7 @@ val tclPROGRESS : 'a tactic -> 'a tactic
val tclCHECKINTERRUPT : unit tactic
exception Timeout
+
(** [tclTIMEOUT n t] can have only one success.
In case of timeout if fails with [tclZERO Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
@@ -406,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
identifying annotation if present *)
val tclTIME : string option -> 'a tactic -> 'a tactic
+(** Internal, don't use. *)
+val tclProofInfo : (Names.Id.t * bool) tactic
+[@@ocaml.deprecated "internal, don't use"]
+
(** {7 Unsafe primitives} *)
(** The primitives in the [Unsafe] module should be avoided as much as
@@ -456,9 +466,9 @@ module Unsafe : sig
(** Clears the future goals store in the proof view. *)
val reset_future_goals : proofview -> proofview
- (** Give an evar the status of a goal (changes its source location
- and makes it unresolvable for type classes. *)
- val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+ (** Give the evars the status of a goal (changes their source location
+ and makes them unresolvable for type classes. *)
+ val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
(** Make an evar unresolvable for type classes. *)
val mark_as_unresolvable : proofview -> Evar.t -> proofview
@@ -475,8 +485,6 @@ module Unsafe : sig
val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
Proofview_monad.goal_with_state list
- val typeclass_resolvable : unit Evd.Store.field
-
end
(** This module gives access to the innards of the monad. Its use is
@@ -507,7 +515,6 @@ module Goal : sig
val hyps : t -> named_context
val env : t -> Environ.env
val sigma : t -> Evd.evar_map
- val extra : t -> Evd.Store.t
val state : t -> Proofview_monad.StateStore.t
(** [nf_enter t] applies the goal-dependent tactic [t] in each goal
@@ -520,8 +527,8 @@ module Goal : sig
(** Like {!nf_enter}, but does not normalize the goal beforehand. *)
val enter : (t -> unit tactic) -> unit tactic
- (** Like {!enter}, but assumes exactly one goal under focus, raising *)
- (** a fatal error otherwise. *)
+ (** Like {!enter}, but assumes exactly one goal under focus, raising
+ a fatal error otherwise. *)
val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
(** Recover the list of current goals under focus, without evar-normalization.
@@ -550,7 +557,7 @@ module Trace : sig
val log : Proofview_monad.lazy_msg -> unit tactic
val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
- val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
+ val pr_info : Environ.env -> Evd.evar_map -> ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
end
@@ -615,8 +622,10 @@ module Notations : sig
(** {!tclBIND} *)
val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
(** {!tclTHEN} *)
val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+
(** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 52bcabf958..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -64,8 +64,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.t
-let pr_lazy_msg msg = msg ()
+type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
(** Info trace. *)
module Info = struct
@@ -80,9 +79,7 @@ module Info = struct
type state = tag Trace.incr
type tree = tag Trace.forest
-
-
- let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
+ let pr_in_comments env sigma m = Pp.(str"(* "++ m env sigma ++str" *)")
let unbranch = function
| Trace.Seq (DBranch,brs) -> brs
@@ -112,31 +109,31 @@ module Info = struct
(** [with_sep] is [true] when [Tactic m] must be printed with a
trailing semi-colon. *)
- let rec pr_tree with_sep = let open Trace in function
- | Seq (Msg m,[]) -> pr_in_comments m
+ let rec pr_tree env sigma with_sep = let open Trace in function
+ | Seq (Msg m,[]) -> pr_in_comments env sigma m
| Seq (Tactic m,_) ->
let tail = if with_sep then Pp.str";" else Pp.mt () in
- Pp.(pr_lazy_msg m ++ tail)
+ Pp.(m env sigma ++ tail)
| Seq (Dispatch,brs) ->
let tail = if with_sep then Pp.str";" else Pp.mt () in
- Pp.(pr_dispatch brs++tail)
+ Pp.(pr_dispatch env sigma brs++tail)
| Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
- and pr_dispatch brs =
+ and pr_dispatch env sigma brs =
let open Pp in
let brs = List.map unbranch brs in
match brs with
- | [br] -> pr_forest br
+ | [br] -> pr_forest env sigma br
| _ ->
let sep () = spc()++str"|"++spc() in
- let branches = prlist_with_sep sep pr_forest brs in
+ let branches = prlist_with_sep sep (pr_forest env sigma) brs in
str"[>"++spc()++branches++spc()++str"]"
- and pr_forest = function
+ and pr_forest env sigma = function
| [] -> Pp.mt ()
- | [tr] -> pr_tree false tr
- | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
+ | [tr] -> pr_tree env sigma false tr
+ | tr::l -> Pp.(pr_tree env sigma true tr ++ pr_forest env sigma l)
- let print f =
- pr_forest (compress f)
+ let print env sigma f =
+ pr_forest env sigma (compress f)
let rec collapse_tree n t =
let open Trace in
@@ -180,7 +177,7 @@ module P = struct
type s = proofview * Environ.env
(** Recording info trace (true) or not. *)
- type e = bool
+ type e = { trace: bool; name : Names.Id.t; poly : bool }
(** Status (safe/unsafe) * shelved goals * given up *)
type w = bool * goal list
@@ -257,13 +254,16 @@ end
(** Lens and utilies pertaining to the info trace *)
module InfoL = struct
- let recording = Logical.current
+ let recording = Logical.(map (fun {P.trace} -> trace) current)
let if_recording t =
let open Logical in
recording >>= fun r ->
if r then t else return ()
- let record_trace t = Logical.local true t
+ let record_trace t =
+ Logical.(
+ current >>= fun s ->
+ local {s with P.trace = true} t)
let raw_update = Logical.update
let update f = if_recording (raw_update f)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 9d75242175..3437b6ce77 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -45,7 +45,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.t
+type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
(** Info trace. *)
module Info : sig
@@ -60,7 +60,7 @@ module Info : sig
type state = tag Trace.incr
type tree = tag Trace.forest
- val print : tree -> Pp.t
+ val print : Environ.env -> Evd.evar_map -> tree -> Pp.t
(** [collapse n t] flattens the first [n] levels of [Tactic] in an
info trace, effectively forgetting about the [n] top level of
@@ -98,7 +98,7 @@ module P : sig
val wprod : w -> w -> w
(** Recording info trace (true) or not. *)
- type e = bool
+ type e = { trace: bool; name : Names.Id.t; poly : bool }
type u = Info.state
diff --git a/engine/termops.ml b/engine/termops.ml
index efe1525c9a..8e12c9be88 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -15,6 +15,7 @@ open Names
open Nameops
open Term
open Constr
+open Context
open Vars
open Environ
@@ -24,97 +25,21 @@ module CompactedDecl = Context.Compacted.Declaration
module Internal = struct
-(* Sorts and sort family *)
-
-let print_sort = function
- | Set -> (str "Set")
- | Prop -> (str "Prop")
- | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
-
-let pr_sort_family = function
- | InSet -> (str "Set")
- | InProp -> (str "Prop")
- | InType -> (str "Type")
-
-let pr_con sp = str(Constant.to_string sp)
-
-let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
- let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
- hov 1
- (str"fix " ++ int i ++ spc() ++ str"{" ++
- v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
- Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
- cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
- str"}")
-
-let pr_puniverses p u =
- if Univ.Instance.is_empty u then p
- else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
-
-(* Minimalistic constr printer, typically for debugging *)
-
-let rec pr_constr c = match kind c with
- | Rel n -> str "#"++int n
- | Meta n -> str "Meta(" ++ int n ++ str ")"
- | Var id -> Id.print id
- | Sort s -> print_sort s
- | Cast (c,_, t) -> hov 1
- (str"(" ++ pr_constr c ++ cut() ++
- str":" ++ pr_constr t ++ str")")
- | Prod (Name(id),t,c) -> hov 1
- (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++
- spc() ++ pr_constr c)
- | Prod (Anonymous,t,c) -> hov 0
- (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
- pr_constr c ++ str")")
- | Lambda (na,t,c) -> hov 1
- (str"fun " ++ Name.print na ++ str":" ++
- pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
- | LetIn (na,b,t,c) -> hov 0
- (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++
- str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
- pr_constr c)
- | App (c,l) -> hov 1
- (str"(" ++ pr_constr c ++ spc() ++
- prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
- | Evar (e,l) -> hov 1
- (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
- prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
- | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
- | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
- | Construct (((sp,i),j),u) ->
- str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
- | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
- | Case (ci,p,c,bl) -> v 0
- (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
- pr_constr c ++ str"of") ++ cut() ++
- prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
- cut() ++ str"end")
- | Fix f -> pr_fix pr_constr f
- | CoFix(i,(lna,tl,bl)) ->
- let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
- hov 1
- (str"cofix " ++ int i ++ spc() ++ str"{" ++
- v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
- Name.print na ++ str":" ++ pr_constr ty ++
- cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
- str"}")
-
-let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
-let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
-let term_printer = ref debug_print_constr_env
+let pr_sort_family = Sorts.pr_sort_family
+[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
+let pr_fix = Constr.debug_print_fix
+[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t =
- let env = Global.env () in
- let evd = Evd.from_env env in
- !term_printer env evd t
+let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr)
let set_print_constr f = term_printer := f
module EvMap = Evar.Map
-let pr_evar_suggested_name evk sigma =
+let evar_suggested_name evk sigma =
let open Evd in
let base_id evk' evi =
match evar_ident evk' sigma with
@@ -143,7 +68,7 @@ let pr_existential_key sigma evk =
let open Evd in
match evar_ident evk sigma with
| None ->
- str "?" ++ Id.print (pr_evar_suggested_name evk sigma)
+ str "?" ++ Id.print (evar_suggested_name evk sigma)
| Some id ->
str "?" ++ Id.print id
@@ -164,10 +89,10 @@ 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 c) a
+let print_kconstr env sigma a =
+ protect (fun c -> print_constr_env env sigma c) a
-let pr_meta_map evd =
+let pr_meta_map env sigma =
let open Evd in
let print_constr = print_kconstr in
let pr_name = function
@@ -177,25 +102,25 @@ let pr_meta_map evd =
| (mv,Cltyp (na,b)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
- print_constr b.rebus ++ fnl ())
+ print_constr env sigma 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 ++
+ print_constr env sigma b.rebus ++
+ str " : " ++ print_constr env sigma t.rebus ++
spc () ++ pr_instance_status s ++ fnl ())
in
- prlist pr_meta_binding (meta_list evd)
+ prlist pr_meta_binding (meta_list sigma)
-let pr_decl (decl,ok) =
+let pr_decl env sigma (decl,ok) =
let open NamedDecl in
let print_constr = print_kconstr in
match decl with
- | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
- | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
- print_constr c ++ str (if ok then ")" else "}")
+ | LocalAssum ({binder_name=id},_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
+ | LocalDef ({binder_name=id},c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
+ print_constr env sigma c ++ str (if ok then ")" else "}")
-let pr_evar_source = function
+let pr_evar_source env sigma = function
| Evar_kinds.NamedHole id -> Id.print id
| Evar_kinds.QuestionMark _ -> str "underscore"
| Evar_kinds.CasesType false -> str "pattern-matching return predicate"
@@ -208,11 +133,11 @@ let pr_evar_source = function
let print_constr = print_kconstr in
let id = Option.get ido in
str "parameter " ++ Id.print id ++ spc () ++ str "of" ++
- spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c)
+ spc () ++ print_constr env sigma (EConstr.of_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 (EConstr.mkInd ind)
+ pr_nth n ++ str " argument of type " ++ print_constr env sigma (EConstr.mkInd ind)
| Evar_kinds.GoalEvar -> str "goal evar"
| Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
| Evar_kinds.MatchingVar _ -> str "matching variable"
@@ -224,7 +149,7 @@ let pr_evar_source = function
| Some Evar_kinds.Domain -> str "domain of "
| Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
-let pr_evar_info evi =
+let pr_evar_info env sigma evi =
let open Evd in
let print_constr = print_kconstr in
let phyps =
@@ -233,23 +158,23 @@ let pr_evar_info evi =
| 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)
+ prlist_with_sep spc (pr_decl env sigma) (List.rev decls)
with Invalid_argument _ -> str "Ill-formed filtered context" in
- let pty = print_constr evi.evar_concl in
+ let pty = print_constr env sigma evi.evar_concl in
let pb =
match evi.evar_body with
| Evar_empty -> mt ()
- | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ | Evar_defined c -> spc() ++ str"=> " ++ print_constr env sigma 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 "}"
+ prlist_with_sep (fun () -> str "|") (print_constr env sigma) l ++ str "}"
| _ ->
mt ()
in
- let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+ let src = str "(" ++ pr_evar_source env sigma (snd evi.evar_source) ++ str ")" in
hov 2
(str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
candidates ++ spc() ++ src)
@@ -273,8 +198,8 @@ let compute_evar_dependency_graph sigma =
let evar_dependency_closure n sigma =
let open Evd in
- (** Create the DAG of depth [n] representing the recursive dependencies of
- undefined evars. *)
+ (* 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
@@ -285,9 +210,9 @@ let evar_dependency_closure n sigma =
Evar.Set.union deps accu
with Not_found -> accu
in
- (** Consider only the newly added evars *)
+ (* Consider only the newly added evars *)
let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
- (** Merge the others *)
+ (* Merge the others *)
let accu = Evar.Set.union curr accu in
aux (n - 1) ncurr accu
in
@@ -304,8 +229,8 @@ 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 reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
+let pr_evd_level sigma = UState.pr_uctx_level (Evd.evar_universe_context sigma)
+let reference_of_level sigma l = UState.qualid_of_level (Evd.evar_universe_context sigma) l
let pr_evar_universe_context ctx =
let open UState in
@@ -321,12 +246,12 @@ let pr_evar_universe_context ctx =
str "WEAK CONSTRAINTS:"++brk(0,1)++
h 0 (UState.pr_weak prl ctx) ++ fnl ())
-let print_env_short env =
+let print_env_short env sigma =
let print_constr = print_kconstr in
let pr_rel_decl = function
- | RelDecl.LocalAssum (n,_) -> Name.print n
- | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
- ++ print_constr (EConstr.of_constr b) ++ str ")"
+ | RelDecl.LocalAssum (n,_) -> Name.print n.binder_name
+ | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n.binder_name ++ str " := "
+ ++ print_constr env sigma (EConstr.of_constr b) ++ str ")"
in
let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
let nc = List.rev (named_context env) in
@@ -337,16 +262,16 @@ let print_env_short env =
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. *)
+ (* 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_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
protect (print_constr_env env sigma) t1 ++ spc () ++
str (match pbty with
| Reduction.CONV -> "=="
@@ -355,7 +280,7 @@ let pr_evar_constraints sigma pbs =
in
prlist_with_sep fnl pr_evconstr pbs
-let pr_evar_map_gen with_univs pr_evars sigma =
+let pr_evar_map_gen with_univs pr_evars env 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 ()
@@ -365,18 +290,30 @@ let pr_evar_map_gen with_univs pr_evars sigma =
else
str "CONSTRAINTS:" ++ brk (0, 1) ++
pr_evar_constraints sigma conv_pbs ++ fnl ()
+ and typeclasses =
+ let evars = Evd.get_typeclass_evars sigma in
+ if Evar.Set.is_empty evars then mt ()
+ else
+ str "TYPECLASSES:" ++ brk (0, 1) ++
+ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
+ and obligations =
+ let evars = Evd.get_obligation_evars sigma in
+ if Evar.Set.is_empty evars then mt ()
+ else
+ str "OBLIGATIONS:" ++ brk (0, 1) ++
+ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
and metas =
if List.is_empty (Evd.meta_list sigma) then mt ()
else
- str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
+ str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
in
- evs ++ svs ++ cstrs ++ metas
+ evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
-let pr_evar_list sigma l =
+let pr_evar_list env sigma l =
let open Evd in
let pr (ev, evi) =
h 0 (Evar.print ev ++
- str "==" ++ pr_evar_info evi ++
+ str "==" ++ pr_evar_info env sigma evi ++
(if evi.evar_body == Evar_empty
then str " {" ++ pr_existential_key sigma ev ++ str "}"
else mt ()))
@@ -399,18 +336,18 @@ let to_list d =
Evd.fold fold_undef d ();
!l
-let pr_evar_by_depth depth sigma = match depth with
+let pr_evar_by_depth depth env sigma = match depth with
| None ->
(* Print all evars *)
- str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl()
+ str"EVARS:" ++ brk(0,1) ++ pr_evar_list env sigma (to_list sigma) ++ fnl()
| Some n ->
(* Print closure of undefined 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()
+ pr_evar_list env sigma (evar_dependency_closure n sigma) ++ fnl()
-let pr_evar_by_filter filter sigma =
+let pr_evar_by_filter filter env sigma =
let open Evd in
let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in
let elts = List.rev elts in
@@ -425,49 +362,49 @@ let pr_evar_by_filter filter sigma =
let prdef =
if List.is_empty defined then mt ()
else str "DEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma defined
+ pr_evar_list env sigma defined
in
let prundef =
if List.is_empty undefined then mt ()
else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
- pr_evar_list sigma undefined
+ pr_evar_list env 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 ?(with_univs=true) depth env sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth env sigma) env 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_evar_map_filter ?(with_univs=true) filter env sigma =
+ pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter env sigma) env 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
- let evd = Evd.from_env env in
+ let sigma = Evd.from_env env in
let pbody = match decl with
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
let c = EConstr.of_constr c in
- let pb = print_constr_env env evd c in
+ let pb = print_constr_env env sigma c in
(str" := " ++ pb ++ cut () ) in
- let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
+ let pt = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
let ptyp = (str" : " ++ pt) in
(Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
let pr_rel_decl env decl =
let open RelDecl in
- let evd = Evd.from_env env in
+ let sigma = Evd.from_env env in
let pbody = match decl with
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
let c = EConstr.of_constr c in
- let pb = print_constr_env env evd c in
+ let pb = print_constr_env env sigma c in
(str":=" ++ spc () ++ pb ++ spc ()) in
- let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
+ let ptyp = print_constr_env env sigma (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 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -523,9 +460,10 @@ let push_named_rec_types (lna,typarray,_) env =
let ctxt =
Array.map2_i
(fun i na t ->
- match na with
- | Name id -> LocalAssum (id, lift i t)
- | Anonymous -> anomaly (Pp.str "Fix declarations must be named."))
+ let id = map_annot (function
+ | Name id -> id
+ | Anonymous -> anomaly (Pp.str "Fix declarations must be named.")) na
+ in LocalAssum (id, lift i t))
lna typarray in
Array.fold_left
(fun e assum -> push_named assum e) env ctxt
@@ -533,14 +471,11 @@ let push_named_rec_types (lna,typarray,_) env =
let lookup_rel_id id sign =
let open RelDecl in
let rec lookrec n = function
- | [] ->
- raise Not_found
- | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
- lookrec (n + 1) l
- | LocalAssum (Name id', t) :: l ->
- if Names.Id.equal id' id then (n,None,t) else lookrec (n + 1) l
- | LocalDef (Name id', b, t) :: l ->
- if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
+ | [] -> raise Not_found
+ | decl :: l ->
+ if Names.Name.equal (Name id) (get_name decl)
+ then (n, get_value decl, get_type decl)
+ else lookrec (n+1) l
in
lookrec 1 sign
@@ -664,7 +599,7 @@ let map_constr_with_binders_left_to_right sigma g f l c =
let open EConstr in
match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
- | Construct _) -> c
+ | Construct _ | Int _) -> c
| Cast (b,k,t) ->
let b' = f l b in
let t' = f l t in
@@ -745,7 +680,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
let open EConstr in
match EConstr.kind sigma cstr with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
- | Construct _) -> cstr
+ | Construct _ | Int _) -> cstr
| Cast (c,k, t) ->
let c' = f l c in
let t' = f l t in
@@ -785,18 +720,16 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
let bl' = Array.map (f l) bl in
if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
mkCase (ci, p', c', bl')
- | Fix (ln,(lna,tl,bl)) ->
+ | Fix (ln,(lna,tl,bl as fx)) ->
let tl' = Array.map (f l) tl in
- let l' =
- Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
+ let l' = fold_rec_types g fx l in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
else mkFix (ln,(lna,tl',bl'))
- | CoFix(ln,(lna,tl,bl)) ->
+ | CoFix(ln,(lna,tl,bl as fx)) ->
let tl' = Array.map (f l) tl in
- let l' =
- Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
+ let l' = fold_rec_types g fx l in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
@@ -816,56 +749,24 @@ let map_constr_with_full_binders_user_view sigma g f =
each binder traversal; it is not recursive *)
let fold_constr_with_full_binders sigma g f n acc c =
- let open RelDecl 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
- | 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 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 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 open EConstr in
+ let f l acc c = f l acc (of_constr c) in
+ let g d l = g (of_rel_decl d) l in
+ let c = Unsafe.to_constr (whd_evar sigma c) in
+ Constr.fold_with_full_binders g 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
+ let open EConstr in
+ let f l acc c = f l acc (of_constr c) in
+ let c = Unsafe.to_constr (whd_evar sigma c) in
+ Constr.fold_constr_with_binders g 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
each binder traversal; it is not recursive and the order with which
subterms are processed is not specified *)
-let iter_constr_with_full_binders sigma g f l c =
- let open RelDecl in
- match EConstr.kind sigma c with
- | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
- | Construct _) -> ()
- | Cast (c,_, t) -> f l c; f l t
- | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
- | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
- | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
- | App (c,args) -> f l c; Array.iter (f l) args
- | Proj (p,c) -> f l c
- | Evar (_,args) -> Array.iter (f l) args
- | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
- | Fix (_,(lna,tl,bl)) ->
- let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
- Array.iter (f l) tl;
- Array.iter (f l') bl
- | CoFix (_,(lna,tl,bl)) ->
- let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
- Array.iter (f l) tl;
- Array.iter (f l') bl
+let iter_constr_with_full_binders = EConstr.iter_with_full_binders
(***************************)
(* occurs check functions *)
@@ -912,9 +813,9 @@ let occur_in_global env id constr =
let occur_var env sigma id c =
let rec 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
+ match EConstr.destRef sigma c with
+ | gr, _ -> occur_in_global env id gr
+ | exception DestKO -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -961,9 +862,7 @@ let collect_vars sigma c =
| _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
-let vars_of_global_reference env gr =
- let c, _ = Global.constr_of_global_in_context env gr in
- vars_of_global (Global.env ()) c
+let vars_of_global_reference = vars_of_global
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -1189,7 +1088,7 @@ let isGlobalRef sigma c =
| Const _ | Ind _ | Construct _ | Var _ -> true
| _ -> false
-let is_template_polymorphic env sigma f =
+let is_template_polymorphic_ind env sigma f =
match EConstr.kind sigma f with
| Ind (ind, u) ->
if not (EConstr.EInstance.is_empty u) then false
@@ -1198,7 +1097,8 @@ let is_template_polymorphic env sigma f =
let base_sort_cmp pb s0 s1 =
match (s0,s1) with
- | Prop, Prop | Set, Set | Type _, Type _ -> true
+ | SProp, SProp | Prop, Prop | Set, Set | Type _, Type _ -> true
+ | SProp, _ | _, SProp -> false
| Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
| Set, Prop | Type _, Prop | Type _, Set -> false
@@ -1452,18 +1352,15 @@ let compact_named_context sign =
let clear_named_body id env =
let open NamedDecl in
let aux _ = function
- | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
+ | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named (LocalAssum (id',t))
| d -> push_named d in
fold_named_context aux env ~init:(reset_context env)
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
+ match EConstr.destRef sigma c with
+ | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+ | exception DestKO -> EConstr.fold sigma filtrec acc c
in
filtrec Id.Set.empty constr
@@ -1520,11 +1417,9 @@ let prod_applist_assum sigma n c l =
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
-(* Combinators on judgments *)
-
-let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
-let on_judgment_value f j = { j with uj_val = f j.uj_val }
-let on_judgment_type f j = { j with uj_type = f j.uj_type }
+let on_judgment = Environ.on_judgment
+let on_judgment_value = Environ.on_judgment_value
+let on_judgment_type = Environ.on_judgment_type
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
variables skips let-in's; let-in's in the middle are put in ctx2 *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..1dd9941c5e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -17,14 +17,15 @@ open Environ
open EConstr
(** printers *)
-val print_sort : Sorts.t -> Pp.t
val pr_sort_family : Sorts.family -> Pp.t
+[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
+[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
(** about contexts *)
-val push_rel_assum : Name.t * types -> 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 push_rel_assum : Name.t Context.binder_annot * types -> env -> env
+val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
+val push_named_rec_types : Name.t Context.binder_annot array * Constr.types array * 'a -> env -> env
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
@@ -39,8 +40,8 @@ val rel_list : int -> int -> constr list
(** iterators/destructors on terms *)
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 : types -> (Name.t Context.binder_annot * types) list -> types
+val it_mkLambda : constr -> (Name.t Context.binder_annot * types) list -> 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 -> Constr.rel_context -> Constr.constr
@@ -87,6 +88,7 @@ val iter_constr_with_full_binders : Evd.evar_map ->
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> unit) -> 'a ->
constr -> unit
+[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
(**********************************************************************)
@@ -118,7 +120,9 @@ 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 -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
@@ -242,7 +246,7 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
(** other signature iterators *)
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 assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t Context.binder_annot * 't) list
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *)
@@ -280,19 +284,22 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
val isGlobalRef : Evd.evar_map -> constr -> bool
-val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
+val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
val is_Prop : Evd.evar_map -> constr -> bool
val is_Set : Evd.evar_map -> constr -> bool
val is_Type : Evd.evar_map -> constr -> bool
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
(** Combinators on judgments *)
val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment]."]
val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
(** {5 Debug pretty-printers} *)
@@ -300,13 +307,13 @@ open Evd
val pr_existential_key : evar_map -> Evar.t -> Pp.t
-val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t
+val evar_suggested_name : Evar.t -> evar_map -> Id.t
-val pr_evar_info : evar_info -> Pp.t
+val pr_evar_info : env -> evar_map -> evar_info -> Pp.t
val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t
+val pr_evar_map : ?with_univs:bool -> int option -> env -> evar_map -> Pp.t
val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
- evar_map -> Pp.t
+ env -> evar_map -> Pp.t
val pr_metaset : Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..6f4f40e2c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -12,6 +12,7 @@ open Pp
open CErrors
open Util
open Names
+open Univ
module UNameMap = Names.Id.Map
@@ -24,36 +25,43 @@ module UPairSet = UnivMinim.UPairSet
(* 2nd part used to check consistency on the fly. *)
type t =
- { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t;
- uctx_local : Univ.ContextSet.t; (** The local context of variables *)
- uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
+ { uctx_names : UnivNames.universe_binders * uinfo LMap.t;
+ uctx_local : ContextSet.t; (** The local context of variables *)
+ uctx_seff_univs : LSet.t; (** Local universes used through private constants *)
uctx_univ_variables : UnivSubst.universe_opt_subst;
(** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.LSet.t;
+ uctx_univ_algebraic : LSet.t;
(** The subset of unification variables that can be instantiated with
algebraic universes as they appear in inferred types only. *)
uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
uctx_weak_constraints : UPairSet.t
}
-
+
+let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+
let empty =
- { uctx_names = UNameMap.empty, Univ.LMap.empty;
- uctx_local = Univ.ContextSet.empty;
- uctx_seff_univs = Univ.LSet.empty;
- uctx_univ_variables = Univ.LMap.empty;
- uctx_univ_algebraic = Univ.LSet.empty;
- uctx_universes = UGraph.initial_universes;
- uctx_initial_universes = UGraph.initial_universes;
+ { uctx_names = UNameMap.empty, LMap.empty;
+ uctx_local = ContextSet.empty;
+ uctx_seff_univs = LSet.empty;
+ uctx_univ_variables = LMap.empty;
+ uctx_univ_algebraic = LSet.empty;
+ uctx_universes = initial_sprop_cumulative;
+ uctx_initial_universes = initial_sprop_cumulative;
uctx_weak_constraints = UPairSet.empty; }
+let elaboration_sprop_cumul =
+ Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+ ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
+
let make u =
+ let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
{ empty with
uctx_universes = u; uctx_initial_universes = u}
let is_empty ctx =
- Univ.ContextSet.is_empty ctx.uctx_local &&
- Univ.LMap.is_empty ctx.uctx_univ_variables
+ ContextSet.is_empty ctx.uctx_local &&
+ LMap.is_empty ctx.uctx_univ_variables
let uname_union s t =
if s == t then s
@@ -67,29 +75,29 @@ let union ctx ctx' =
if ctx == ctx' then ctx
else if is_empty ctx' then ctx
else
- let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
- let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in
+ let local = ContextSet.union ctx.uctx_local ctx'.uctx_local in
+ let seff = LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in
let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
- let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
- (Univ.ContextSet.levels ctx.uctx_local) in
- let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+ let newus = LSet.diff (ContextSet.levels ctx'.uctx_local)
+ (ContextSet.levels ctx.uctx_local) in
+ let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in
let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in
let declarenew g =
- Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+ LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
in
- let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+ let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
uctx_local = local;
uctx_seff_univs = seff;
uctx_univ_variables =
- Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
+ LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
uctx_univ_algebraic =
- Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
+ LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
uctx_initial_universes = declarenew ctx.uctx_initial_universes;
uctx_universes =
(if local == ctx.uctx_local then ctx.uctx_universes
else
- let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
+ let cstrsr = ContextSet.constraints ctx'.uctx_local in
UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
uctx_weak_constraints = weak}
@@ -97,18 +105,18 @@ let context_set ctx = ctx.uctx_local
let constraints ctx = snd ctx.uctx_local
-let context ctx = Univ.ContextSet.to_context ctx.uctx_local
+let context ctx = ContextSet.to_context ctx.uctx_local
-let const_univ_entry ~poly uctx =
+let univ_entry ~poly uctx =
let open Entries in
- if poly then Polymorphic_const_entry (context uctx)
- else Monomorphic_const_entry (context_set uctx)
+ if poly then
+ let (binders, _) = uctx.uctx_names in
+ let uctx = context uctx in
+ let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+ Polymorphic_entry (nas, uctx)
+ else Monomorphic_entry (context_set uctx)
-(* does not support cumulativity since you need more info *)
-let ind_univ_entry ~poly uctx =
- let open Entries in
- if poly then Polymorphic_ind_entry (context uctx)
- else Monomorphic_ind_entry (context_set uctx)
+let const_univ_entry = univ_entry
let of_context_set ctx = { empty with uctx_local = ctx }
@@ -124,26 +132,43 @@ let add_uctx_names ?loc s l (names, names_rev) =
if UNameMap.mem s names
then user_err ?loc ~hdr:"add_uctx_names"
Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound.");
- (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
+ (UNameMap.add s l names, LMap.add l { uname = Some s; uloc = loc } names_rev)
let add_uctx_loc l loc (names, names_rev) =
match loc with
| None -> (names, names_rev)
- | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev)
+ | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev)
let of_binders b =
let ctx = empty in
let rmap =
UNameMap.fold (fun id l rmap ->
- Univ.LMap.add l { uname = Some id; uloc = None } rmap)
- b Univ.LMap.empty
+ LMap.add l { uname = Some id; uloc = None } rmap)
+ b LMap.empty
in
{ ctx with uctx_names = b, rmap }
-let universe_binders ctx = fst ctx.uctx_names
+let invent_name (named,cnt) u =
+ let rec aux i =
+ let na = Id.of_string ("u"^(string_of_int i)) in
+ if Id.Map.mem na named then aux (i+1)
+ else Id.Map.add na u named, i+1
+ in
+ aux cnt
+
+let universe_binders ctx =
+ let named, rev = ctx.uctx_names in
+ let named, _ = LSet.fold (fun u named ->
+ match LMap.find u rev with
+ | exception Not_found -> (* not sure if possible *) invent_name named u
+ | { uname = None } -> invent_name named u
+ | { uname = Some _ } -> named)
+ (ContextSet.levels ctx.uctx_local) (named, 0)
+ in
+ named
let instantiate_variable l b v =
- try v := Univ.LMap.set l (Some b) !v
+ try v := LMap.set l (Some b) !v
with Not_found -> assert false
exception UniversesDiffer
@@ -151,7 +176,6 @@ exception UniversesDiffer
let drop_weak_constraints = ref false
let process_universe_constraints ctx cstrs =
- let open Univ in
let open UnivSubst in
let open UnivProblem in
let univs = ctx.uctx_universes in
@@ -164,14 +188,14 @@ let process_universe_constraints ctx cstrs =
| UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
| ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
in
- let is_local l = Univ.LMap.mem l !vars in
+ let is_local l = LMap.mem l !vars in
let varinfo x =
- match Univ.Universe.level x with
+ match Universe.level x with
| None -> Inl x
| Some l -> Inr l
in
let equalize_variables fo l l' r r' local =
- (** Assumes l = [l',0] and r = [r',0] *)
+ (* Assumes l = [l',0] and r = [r',0] *)
let () =
if is_local l' then
instantiate_variable l' r vars
@@ -180,27 +204,27 @@ let process_universe_constraints ctx cstrs =
else if not (UGraph.check_eq_level univs l' r') then
(* Two rigid/global levels, none of them being local,
one of them being Prop/Set, disallow *)
- if Univ.Level.is_small l' || Univ.Level.is_small r' then
- raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ if Level.is_small l' || Level.is_small r' then
+ raise (UniverseInconsistency (Eq, l, r, None))
else if fo then
raise UniversesDiffer
in
- Univ.enforce_eq_level l' r' local
+ enforce_eq_level l' r' local
in
let equalize_universes l r local = match varinfo l, varinfo r with
| Inr l', Inr r' -> equalize_variables false l l' r r' local
| Inr l, Inl r | Inl r, Inr l ->
- let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in
- let inst = Univ.univ_level_rem l r r in
+ let alg = LSet.mem l ctx.uctx_univ_algebraic in
+ let inst = univ_level_rem l r r in
if alg then (instantiate_variable l inst vars; local)
else
- let lu = Univ.Universe.make l in
- if Univ.univ_level_mem l r then
- Univ.enforce_leq inst lu local
- else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+ let lu = Universe.make l in
+ if univ_level_mem l r then
+ enforce_leq inst lu local
+ else raise (UniverseInconsistency (Eq, lu, r, None))
| Inl _, Inl _ (* both are algebraic *) ->
if UGraph.check_eq univs l r then local
- else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ else raise (UniverseInconsistency (Eq, l, r, None))
in
let unify_universes cst local =
let cst = nf_constraint cst in
@@ -209,31 +233,31 @@ let process_universe_constraints ctx cstrs =
match cst with
| ULe (l, r) ->
if UGraph.check_leq univs l r then
- (** Keep Prop/Set <= var around if var might be instantiated by prop or set
- later. *)
- match Univ.Universe.level l, Univ.Universe.level r with
+ (* Keep Prop/Set <= var around if var might be instantiated by prop or set
+ later. *)
+ match Universe.level l, Universe.level r with
| Some l, Some r ->
- Univ.Constraint.add (l, Univ.Le, r) local
+ Constraint.add (l, Le, r) local
| _ -> local
else
- begin match Univ.Universe.level r with
+ begin match Universe.level r with
| None -> user_err Pp.(str "Algebraic universe on the right")
| Some r' ->
- if Univ.Level.is_small r' then
- if not (Univ.Universe.is_levels l)
+ if Level.is_small r' then
+ if not (Universe.is_levels l)
then
- raise (Univ.UniverseInconsistency (Univ.Le, l, r, None))
+ raise (UniverseInconsistency (Le, l, r, None))
else
- let levels = Univ.Universe.levels l in
+ let levels = Universe.levels l in
let fold l' local =
- let l = Univ.Universe.make l' in
- if Univ.Level.is_small l' || is_local l' then
+ let l = Universe.make l' in
+ if Level.is_small l' || is_local l' then
equalize_variables false l l' r r' local
- else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None))
+ else raise (UniverseInconsistency (Le, l, r, None))
in
- Univ.LSet.fold fold levels local
+ LSet.fold fold levels local
else
- Univ.enforce_leq l r local
+ enforce_leq l r local
end
| ULub (l, r) ->
equalize_variables true (Universe.make l) l (Universe.make r) r local
@@ -242,26 +266,26 @@ let process_universe_constraints ctx cstrs =
| UEq (l, r) -> equalize_universes l r local
in
let local =
- UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty
+ UnivProblem.Set.fold unify_universes cstrs Constraint.empty
in
!vars, !weak, local
let add_constraints ctx cstrs =
let univs, local = ctx.uctx_local in
- let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc ->
- let l = Univ.Universe.make l and r = Univ.Universe.make r in
+ let cstrs' = Constraint.fold (fun (l,d,r) acc ->
+ let l = Universe.make l and r = Universe.make r in
let cstr' = let open UnivProblem in
match d with
- | Univ.Lt ->
- ULe (Univ.Universe.super l, r)
- | Univ.Le -> ULe (l, r)
- | Univ.Eq -> UEq (l, r)
+ | Lt ->
+ ULe (Universe.super l, r)
+ | Le -> ULe (l, r)
+ | Eq -> UEq (l, r)
in UnivProblem.Set.add cstr' acc)
cstrs UnivProblem.Set.empty
in
let vars, weak, local' = process_universe_constraints ctx cstrs' in
{ ctx with
- uctx_local = (univs, Univ.Constraint.union local local');
+ uctx_local = (univs, Constraint.union local local');
uctx_univ_variables = vars;
uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes;
uctx_weak_constraints = weak; }
@@ -273,7 +297,7 @@ let add_universe_constraints ctx cstrs =
let univs, local = ctx.uctx_local in
let vars, weak, local' = process_universe_constraints ctx cstrs in
{ ctx with
- uctx_local = (univs, Univ.Constraint.union local local');
+ uctx_local = (univs, Constraint.union local local');
uctx_univ_variables = vars;
uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes;
uctx_weak_constraints = weak; }
@@ -281,14 +305,14 @@ let add_universe_constraints ctx cstrs =
let constrain_variables diff ctx =
let univs, local = ctx.uctx_local in
let univs, vars, local =
- Univ.LSet.fold
+ LSet.fold
(fun l (univs, vars, cstrs) ->
try
- match Univ.LMap.find l vars with
+ match LMap.find l vars with
| Some u ->
- (Univ.LSet.add l univs,
- Univ.LMap.remove l vars,
- Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs)
+ (LSet.add l univs,
+ LMap.remove l vars,
+ Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs)
| None -> (univs, vars, cstrs)
with Not_found | Option.IsNone -> (univs, vars, cstrs))
diff (univs, ctx.uctx_univ_variables, local)
@@ -298,12 +322,14 @@ let constrain_variables diff ctx =
let qualid_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+ try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
with Not_found | Option.IsNone ->
UnivNames.qualid_of_level l
let pr_uctx_level uctx l =
- Libnames.pr_qualid (qualid_of_level uctx l)
+ match qualid_of_level uctx l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Level.pr l
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
@@ -312,16 +338,15 @@ type ('a, 'b) gen_universe_decl = {
univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (lident list, Univ.Constraint.t) gen_universe_decl
+ (lident list, Constraint.t) gen_universe_decl
let default_univ_decl =
{ univdecl_instance = [];
univdecl_extensible_instance = true;
- univdecl_constraints = Univ.Constraint.empty;
+ univdecl_constraints = Constraint.empty;
univdecl_extensible_constraints = true }
let error_unbound_universes left uctx =
- let open Univ in
let n = LSet.cardinal left in
let loc =
try
@@ -337,7 +362,6 @@ let error_unbound_universes left uctx =
str" unbound."))
let universe_context ~names ~extensible uctx =
- let open Univ in
let levels = ContextSet.levels uctx.uctx_local in
let newinst, left =
List.fold_right
@@ -360,7 +384,6 @@ let universe_context ~names ~extensible uctx =
let check_universe_context_set ~names ~extensible uctx =
if extensible then ()
else
- let open Univ in
let left = List.fold_left (fun left { CAst.loc; v = id } ->
let l =
try UNameMap.find id (fst uctx.uctx_names)
@@ -387,39 +410,56 @@ let check_mono_univ_decl uctx decl =
if not decl.univdecl_extensible_constraints then
check_implication uctx
decl.univdecl_constraints
- (Univ.ContextSet.constraints uctx.uctx_local);
+ (ContextSet.constraints uctx.uctx_local);
uctx.uctx_local
let check_univ_decl ~poly uctx decl =
let ctx =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
- if poly
- then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+ if poly then
+ let (binders, _) = uctx.uctx_names in
+ let uctx = universe_context ~names ~extensible uctx in
+ let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+ Entries.Polymorphic_entry (nas, uctx)
else
let () = check_universe_context_set ~names ~extensible uctx in
- Entries.Monomorphic_const_entry uctx.uctx_local
+ Entries.Monomorphic_entry uctx.uctx_local
in
if not decl.univdecl_extensible_constraints then
check_implication uctx
decl.univdecl_constraints
- (Univ.ContextSet.constraints uctx.uctx_local);
+ (ContextSet.constraints uctx.uctx_local);
ctx
+let restrict_universe_context (univs, csts) keep =
+ let removed = LSet.diff univs keep in
+ if LSet.is_empty removed then univs, csts
+ else
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.initial_universes in
+ let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in
+ let g = UGraph.merge_constraints csts g in
+ let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
+ let csts = UGraph.constraints_for ~kept:allkept g in
+ let csts = Constraint.filter (fun (l,d,r) ->
+ not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+ (LSet.inter univs keep, csts)
+
let restrict ctx vars =
- let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
- let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
+ let vars = LSet.union vars ctx.uctx_seff_univs in
+ let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
(fst ctx.uctx_names) vars
in
- let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+ let uctx' = restrict_universe_context ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }
let demote_seff_univs entry uctx =
let open Entries in
match entry.const_entry_universes with
- | Polymorphic_const_entry _ -> uctx
- | Monomorphic_const_entry (univs, _) ->
- let seff = Univ.LSet.union uctx.uctx_seff_univs univs in
+ | Polymorphic_entry _ -> uctx
+ | Monomorphic_entry (univs, _) ->
+ let seff = LSet.union uctx.uctx_seff_univs univs in
{ uctx with uctx_seff_univs = seff }
type rigid =
@@ -437,7 +477,6 @@ let univ_flexible_alg = UnivFlexible true
or defined separately. In the later case, there is no extension,
see [emit_side_effects] for example. *)
let merge ?loc ~sideff ~extend rigid uctx ctx' =
- let open Univ in
let levels = ContextSet.levels ctx' in
let uctx =
if not extend then uctx else
@@ -481,7 +520,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
uctx_initial_universes = initial }
let merge_subst uctx s =
- { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
+ { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
let emit_side_effects eff u =
let uctxs = Safe_typing.universes_of_private eff in
@@ -489,15 +528,15 @@ let emit_side_effects eff u =
let new_univ_variable ?loc rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
- let u = UnivGen.new_univ_level () in
- let ctx' = Univ.ContextSet.add_universe u ctx in
+ let u = UnivGen.fresh_level () in
+ let ctx' = ContextSet.add_universe u ctx in
let uctx', pred =
match rigid with
| UnivRigid -> uctx, true
| UnivFlexible b ->
- let uvars' = Univ.LMap.add u None uvars in
+ let uvars' = LMap.add u None uvars in
if b then {uctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = Univ.LSet.add u avars}, false
+ uctx_univ_algebraic = LSet.add u avars}, false
else {uctx with uctx_univ_variables = uvars'}, false
in
let names =
@@ -528,71 +567,80 @@ let add_global_univ uctx u =
let univs =
UGraph.add_universe u true uctx.uctx_universes
in
- { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
+ { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
uctx_initial_universes = initial;
uctx_universes = univs }
let make_flexible_variable ctx ~algebraic u =
- let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
- let uvars' = Univ.LMap.add u None uvars in
- let avars' =
- if algebraic then
- let uu = Univ.Universe.make u in
- let substu_not_alg u' v =
- Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
- in
- let has_upper_constraint () =
- Univ.Constraint.exists
- (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u)
- (Univ.ContextSet.constraints cstrs)
- in
- if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ())
- then Univ.LSet.add u avars else avars
- else avars
- in
- {ctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = avars'}
+ let {uctx_local = cstrs; uctx_univ_variables = uvars;
+ uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in
+ assert (try LMap.find u uvars == None with Not_found -> true);
+ match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with
+ | Some v ->
+ let uvars' = LMap.add u (Some (Universe.make v)) uvars in
+ { ctx with uctx_univ_variables = uvars'; }
+ | None ->
+ let uvars' = LMap.add u None uvars in
+ let avars' =
+ if algebraic then
+ let uu = Universe.make u in
+ let substu_not_alg u' v =
+ Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v
+ in
+ let has_upper_constraint () =
+ Constraint.exists
+ (fun (l,d,r) -> d == Lt && Level.equal l u)
+ (ContextSet.constraints cstrs)
+ in
+ if not (LMap.exists substu_not_alg uvars || has_upper_constraint ())
+ then LSet.add u avars else avars
+ else avars
+ in
+ {ctx with uctx_univ_variables = uvars';
+ uctx_univ_algebraic = avars'}
+
+let make_nonalgebraic_variable ctx u =
+ { ctx with uctx_univ_algebraic = LSet.remove u ctx.uctx_univ_algebraic }
let make_flexible_nonalgebraic ctx =
- {ctx with uctx_univ_algebraic = Univ.LSet.empty}
+ {ctx with uctx_univ_algebraic = LSet.empty}
let is_sort_variable uctx s =
match s with
| Sorts.Type u ->
- (match Univ.universe_level u with
+ (match universe_level u with
| Some l as x ->
- if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
+ if LSet.mem l (ContextSet.levels uctx.uctx_local) then x
else None
| None -> None)
| _ -> None
let subst_univs_context_with_def def usubst (ctx, cst) =
- (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
+ (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
let is_trivial_leq (l,d,r) =
- Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
+ Level.is_prop l && (d == Le || (d == Lt && Level.is_set r))
(* Prop < i <-> Set+1 <= i <-> Set < i *)
let translate_cstr (l,d,r as cstr) =
- let open Univ in
- if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
+ if Level.equal Level.prop l && d == Lt && not (Level.equal Level.set r) then
(Level.set, d, r)
else cstr
let refresh_constraints univs (ctx, cstrs) =
let cstrs', univs' =
- Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
+ Constraint.fold (fun c (cstrs', univs as acc) ->
let c = translate_cstr c in
if is_trivial_leq c then acc
- else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
- cstrs (Univ.Constraint.empty, univs)
+ else (Constraint.add c cstrs', UGraph.enforce_constraint c univs))
+ cstrs (Constraint.empty, univs)
in ((ctx, cstrs'), univs')
let normalize_variables uctx =
let normalized_variables, def, subst =
UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
in
- let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
+ let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.uctx_local in
let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in
subst, { uctx with uctx_local = ctx_local';
uctx_univ_variables = normalized_variables;
@@ -600,17 +648,17 @@ let normalize_variables uctx =
let abstract_undefined_variables uctx =
let vars' =
- Univ.LMap.fold (fun u v acc ->
- if v == None then Univ.LSet.remove u acc
+ LMap.fold (fun u v acc ->
+ if v == None then LSet.remove u acc
else acc)
uctx.uctx_univ_variables uctx.uctx_univ_algebraic
- in { uctx with uctx_local = Univ.ContextSet.empty;
+ in { uctx with uctx_local = ContextSet.empty;
uctx_univ_algebraic = vars' }
let fix_undefined_variables uctx =
let algs', vars' =
- Univ.LMap.fold (fun u v (algs, vars as acc) ->
- if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+ LMap.fold (fun u v (algs, vars as acc) ->
+ if v == None then (LSet.remove u algs, LMap.remove u vars)
else acc)
uctx.uctx_univ_variables
(uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
@@ -620,20 +668,20 @@ let fix_undefined_variables uctx =
let refresh_undefined_univ_variables uctx =
let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in
- let subst_fn u = Univ.subst_univs_level_level subst u in
- let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
- uctx.uctx_univ_algebraic Univ.LSet.empty
+ let subst_fn u = subst_univs_level_level subst u in
+ let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
+ uctx.uctx_univ_algebraic LSet.empty
in
let vars =
- Univ.LMap.fold
+ LMap.fold
(fun u v acc ->
- Univ.LMap.add (subst_fn u)
- (Option.map (Univ.subst_univs_level_universe subst) v) acc)
- uctx.uctx_univ_variables Univ.LMap.empty
+ LMap.add (subst_fn u)
+ (Option.map (subst_univs_level_universe subst) v) acc)
+ uctx.uctx_univ_variables LMap.empty
in
let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in
- let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
- (Univ.ContextSet.levels ctx') g in
+ let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g)
+ (ContextSet.levels ctx') g in
let initial = declare uctx.uctx_initial_universes in
let univs = declare UGraph.initial_universes in
let uctx' = {uctx_names = uctx.uctx_names;
@@ -651,7 +699,7 @@ let minimize uctx =
normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
in
- if Univ.ContextSet.equal us' uctx.uctx_local then uctx
+ if ContextSet.equal us' uctx.uctx_local then uctx
else
let us', universes =
refresh_constraints uctx.uctx_initial_universes us'
@@ -669,7 +717,7 @@ let universe_of_name uctx s =
UNameMap.find s (fst uctx.uctx_names)
let update_sigma_env uctx env =
- let univs = Environ.universes env in
+ let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
let eunivs =
{ uctx with uctx_initial_universes = univs;
uctx_universes = univs }
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..a358813825 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
primitives when needed. *)
open Names
+open Univ
exception UniversesDiffer
@@ -63,12 +64,11 @@ val constraints : t -> Univ.Constraint.t
val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
-val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
-val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
-(** Pick from {!context} or {!context_set} based on [poly].
- Cannot create cumulative entries. *)
+val const_univ_entry : poly:bool -> t -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
(** {5 Constraints handling} *)
@@ -91,6 +91,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
(** {5 Unification} *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+ the universes in [keep]. The constraints [csts] are adjusted so
+ that transitive constraints between remaining universes (those in
+ [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+ [ctx] extended by local named universes and side effect universes
+ (from [demote_seff_univs]). Transitive constraints between retained
+ universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
@@ -115,9 +125,15 @@ val add_global_univ : t -> Univ.Level.t -> t
Turn the variable [l] flexible, and algebraic if [algebraic] is true
and [l] can be. That is if there are no strict upper constraints on
[l] and and it does not appear in the instance of any non-algebraic
- universe. Otherwise the variable is just made flexible. *)
+ universe. Otherwise the variable is just made flexible.
+
+ If [l] is already algebraic it will remain so even with [algebraic:false]. *)
val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
+val make_nonalgebraic_variable : t -> Univ.Level.t -> t
+(** Make the level non algebraic. Undefined behaviour on
+ already-defined algebraics. *)
+
(** Turn all undefined flexible algebraic variables into simply flexible
ones. Can be used in case the variables might appear in universe instances
(typically for polymorphic program obligations). *)
@@ -160,7 +176,7 @@ val default_univ_decl : universe_decl
When polymorphic, the universes corresponding to
[decl.univdecl_instance] come first in the order defined by that
list. *)
-val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
@@ -171,6 +187,6 @@ val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..c310331b15 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,143 +11,81 @@
open Sorts
open Names
open Constr
-open Environ
open Univ
+type univ_unique_id = int
(* Generator of levels *)
-type universe_id = DirPath.t * int
-
let new_univ_id, set_remote_new_univ_id =
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
- ~build:(fun n -> Global.current_dirpath (), n)
+ ~build:(fun n -> n)
-let new_univ_level () =
- let dp, id = new_univ_id () in
- Univ.Level.make dp id
+let new_univ_global () =
+ Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+ Univ.Level.make (new_univ_global ())
(* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
-
-let fresh_universe_instance ctx =
- let init _ = new_univ_level () in
- Instance.of_array (Array.init (AUContext.size ctx) init)
-
-let fresh_instance_from_context ctx =
- let inst = fresh_universe_instance ctx in
- let constraints = AUContext.instantiate inst ctx in
- inst, constraints
-
-let fresh_instance ctx =
- let ctx' = ref LSet.empty in
- let init _ =
- let u = new_univ_level () in
- ctx' := LSet.add u !ctx'; u
- in
- let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
- in !ctx', inst
+let new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = sort_of_univ (new_univ ())
+
+let fresh_instance auctx =
+ let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
+ let ctx = Array.fold_right LSet.add inst LSet.empty in
+ let inst = Instance.of_array inst in
+ inst, (ctx, AUContext.instantiate inst auctx)
-let existing_instance ctx inst =
+let existing_instance ?loc auctx inst =
let () =
let len1 = Array.length (Instance.to_array inst)
- and len2 = AUContext.size ctx in
+ and len2 = AUContext.size auctx in
if not (len1 == len2) then
- CErrors.user_err ~hdr:"Universes"
- Pp.(str "Polymorphic constant expected " ++ int len2 ++
- str" levels but was given " ++ int len1)
+ CErrors.user_err ?loc ~hdr:"Universes"
+ Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
else ()
- in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
- let ctx', inst =
- match inst with
- | Some inst -> existing_instance ctx inst
- | None -> fresh_instance ctx
in
- let constraints = AUContext.instantiate inst ctx in
- inst, (ctx', constraints)
+ inst, (LSet.empty, AUContext.instantiate inst auctx)
-(** Fresh universe polymorphic construction *)
+let fresh_instance_from ?loc ctx = function
+ | Some inst -> existing_instance ?loc ctx inst
+ | None -> fresh_instance ctx
-let fresh_constant_instance env c inst =
- let cb = lookup_constant c env in
- match cb.Declarations.const_universes with
- | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_const auctx ->
- let inst, ctx =
- fresh_instance_from auctx inst
- in
- ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- ((ind,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind uactx ->
- let inst, ctx = (fresh_instance_from uactx) inst in
- ((ind,inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx =
- fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
- in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx inst in
- (((ind,i),inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
- (((ind,i),inst), ctx)
+(** Fresh universe polymorphic construction *)
open Globnames
-let fresh_global_instance ?names env gr =
- match gr with
- | VarRef id -> mkVar id, ContextSet.empty
- | ConstRef sp ->
- let c, ctx = fresh_constant_instance env sp names in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = fresh_constructor_instance env sp names in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = fresh_inductive_instance env sp names in
- mkIndU c, ctx
-
-let fresh_constant_instance env sp =
- fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp =
- fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp =
- fresh_constructor_instance env sp None
-
-let constr_of_global gr =
- let c, ctx = fresh_global_instance (Global.env ()) gr in
- if not (Univ.ContextSet.is_empty ctx) then
- if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
- (* Should be an error as we might forget constraints, allow for now
- to make firstorder work with "using" clauses *)
- c
- else CErrors.user_err ~hdr:"constr_of_global"
- Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
- str " would forget universes.")
- else c
-
-let constr_of_global_univ (gr,u) =
- match gr with
- | VarRef id -> mkVar id
- | ConstRef sp -> mkConstU (sp,u)
- | ConstructRef sp -> mkConstructU (sp,u)
- | IndRef sp -> mkIndU (sp,u)
+let fresh_global_instance ?loc ?names env gr =
+ let auctx = Environ.universes_of_global env gr in
+ let u, ctx = fresh_instance_from ?loc auctx names in
+ u, ctx
+
+let fresh_constant_instance env c =
+ let u, ctx = fresh_global_instance env (ConstRef c) in
+ (c, u), ctx
+
+let fresh_inductive_instance env ind =
+ let u, ctx = fresh_global_instance env (IndRef ind) in
+ (ind, u), ctx
+
+let fresh_constructor_instance env c =
+ let u, ctx = fresh_global_instance env (ConstructRef c) in
+ (c, u), ctx
+
+let fresh_global_instance ?loc ?names env gr =
+ let u, ctx = fresh_global_instance ?loc ?names env gr in
+ mkRef (gr, u), ctx
+
+let constr_of_monomorphic_global gr =
+ if not (Global.is_polymorphic gr) then
+ fst (fresh_global_instance (Global.env ()) gr)
+ else CErrors.user_err ~hdr:"constr_of_global"
+ Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+ str " would forget universes.")
+
+let constr_of_global gr = constr_of_monomorphic_global gr
+
+let constr_of_global_univ = mkRef
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
@@ -166,67 +104,41 @@ open Declarations
let type_of_reference env r =
match r with
| VarRef id -> Environ.named_type id env, ContextSet.empty
+
| ConstRef c ->
let cb = Environ.lookup_constant c env in
let ty = cb.const_type in
- begin
- match cb.const_universes with
- | Monomorphic_const _ -> ty, ContextSet.empty
- | Polymorphic_const auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Vars.subst_instance_constr inst ty, ctx
- end
+ let auctx = Declareops.constant_polymorphic_context cb in
+ let inst, ctx = fresh_instance auctx in
+ Vars.subst_instance_constr inst ty, ctx
+
| IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
- ty, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- end
-
- | ConstructRef cstr ->
- let (mib,oib as specif) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- end
+ let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ let ty = Inductive.type_of_inductive env (specif, inst) in
+ ty, ctx
+
+ | ConstructRef (ind,_ as cstr) ->
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ Inductive.type_of_constructor (cstr,inst) specif, ctx
let type_of_global t = type_of_reference (Global.env ()) t
let fresh_sort_in_family = function
+ | InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
| InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
- Type (Univ.Universe.make u), ContextSet.singleton u
+ sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
let new_sort_in_family sf =
fst (fresh_sort_in_family sf)
-let extend_context (a, ctx) (ctx') =
- (a, ContextSet.union ctx ctx')
+let extend_context = Univ.extend_in_context_set
let new_global_univ () =
let u = fresh_level () in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,28 +15,32 @@ open Univ
(** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
(** Side-effecting functions creating new universe levels. *)
-val new_univ_id : unit -> universe_id
-val new_univ_level : unit -> Level.t
+val new_univ_global : unit -> Level.UGlobal.t
+val fresh_level : unit -> Level.t
+
val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type : unit -> types
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_global_univ : unit -> Universe.t in_universe_context_set
val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
-val fresh_instance_from_context : AUContext.t ->
- Instance.t constrained
+val fresh_instance : AUContext.t -> Instance.t in_universe_context_set
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
Instance.t in_universe_context_set
val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +52,7 @@ val fresh_inductive_instance : env -> inductive ->
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
@@ -63,18 +67,26 @@ val fresh_universe_context_set_instance : ContextSet.t ->
val global_of_constr : constr -> GlobRef.t puniverses
val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
val extend_context : 'a in_universe_context_set -> ContextSet.t ->
'a in_universe_context_set
+[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
(** Create a fresh global in the global environment, without side effects.
- BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+ BEWARE: this raises an error on polymorphic constants/inductives:
the constraints should be properly added to an evd.
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
- the proper way to get a fresh copy of a global reference. *)
+ the proper way to get a fresh copy of a polymorphic global reference. *)
+val constr_of_monomorphic_global : GlobRef.t -> constr
+
val constr_of_global : GlobRef.t -> constr
+[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
+ use [constr_of_monomorphic_global] if the reference is guaranteed to\
+ be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
(** Returns the type of the global reference, by creating a fresh instance of polymorphic
references and computing their instantiated universe context. (side-effect on the
universe counter, use with care). *)
val type_of_global : GlobRef.t -> types in_universe_context_set
+[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index f10e6d2ec1..46ff6340b4 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -12,17 +12,12 @@ open Univ
open UnivSubst
(* To disallow minimization to Set *)
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-
-let _ =
- Goptions.(declare_bool_option
- { optdepr = false;
- optname = "minimization to Set";
- optkey = ["Universe";"Minimization";"ToSet"];
- optread = is_set_minimization;
- optwrite = (:=) set_minimization })
-
+let get_set_minimization =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~name:"minimization to Set"
+ ~key:["Universe";"Minimization";"ToSet"]
+ ~value:true
(** Simplification *)
@@ -37,15 +32,15 @@ let add_list_map u t map =
let choose_canonical ctx flexible algs s =
let global = LSet.diff s ctx in
let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
- (** If there is a global universe in the set, choose it *)
+ (* If there is a global universe in the set, choose it *)
if not (LSet.is_empty global) then
let canon = LSet.choose global in
canon, (LSet.remove canon global, rigid, flexible)
- else (** No global in the equivalence class, choose a rigid one *)
+ else (* No global in the equivalence class, choose a rigid one *)
if not (LSet.is_empty rigid) then
let canon = LSet.choose rigid in
canon, (global, LSet.remove canon rigid, flexible)
- else (** There are only flexible universes in the equivalence
+ else (* There are only flexible universes in the equivalence
class, choose a non-algebraic. *)
let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
if not (LSet.is_empty nonalgs) then
@@ -99,8 +94,8 @@ let find_inst insts v =
with Found (f,l) -> (f,l)
let compute_lbound left =
- (** The universe variable was not fixed yet.
- Compute its level using its lower bound. *)
+ (* The universe variable was not fixed yet.
+ Compute its level using its lower bound. *)
let sup l lbound =
match lbound with
| None -> Some l
@@ -159,9 +154,10 @@ let not_lower lower (d,l) =
* constraints we must keep it. *)
compare_constraint_type d d' > 0
with Not_found ->
- (** No constraint existing on l *) true) l
+ (* No constraint existing on l *) true) l
exception UpperBoundedAlg
+
(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
constraints to [lbound], adding them to [cstrs].
@@ -272,14 +268,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
module UPairs = OrderedType.UnorderedPair(Univ.Level)
module UPairSet = Set.Make (UPairs)
+(* TODO check is_small/sprop *)
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
- (** Keep the Prop/Set <= i constraints separate for minimization *)
+ (* Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
in
- let smallles = if is_set_minimization ()
- then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+ let smallles = if get_set_minimization ()
+ then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
else Constraint.empty
in
let csts, partition =
diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..7e6ed5e4c0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,17 +15,15 @@ open Univ
let qualid_of_level l =
match Level.name l with
- | Some (d, n as na) ->
- begin
- try Nametab.shortest_qualid_of_universe na
- with Not_found ->
- let name = Id.of_string_soft (string_of_int n) in
- Libnames.make_qualid d name
- end
- | None ->
- Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+ | Some qid ->
+ (try Some (Nametab.shortest_qualid_of_universe qid)
+ with Not_found -> None)
+ | None -> None
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+ match qualid_of_level l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Level.pr l
(** Global universe information outside the kernel, to handle
polymorphic universe names in sections that have to be discharged. *)
@@ -36,69 +34,24 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
let empty_binders = Id.Map.empty
-let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : Id.t list =
- try
- let l = GlobRef.Map.find ref !universe_binders_table in l
- with Not_found -> []
-
-let cache_ubinder (_,(ref,l)) =
- universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
- let ref' = fst (Globnames.subst_global subst ref) in
- if ref == ref' then orig else ref', l
-
let name_universe lvl =
- (** Best-effort naming from the string representation of the level. This is
- completely hackish and should be solved in upper layers instead. *)
+ (* Best-effort naming from the string representation of the level. This is
+ completely hackish and should be solved in upper layers instead. *)
Id.of_string_soft (Level.to_string lvl)
-let discharge_ubinder (_,(ref,l)) =
- (** Expand polymorphic binders with the section context *)
- let info = Lib.section_segment_of_reference ref in
- let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
- let map lvl = match Level.name lvl with
- | None -> (* Having Prop/Set/Var as section universes makes no sense *)
- assert false
- | Some na ->
- try
- let qid = Nametab.shortest_qualid_of_universe na in
- snd (Libnames.repr_qualid qid)
- with Not_found -> name_universe lvl
- in
- let l = List.map map sec_inst @ l in
- Some (ref, l)
-
-let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
- let open Libobject in
- declare_object { (default_object "universe binder") with
- cache_function = cache_ubinder;
- load_function = (fun _ x -> cache_ubinder x);
- classify_function = (fun x -> Substitute x);
- subst_function = subst_ubinder;
- discharge_function = discharge_ubinder;
- rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref ubinders =
- (** TODO: change the API to register a [Name.t list] instead. This is the last
- part of the code that depends on the internal representation of names in
- abstract contexts, but removing it requires quite a rework of the
- callers. *)
- let univs = AUContext.instance (Global.universes_of_global ref) in
+let compute_instance_binders inst ubinders =
let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
let map lvl =
- try LMap.find lvl revmap
- with Not_found -> name_universe lvl
+ try Name (LMap.find lvl revmap)
+ with Not_found -> Name (name_universe lvl)
in
- let ubinders = Array.map_to_list map (Instance.to_array univs) in
- if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
+ Array.map map (Instance.to_array inst)
type univ_name_list = Names.lname list
-let universe_binders_with_opt_names ref names =
- let orig = universe_binders_of_global ref in
+let universe_binders_with_opt_names orig names =
+ let orig = AUContext.names orig in
+ let orig = Array.to_list orig in
let udecl = match names with
| None -> orig
| Some udecl ->
@@ -106,11 +59,14 @@ let universe_binders_with_opt_names ref names =
List.map2 (fun orig {CAst.v = na} ->
match na with
| Anonymous -> orig
- | Name id -> id) orig udecl
+ | Name id -> Name id) orig udecl
with Invalid_argument _ ->
let len = List.length orig in
CErrors.user_err ~hdr:"universe_binders_with_opt_names"
Pp.(str "Universe instance should have length " ++ int len)
in
- let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+ let fold i acc na = match na with
+ | Name id -> Names.Id.Map.add id (Level.var i) acc
+ | Anonymous -> acc
+ in
List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index bd4062ade4..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
open Univ
val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
(** Local universe name <-> level mapping *)
@@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
-val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
type univ_name_list = Names.lname list
@@ -29,5 +29,5 @@ type univ_name_list = Names.lname list
of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
Otherwise return the bound universe names registered for [ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
+val universe_binders_with_opt_names : AUContext.t ->
univ_name_list option -> universe_binders
diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,30 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Univ
-open Constr
+let universes_of_constr = Vars.universes_of_constr
-let universes_of_constr c =
- let rec aux s c =
- match kind c with
- | Const (c, u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Sort u when not (Sorts.is_small u) ->
- let u = Sorts.univ_of_sort u in
- LSet.fold LSet.add (Universe.levels u) s
- | _ -> Constr.fold aux s c
- in aux LSet.empty c
-
-let restrict_universe_context (univs, csts) keep =
- let removed = LSet.diff univs keep in
- if LSet.is_empty removed then univs, csts
- else
- let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
- let g = UGraph.empty_universes in
- let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
- let g = UGraph.merge_constraints csts g in
- let allkept = LSet.diff allunivs removed in
- let csts = UGraph.constraints_for ~kept:allkept g in
- (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,9 +13,7 @@ open Univ
(** Return the set of all universes appearing in [constr]. *)
val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
- the universes in [keep]. The constraints [csts] are adjusted so
- that transitive constraints between remaining universes (those in
- [keep] and those not in [univs]) are preserved. *)
val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 21:41:33 +0000