aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml17
-rw-r--r--engine/eConstr.mli1
-rw-r--r--engine/evar_kinds.ml1
-rw-r--r--engine/evar_kinds.mli1
-rw-r--r--engine/evarutil.ml3
-rw-r--r--engine/evd.ml9
-rw-r--r--engine/evd.mli16
-rw-r--r--engine/logic_monad.ml2
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/proofview.ml22
-rw-r--r--engine/proofview.mli2
-rw-r--r--engine/termops.ml13
-rw-r--r--engine/uState.ml292
-rw-r--r--engine/uState.mli36
-rw-r--r--engine/univNames.ml8
-rw-r--r--engine/univNames.mli6
16 files changed, 233 insertions, 198 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 36297fe243..c29de27efb 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -127,9 +127,9 @@ let isRef sigma c = match kind sigma c with
let isRefX sigma x c =
let open GlobRef in
match x, kind sigma c with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
+ | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
+ | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i'
| VarRef id, Var id' -> Id.equal id id'
| _ -> false
@@ -452,6 +452,9 @@ let eq_universes env sigma cstrs cv_pb refargs l l' =
let open GlobRef in
let open UnivProblem in
match refargs with
+ | Some (ConstRef c, 1) when Environ.is_array_type env c ->
+ cstrs := compare_cumulative_instances cv_pb true [|Univ.Variance.Irrelevant|] l l' !cstrs;
+ true
| None | Some (ConstRef _, _) ->
cstrs := enforce_eq_instances_univs true l l' !cstrs; true
| Some (VarRef _, _) -> assert false (* variables don't have instances *)
@@ -514,7 +517,7 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
(match kind f with
- | Const (p', u) when Constant.equal (Projection.constant p) p' ->
+ | Const (p', u) when Environ.QConstant.equal env (Projection.constant p) p' ->
let npars = Projection.npars p in
if Array.length args == npars + 1 then
eqc' 0 c args.(npars)
@@ -563,6 +566,9 @@ let universes_of_constr sigma c =
| Array (u,_,_,_) ->
let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
fold sigma aux s c
+ | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+ let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
+ fold sigma aux s c
| _ -> fold sigma aux s c
in aux LSet.empty c
@@ -625,6 +631,9 @@ 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))
+let subst_univs_constr subst c =
+ of_constr (UnivSubst.subst_univs_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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index a018f4064f..882dfe2848 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -295,6 +295,7 @@ val closedn : Evd.evar_map -> int -> t -> bool
val closed0 : Evd.evar_map -> t -> bool
val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+val subst_univs_constr : Univ.universe_subst -> t -> t
val subst_of_rel_context_instance : rel_context -> t list -> t list
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 71d68f739e..fb41c4491e 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -40,6 +40,7 @@ type t =
| ImplicitArg of GlobRef.t * (int * Id.t option)
* bool (** Force inference *)
| BinderType of Name.t
+ | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
| NamedHole of Id.t (* coming from some ?[id] syntax *)
| QuestionMark of question_mark
| CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli
index ffc57cfd15..b2b39d49be 100644
--- a/engine/evar_kinds.mli
+++ b/engine/evar_kinds.mli
@@ -39,6 +39,7 @@ type t =
| ImplicitArg of GlobRef.t * (int * Id.t option)
* bool (** Force inference *)
| BinderType of Name.t
+ | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
| NamedHole of Id.t (* coming from some ?[id] syntax *)
| QuestionMark of question_mark
| CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 771571fd3f..ba6a9ea6d9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -371,7 +371,8 @@ let push_rel_decl_to_named_context
let subst = update_var id0 id subst in
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
let nc = replace_var_named_declaration id0 id nc in
- (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc)
+ let avoid = Id.Set.add id (Id.Set.add id0 avoid) in
+ (push_var id0 subst, avoid, push_named_context_val d nc)
| Some id0 when hypnaming = FailIfConflict ->
user_err Pp.(Id.print id0 ++ str " is already used.")
| _ ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 4ae1d034d7..59eea97ce9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -832,9 +832,9 @@ let empty = {
extras = Store.empty;
}
-let from_env e = { empty with universes = UState.from_env e }
+let from_env ?binders e = { empty with universes = UState.from_env ?binders e }
-let from_ctx ctx = { empty with universes = ctx }
+let from_ctx uctx = { empty with universes = uctx }
let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd =
let evd = declare_future_goal evk' evd in
(evd, evk')
+let update_source evd evk src =
+ let evar_info = EvMap.find evk evd.undf_evars in
+ let evar_info' = { evar_info with evar_source = src } in
+ { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+
(**********************************************************)
(* Accessing metas *)
diff --git a/engine/evd.mli b/engine/evd.mli
index fafaad9a04..911e00c23a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -153,12 +153,18 @@ type evar_map
val empty : evar_map
(** The empty evar map. *)
-val from_env : env -> evar_map
+val from_env : ?binders:lident list -> env -> evar_map
(** The empty evar map with given universe context, taking its initial
- universes from env. *)
+ universes from env, possibly with initial universe binders. This
+ is the main entry point at the beginning of the process of
+ interpreting a declaration (e.g. before entering the
+ interpretation of a Theorem statement). *)
val from_ctx : UState.t -> evar_map
-(** The empty evar map with given universe context *)
+(** The empty evar map with given universe context. This is the main
+ entry point when resuming from a already interpreted declaration
+ (e.g. after having interpreted a Theorem statement and preparing
+ to open a goal). *)
val is_empty : evar_map -> bool
(** Whether an evarmap is empty. *)
@@ -284,6 +290,10 @@ 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 update_source : evar_map -> Evar.t -> Evar_kinds.t located -> evar_map
+(** To update the source a posteriori, e.g. when an evar type of
+ another evar has to refer to this other evar, with a mutual dependency *)
+
val get_aliased_evars : evar_map -> Evar.t Evar.Map.t
(** The map of aliased evars *)
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4c7ed9047d..38ec668884 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -99,7 +99,7 @@ struct
let print_char = fun c -> (); fun () -> print_char c
let timeout = fun n t -> (); fun () ->
- Control.timeout n t () (Exception Tac_Timeout)
+ Control.timeout n t ()
let make f = (); fun () ->
try f ()
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 7df29c6653..7784b38c80 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -74,7 +74,7 @@ module NonLogical : sig
(** [try ... with ...] but restricted to {!Exception}. *)
val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
- val timeout : int -> 'a t -> 'a t
+ val timeout : int -> 'a t -> 'a option t
(** Construct a monadified side-effect. Exceptions raised by the argument are
wrapped with {!Exception}. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 978088872c..22863f451d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -937,22 +937,12 @@ let tclTIMEOUT n t =
Proof.get >>= fun initial ->
Proof.current >>= fun envvar ->
Proof.lift begin
- Logic_monad.NonLogical.catch
- begin
- let open Logic_monad.NonLogical in
- timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
- match r with
- | Logic_monad.Nil e -> return (Util.Inr e)
- | Logic_monad.Cons (r, _) -> return (Util.Inl r)
- end
- begin let open Logic_monad.NonLogical in function (e, info) ->
- match e with
- | Logic_monad.Tac_Timeout ->
- return (Util.Inr (Logic_monad.Tac_Timeout, info))
- | Logic_monad.TacticFailure e ->
- return (Util.Inr (e, info))
- | e -> Logic_monad.NonLogical.raise (e, info)
- end
+ let open Logic_monad.NonLogical in
+ timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
+ match r with
+ | None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null))
+ | Some (Logic_monad.Nil e) -> return (Util.Inr e)
+ | Some (Logic_monad.Cons (r, _)) -> return (Util.Inl r)
end >>= function
| Util.Inl (res,s,m,i) ->
Proof.set s >>
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 816b45984b..fe0d7ae51e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -417,7 +417,7 @@ end
val tclCHECKINTERRUPT : unit tactic
(** [tclTIMEOUT n t] can have only one success.
- In case of timeout if fails with [tclZERO Timeout]. *)
+ In case of timeout it fails with [tclZERO Tac_Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
(** [tclTIME s t] displays time for each atomic call to t, using s as an
diff --git a/engine/termops.ml b/engine/termops.ml
index 467b269e37..ccd49ca495 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -123,6 +123,13 @@ let pr_evar_source env sigma = function
str "subterm of pattern-matching return predicate"
| Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id
| Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+ | Evar_kinds.EvarType (ido,evk) ->
+ let pp = match ido with
+ | Some id -> str "?" ++ Id.print id
+ | None ->
+ try pr_existential_key sigma evk
+ with (* defined *) Not_found -> str "an internal placeholder" in
+ str "type of " ++ pp
| Evar_kinds.ImplicitArg (c,(n,ido),b) ->
let open Globnames in
let print_constr = print_kconstr in
@@ -1145,9 +1152,9 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
| Prod (_,t1,c1), Prod (_,t2,c2) ->
f Reduction.CONV t1 t2 && f cv_pb c1 c2
- | Const (c, u), Const (c', u') -> Constant.equal c c'
- | Ind (i, _), Ind (i', _) -> eq_ind i i'
- | Construct (i, _), Construct (i', _) -> eq_constructor i i'
+ | Const (c, u), Const (c', u') -> Constant.CanOrd.equal c c'
+ | Ind (i, _), Ind (i', _) -> Ind.CanOrd.equal i i'
+ | Construct (i, _), Construct (i', _) -> Construct.CanOrd.equal i i'
| _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
let constr_cmp sigma cv_pb t1 t2 =
diff --git a/engine/uState.ml b/engine/uState.ml
index 9557111cfd..0c994dfea0 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -25,8 +25,8 @@ module UPairSet = UnivMinim.UPairSet
(* 2nd part used to check consistency on the fly. *)
type t =
- { names : UnivNames.universe_binders * uinfo LMap.t;
- local : ContextSet.t; (** The local context of variables *)
+ { names : UnivNames.universe_binders * uinfo LMap.t; (** Printing/location information *)
+ local : ContextSet.t; (** The local graph of universes (variables and constraints) *)
seff_univs : LSet.t; (** Local universes used through private constants *)
univ_variables : UnivSubst.universe_opt_subst;
(** The local universes that are unification variables *)
@@ -56,18 +56,16 @@ let elaboration_sprop_cumul =
Goptions.declare_bool_option_and_ref ~depr:false
~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
-let make ~lbound u =
- let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in
+let make ~lbound univs =
+ let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) univs in
{ empty with
- universes = u;
+ universes = univs;
universes_lbound = lbound;
- initial_universes = u}
+ initial_universes = univs}
-let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e)
-
-let is_empty ctx =
- ContextSet.is_empty ctx.local &&
- LMap.is_empty ctx.univ_variables
+let is_empty uctx =
+ ContextSet.is_empty uctx.local &&
+ LMap.is_empty uctx.univ_variables
let uname_union s t =
if s == t then s
@@ -77,42 +75,42 @@ let uname_union s t =
| Some _, _ -> l
| _, _ -> r) s t
-let union ctx ctx' =
- if ctx == ctx' then ctx
- else if is_empty ctx' then ctx
+let union uctx uctx' =
+ if uctx == uctx' then uctx
+ else if is_empty uctx' then uctx
else
- let local = ContextSet.union ctx.local ctx'.local in
- let seff = LSet.union ctx.seff_univs ctx'.seff_univs in
- let names = uname_union (fst ctx.names) (fst ctx'.names) in
- let newus = LSet.diff (ContextSet.levels ctx'.local)
- (ContextSet.levels ctx.local) in
- let newus = LSet.diff newus (LMap.domain ctx.univ_variables) in
- let weak = UPairSet.union ctx.weak_constraints ctx'.weak_constraints in
+ let local = ContextSet.union uctx.local uctx'.local in
+ let seff = LSet.union uctx.seff_univs uctx'.seff_univs in
+ let names = uname_union (fst uctx.names) (fst uctx'.names) in
+ let names_rev = LMap.lunion (snd uctx.names) (snd uctx'.names) in
+ let newus = LSet.diff (ContextSet.levels uctx'.local)
+ (ContextSet.levels uctx.local) in
+ let newus = LSet.diff newus (LMap.domain uctx.univ_variables) in
+ let weak = UPairSet.union uctx.weak_constraints uctx'.weak_constraints in
let declarenew g =
- LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.universes_lbound ~strict:false g) newus g
+ LSet.fold (fun u g -> UGraph.add_universe u ~lbound:uctx.universes_lbound ~strict:false g) newus g
in
- let names_rev = LMap.lunion (snd ctx.names) (snd ctx'.names) in
{ names = (names, names_rev);
local = local;
seff_univs = seff;
univ_variables =
- LMap.subst_union ctx.univ_variables ctx'.univ_variables;
+ LMap.subst_union uctx.univ_variables uctx'.univ_variables;
univ_algebraic =
- LSet.union ctx.univ_algebraic ctx'.univ_algebraic;
- initial_universes = declarenew ctx.initial_universes;
+ LSet.union uctx.univ_algebraic uctx'.univ_algebraic;
+ initial_universes = declarenew uctx.initial_universes;
universes =
- (if local == ctx.local then ctx.universes
+ (if local == uctx.local then uctx.universes
else
- let cstrsr = ContextSet.constraints ctx'.local in
- UGraph.merge_constraints cstrsr (declarenew ctx.universes));
- universes_lbound = ctx.universes_lbound;
+ let cstrsr = ContextSet.constraints uctx'.local in
+ UGraph.merge_constraints cstrsr (declarenew uctx.universes));
+ universes_lbound = uctx.universes_lbound;
weak_constraints = weak}
-let context_set ctx = ctx.local
+let context_set uctx = uctx.local
-let constraints ctx = snd ctx.local
+let constraints uctx = snd uctx.local
-let context ctx = ContextSet.to_context ctx.local
+let context uctx = ContextSet.to_context uctx.local
let compute_instance_binders inst ubinders =
let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
@@ -131,15 +129,15 @@ let univ_entry ~poly uctx =
Polymorphic_entry (nas, uctx)
else Monomorphic_entry (context_set uctx)
-let of_context_set ctx = { empty with local = ctx }
+let of_context_set local = { empty with local }
-let subst ctx = ctx.univ_variables
+let subst uctx = uctx.univ_variables
-let ugraph ctx = ctx.universes
+let ugraph uctx = uctx.universes
-let initial_graph ctx = ctx.initial_universes
+let initial_graph uctx = uctx.initial_universes
-let algebraics ctx = ctx.univ_algebraic
+let algebraics uctx = uctx.univ_algebraic
let add_names ?loc s l (names, names_rev) =
if UNameMap.mem s names
@@ -152,14 +150,13 @@ let add_loc l loc (names, names_rev) =
| None -> (names, names_rev)
| Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev)
-let of_binders b =
- let ctx = empty in
- let rmap =
+let of_binders names =
+ let rev_map =
UNameMap.fold (fun id l rmap ->
LMap.add l { uname = Some id; uloc = None } rmap)
- b LMap.empty
+ names LMap.empty
in
- { ctx with names = b, rmap }
+ { empty with names = (names, rev_map) }
let invent_name (named,cnt) u =
let rec aux i =
@@ -169,14 +166,14 @@ let invent_name (named,cnt) u =
in
aux cnt
-let universe_binders ctx =
- let named, rev = ctx.names in
+let universe_binders uctx =
+ let named, rev = 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.local) (named, 0)
+ (ContextSet.levels uctx.local) (named, 0)
in
named
@@ -192,12 +189,12 @@ let drop_weak_constraints =
~key:["Cumulativity";"Weak";"Constraints"]
~value:false
-let process_universe_constraints ctx cstrs =
+let process_universe_constraints uctx cstrs =
let open UnivSubst in
let open UnivProblem in
- let univs = ctx.universes in
- let vars = ref ctx.univ_variables in
- let weak = ref ctx.weak_constraints in
+ let univs = uctx.universes in
+ let vars = ref uctx.univ_variables in
+ let weak = ref uctx.weak_constraints in
let normalize u = normalize_univ_variable_opt_subst !vars u in
let nf_constraint = function
| ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
@@ -231,7 +228,7 @@ let process_universe_constraints ctx cstrs =
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 = LSet.mem l ctx.univ_algebraic in
+ let alg = LSet.mem l uctx.univ_algebraic in
let inst = univ_level_rem l r r in
if alg && not (LSet.mem l (Universe.levels inst)) then
(instantiate_variable l inst vars; local)
@@ -295,8 +292,8 @@ let process_universe_constraints ctx cstrs =
in
!vars, !weak, local
-let add_constraints ctx cstrs =
- let univs, local = ctx.local in
+let add_constraints uctx cstrs =
+ let univs, old_cstrs = uctx.local 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
@@ -308,27 +305,27 @@ let add_constraints ctx cstrs =
in UnivProblem.Set.add cstr' acc)
cstrs UnivProblem.Set.empty
in
- let vars, weak, local' = process_universe_constraints ctx cstrs' in
- { ctx with
- local = (univs, Constraint.union local local');
+ let vars, weak, cstrs' = process_universe_constraints uctx cstrs' in
+ { uctx with
+ local = (univs, Constraint.union old_cstrs cstrs');
univ_variables = vars;
- universes = UGraph.merge_constraints local' ctx.universes;
+ universes = UGraph.merge_constraints cstrs' uctx.universes;
weak_constraints = weak; }
(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
-let add_universe_constraints ctx cstrs =
- let univs, local = ctx.local in
- let vars, weak, local' = process_universe_constraints ctx cstrs in
- { ctx with
+let add_universe_constraints uctx cstrs =
+ let univs, local = uctx.local in
+ let vars, weak, local' = process_universe_constraints uctx cstrs in
+ { uctx with
local = (univs, Constraint.union local local');
univ_variables = vars;
- universes = UGraph.merge_constraints local' ctx.universes;
+ universes = UGraph.merge_constraints local' uctx.universes;
weak_constraints = weak; }
-let constrain_variables diff ctx =
- let univs, local = ctx.local in
+let constrain_variables diff uctx =
+ let univs, local = uctx.local in
let univs, vars, local =
LSet.fold
(fun l (univs, vars, cstrs) ->
@@ -340,16 +337,20 @@ let constrain_variables diff ctx =
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.univ_variables, local)
+ diff (univs, uctx.univ_variables, local)
in
- { ctx with local = (univs, local); univ_variables = vars }
+ { uctx with local = (univs, local); univ_variables = vars }
-let qualid_of_level uctx =
+let id_of_level uctx l =
+ try Some (Option.get (LMap.find l (snd uctx.names)).uname)
+ with Not_found | Option.IsNone ->
+ None
+
+let qualid_of_level uctx l =
let map, map_rev = uctx.names in
- fun l ->
- try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
- with Not_found | Option.IsNone ->
- UnivNames.qualid_of_level l
+ try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
+ with Not_found | Option.IsNone ->
+ UnivNames.qualid_of_level map l
let pr_uctx_level uctx l =
match qualid_of_level uctx l with
@@ -403,8 +404,8 @@ let universe_context ~names ~extensible uctx =
let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
let inst = Array.append (Array.of_list newinst) left in
let inst = Instance.of_array inst in
- let ctx = UContext.make (inst, ContextSet.constraints uctx.local) in
- ctx
+ let uctx = UContext.make (inst, ContextSet.constraints uctx.local) in
+ uctx
let check_universe_context_set ~names ~extensible uctx =
if extensible then ()
@@ -439,27 +440,24 @@ let check_mono_univ_decl uctx decl =
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
- let (binders, _) = uctx.names in
- let uctx = universe_context ~names ~extensible uctx in
- let nas = 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_entry uctx.local
- in
if not decl.univdecl_extensible_constraints then
check_implication uctx
decl.univdecl_constraints
(ContextSet.constraints uctx.local);
- ctx
+ let names = decl.univdecl_instance in
+ let extensible = decl.univdecl_extensible_instance in
+ if poly then
+ let (binders, _) = uctx.names in
+ let uctx = universe_context ~names ~extensible uctx in
+ let nas = 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_entry uctx.local
let is_bound l lbound = match lbound with
-| UGraph.Bound.Prop -> Level.is_prop l
-| UGraph.Bound.Set -> Level.is_set l
+ | UGraph.Bound.Prop -> Level.is_prop l
+ | UGraph.Bound.Set -> Level.is_set l
let restrict_universe_context ~lbound (univs, csts) keep =
let removed = LSet.diff univs keep in
@@ -476,13 +474,13 @@ let restrict_universe_context ~lbound (univs, csts) keep =
not ((is_bound l lbound && 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 = LSet.union vars ctx.seff_univs in
+let restrict uctx vars =
+ let vars = LSet.union vars uctx.seff_univs in
let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
- (fst ctx.names) vars
+ (fst uctx.names) vars
in
- let uctx' = restrict_universe_context ~lbound:ctx.universes_lbound ctx.local vars in
- { ctx with local = uctx' }
+ let uctx' = restrict_universe_context ~lbound:uctx.universes_lbound uctx.local vars in
+ { uctx with local = uctx' }
type rigid =
| UnivRigid
@@ -498,8 +496,8 @@ let univ_flexible_alg = UnivFlexible true
context we merge comes from a side effect that is already inlined
or defined separately. In the later case, there is no extension,
see [emit_side_effects] for example. *)
-let merge ?loc ~sideff rigid uctx ctx' =
- let levels = ContextSet.levels ctx' in
+let merge ?loc ~sideff rigid uctx uctx' =
+ let levels = ContextSet.levels uctx' in
let uctx =
match rigid with
| UnivRigid -> uctx
@@ -514,7 +512,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
univ_algebraic = LSet.union uctx.univ_algebraic levels }
else { uctx with univ_variables = uvars' }
in
- let local = ContextSet.append ctx' uctx.local in
+ let local = ContextSet.append uctx' uctx.local in
let declare g =
LSet.fold (fun u g ->
try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g
@@ -534,7 +532,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
in
let initial = declare uctx.initial_universes in
let univs = declare uctx.universes in
- let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+ let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
{ uctx with names; local; universes;
initial_universes = initial }
@@ -553,19 +551,18 @@ let demote_global_univs env uctx =
ContextSet.(of_set global_univs |> add_constraints global_constraints) in
{ uctx with local = ContextSet.diff uctx.local promoted_uctx }
-let merge_seff uctx ctx' =
- let levels = ContextSet.levels ctx' in
+let merge_seff uctx uctx' =
+ let levels = ContextSet.levels uctx' in
let declare g =
LSet.fold (fun u g ->
try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g
with UGraph.AlreadyDeclared -> g)
levels g
in
- let initial = declare uctx.initial_universes in
+ let initial_universes = declare uctx.initial_universes in
let univs = declare uctx.universes in
- let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
- { uctx with universes;
- initial_universes = initial }
+ let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
+ { uctx with universes; initial_universes }
let emit_side_effects eff u =
let uctx = Safe_typing.universes_of_private eff in
@@ -581,60 +578,54 @@ let update_sigma_univs uctx ugraph =
in
merge_seff eunivs eunivs.local
-let new_univ_variable ?loc rigid name
- ({ local = ctx; univ_variables = uvars; univ_algebraic = avars} as uctx) =
- 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' = LMap.add u None uvars in
- if b then {uctx with univ_variables = uvars';
- univ_algebraic = LSet.add u avars}, false
- else {uctx with univ_variables = uvars'}, false
- in
+let add_universe ?loc name strict lbound uctx u =
+ let initial_universes = UGraph.add_universe ~lbound ~strict u uctx.initial_universes in
+ let universes = UGraph.add_universe ~lbound ~strict u uctx.universes in
+ let local = ContextSet.add_universe u uctx.local in
let names =
match name with
| Some n -> add_names ?loc n u uctx.names
| None -> add_loc u loc uctx.names
in
- let initial =
- UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u uctx.initial_universes
+ { uctx with names; local; initial_universes; universes }
+
+let new_univ_variable ?loc rigid name uctx =
+ let u = UnivGen.fresh_level () in
+ let uctx =
+ match rigid with
+ | UnivRigid -> uctx
+ | UnivFlexible allow_alg ->
+ let univ_variables = LMap.add u None uctx.univ_variables in
+ if allow_alg
+ then
+ let univ_algebraic = LSet.add u uctx.univ_algebraic in
+ { uctx with univ_variables; univ_algebraic }
+ else
+ { uctx with univ_variables }
in
- let uctx' =
- {uctx' with names = names; local = ctx';
- universes = UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false
- u uctx.universes;
- initial_universes = initial}
- in uctx', u
-
-let make_with_initial_binders ~lbound e us =
- let uctx = make ~lbound e in
+ let uctx = add_universe ?loc name false uctx.universes_lbound uctx u in
+ uctx, u
+
+let add_global_univ uctx u = add_universe None true UGraph.Bound.Set uctx u
+
+let make_with_initial_binders ~lbound univs us =
+ let uctx = make ~lbound univs in
List.fold_left
(fun uctx { CAst.loc; v = id } ->
fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
uctx us
-let add_global_univ uctx u =
- let initial =
- UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.initial_universes
- in
- let univs =
- UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.universes
- in
- { uctx with local = ContextSet.add_universe u uctx.local;
- initial_universes = initial;
- universes = univs }
+let from_env ?(binders=[]) env =
+ make_with_initial_binders ~lbound:(Environ.universes_lbound env) (Environ.universes env) binders
-let make_flexible_variable ctx ~algebraic u =
+let make_flexible_variable uctx ~algebraic u =
let {local = cstrs; univ_variables = uvars;
- univ_algebraic = avars; universes=g; } = ctx in
+ univ_algebraic = avars; universes=g; } = uctx 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 univ_variables = uvars'; }
+ { uctx with univ_variables = uvars'; }
| None ->
let uvars' = LMap.add u None uvars in
let avars' =
@@ -652,14 +643,13 @@ let make_flexible_variable ctx ~algebraic u =
then LSet.add u avars else avars
else avars
in
- {ctx with univ_variables = uvars';
- univ_algebraic = avars'}
+ { uctx with univ_variables = uvars'; univ_algebraic = avars' }
-let make_nonalgebraic_variable ctx u =
- { ctx with univ_algebraic = LSet.remove u ctx.univ_algebraic }
+let make_nonalgebraic_variable uctx u =
+ { uctx with univ_algebraic = LSet.remove u uctx.univ_algebraic }
-let make_flexible_nonalgebraic ctx =
- {ctx with univ_algebraic = LSet.empty}
+let make_flexible_nonalgebraic uctx =
+ { uctx with univ_algebraic = LSet.empty }
let is_sort_variable uctx s =
match s with
@@ -671,8 +661,8 @@ let is_sort_variable uctx s =
| None -> None)
| _ -> None
-let subst_univs_context_with_def def usubst (ctx, cst) =
- (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
+let subst_univs_context_with_def def usubst (uctx, cst) =
+ (LSet.diff uctx def, UnivSubst.subst_univs_constraints usubst cst)
let is_trivial_leq (l,d,r) =
Level.is_prop l && (d == Le || d == Lt) && Level.is_set r
@@ -696,9 +686,9 @@ let normalize_variables uctx =
let normalized_variables, def, subst =
UnivSubst.normalize_univ_variables uctx.univ_variables
in
- let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.local in
- let ctx_local', univs = refresh_constraints uctx.initial_universes ctx_local in
- subst, { uctx with local = ctx_local';
+ let uctx_local = subst_univs_context_with_def def (make_subst subst) uctx.local in
+ let uctx_local', univs = refresh_constraints uctx.initial_universes uctx_local in
+ subst, { uctx with local = uctx_local';
univ_variables = normalized_variables;
universes = univs }
diff --git a/engine/uState.mli b/engine/uState.mli
index 7fec03e3b2..442c29180c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -23,25 +23,34 @@ type t
(** {5 Constructors} *)
+(** Different ways to create a new universe state *)
+
val empty : t
val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+[@@ocaml.deprecated "Use from_env"]
val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+[@@ocaml.deprecated "Use from_env"]
-val from_env : Environ.env -> t
-
-val is_empty : t -> bool
+val from_env : ?binders:lident list -> Environ.env -> t
+(** Main entry point at the beginning of a declaration declaring the
+ binding names as rigid universes. *)
-val union : t -> t -> t
+val of_binders : UnivNames.universe_binders -> t
+(** Main entry point when only names matter, e.g. for printing. *)
val of_context_set : Univ.ContextSet.t -> t
+(** Main entry point when starting from the instance of a global
+ reference, e.g. when building a scheme. *)
-val of_binders : UnivNames.universe_binders -> t
+(** Misc *)
-val universe_binders : t -> UnivNames.universe_binders
+val is_empty : t -> bool
+
+val union : t -> t -> t
-(** {5 Projections} *)
+(** {5 Projections and other destructors} *)
val context_set : t -> Univ.ContextSet.t
(** The local context of the state, i.e. a set of bound variables together
@@ -69,6 +78,9 @@ val context : t -> Univ.UContext.t
val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
+val universe_binders : t -> UnivNames.universe_binders
+(** Return names of universes, inventing names if needed *)
+
(** {5 Constraints handling} *)
val add_constraints : t -> Univ.Constraint.t -> t
@@ -115,7 +127,7 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
val demote_global_univs : Environ.env -> t -> t
(** Removes from the uctx_local part of the UState the universes and constraints
that are present in the universe graph in the input env (supposedly the
- global ones *)
+ global ones) *)
val demote_seff_univs : Univ.LSet.t -> t -> t
(** Mark the universes as not local any more, because they have been
@@ -123,6 +135,11 @@ val demote_seff_univs : Univ.LSet.t -> t -> t
emit_side_effects instead. *)
val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
+(** Declare a new local universe; use rigid if a global or bound
+ universe; use flexible for a universe existential variable; use
+ univ_flexible_alg for a universe existential variable allowed to
+ be instantiated with an algebraic universe *)
+
val add_global_univ : t -> Univ.Level.t -> t
(** [make_flexible_variable g algebraic l]
@@ -192,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
+(** Only looks in the local names, not in the nametab. *)
+val id_of_level : t -> Univ.Level.t -> Id.t option
+
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 2e15558db2..f5542cc0f7 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -12,15 +12,15 @@ open Names
open Univ
-let qualid_of_level l =
+let qualid_of_level ctx l =
match Level.name l with
| Some qid ->
- (try Some (Nametab.shortest_qualid_of_universe qid)
+ (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
with Not_found -> None)
| None -> None
-let pr_with_global_universes l =
- match qualid_of_level l with
+let pr_with_global_universes ctx l =
+ match qualid_of_level ctx l with
| Some qid -> Libnames.pr_qualid qid
| None -> Level.pr l
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 5f69d199b3..875c043032 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -10,9 +10,6 @@
open Univ
-val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid option
-
(** Local universe name <-> level mapping *)
type universe_binders = Univ.Level.t Names.Id.Map.t
@@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
type univ_name_list = Names.lname list
+
+val pr_with_global_universes : universe_binders -> Level.t -> Pp.t
+val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:18:39 +0000