aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml24
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml6
-rw-r--r--engine/evarutil.mli1
-rw-r--r--engine/evd.ml5
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/namegen.ml3
-rw-r--r--engine/proofview.ml14
-rw-r--r--engine/proofview.mli17
-rw-r--r--engine/proofview_monad.ml9
-rw-r--r--engine/proofview_monad.mli2
-rw-r--r--engine/termops.ml16
-rw-r--r--engine/termops.mli5
-rw-r--r--engine/uState.ml248
-rw-r--r--engine/uState.mli9
15 files changed, 185 insertions, 184 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 24d161d00a..8756ebfdf2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -73,6 +73,7 @@ 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 mkInt i = of_kind (Int i)
let mkRef (gr,u) = let open GlobRef in match gr with
| ConstRef c -> mkConstU (c,u)
@@ -81,6 +82,7 @@ let mkRef (gr,u) = let open GlobRef in match gr with
| VarRef x -> mkVar x
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
@@ -328,7 +330,7 @@ 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
@@ -403,25 +405,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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 49cbc4d7e5..2f4cf7d5d0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -124,10 +124,12 @@ 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 mkInt : Uint63.t -> t
val mkRef : GlobRef.t * EInstance.t -> 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
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index db56d0628f..d70c009c6d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -337,6 +337,7 @@ type naming_mode =
| KeepUserNameAndRenameExistingEvenSectionNames
| KeepExistingNames
| FailIfConflict
+ | ProgramNaming
let push_rel_decl_to_named_context
?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
@@ -364,7 +365,7 @@ 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 *)
@@ -372,7 +373,8 @@ let push_rel_decl_to_named_context
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
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 0e67475778..23b240f1a0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -38,6 +38,7 @@ type naming_mode =
| KeepUserNameAndRenameExistingEvenSectionNames
| KeepExistingNames
| FailIfConflict
+ | ProgramNaming
val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
diff --git a/engine/evd.ml b/engine/evd.ml
index eee2cb700c..f0433d3387 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -852,8 +852,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
diff --git a/engine/evd.mli b/engine/evd.mli
index de73144895..d2d18ca486 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -597,12 +597,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
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 018eca1ba2..294b61fd3d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
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
+ | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
in
hdrec c
@@ -163,6 +163,7 @@ let hdchar env sigma c =
lowercase_first_char id
| Evar _ (* We could do better... *)
| Meta _ | Case (_, _, _, _) -> "y"
+ | Int _ -> "i"
in
hdrec 0 c
diff --git a/engine/proofview.ml b/engine/proofview.ml
index cf4224bbdb..a725444e81 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
@@ -223,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)
@@ -993,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} *)
@@ -1275,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 286703c0dc..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} *)
@@ -407,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
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 69341d97df..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -177,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
@@ -254,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 a08cab3bf6..3437b6ce77 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -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 137770d8f0..2f766afaa6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -38,7 +38,7 @@ 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
@@ -67,7 +67,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
@@ -600,7 +600,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
@@ -681,7 +681,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
@@ -1417,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 7920af8e0e..dea59e9efc 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -295,8 +295,11 @@ 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} *)
@@ -304,7 +307,7 @@ 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 : env -> evar_map -> evar_info -> Pp.t
val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
diff --git a/engine/uState.ml b/engine/uState.ml
index 6969d2ba44..77d1896683 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,12 +25,12 @@ 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 *)
@@ -38,11 +39,11 @@ type t =
}
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_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 = UGraph.initial_universes;
uctx_initial_universes = UGraph.initial_universes;
uctx_weak_constraints = UPairSet.empty; }
@@ -52,8 +53,8 @@ let make u =
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 +68,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,26 +98,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
let (binders, _) = uctx.uctx_names in
let uctx = context uctx in
- let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
- Polymorphic_const_entry (nas, uctx)
- else Monomorphic_const_entry (context_set uctx)
+ 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
- let (binders, _) = uctx.uctx_names in
- let uctx = context uctx in
- let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
- Polymorphic_ind_entry (nas, uctx)
- else Monomorphic_ind_entry (context_set uctx)
+let const_univ_entry = univ_entry
let of_context_set ctx = { empty with uctx_local = ctx }
@@ -132,19 +125,19 @@ 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 }
@@ -157,7 +150,6 @@ let invent_name (named,cnt) u =
aux cnt
let universe_binders ctx =
- let open Univ in
let named, rev = ctx.uctx_names in
let named, _ = LSet.fold (fun u named ->
match LMap.find u rev with
@@ -169,7 +161,7 @@ let universe_binders ctx =
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
@@ -177,7 +169,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
@@ -190,9 +181,9 @@ 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
@@ -206,27 +197,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
@@ -237,29 +228,29 @@ let process_universe_constraints ctx cstrs =
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
+ 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
@@ -268,26 +259,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; }
@@ -299,7 +290,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; }
@@ -307,14 +298,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)
@@ -324,14 +315,14 @@ let constrain_variables diff ctx =
let qualid_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Some (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 =
match qualid_of_level uctx l with
| Some qid -> Libnames.pr_qualid qid
- | None -> Univ.Level.pr l
+ | None -> Level.pr l
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
@@ -340,16 +331,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
@@ -365,7 +355,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
@@ -388,7 +377,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)
@@ -415,7 +403,7 @@ 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 =
@@ -425,20 +413,19 @@ let check_univ_decl ~poly uctx decl =
if poly then
let (binders, _) = uctx.uctx_names in
let uctx = universe_context ~names ~extensible uctx in
- let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in
- Entries.Polymorphic_const_entry (nas, uctx)
+ 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 open Univ in
let removed = LSet.diff univs keep in
if LSet.is_empty removed then univs, csts
else
@@ -453,8 +440,8 @@ let restrict_universe_context (univs, csts) keep =
(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' = restrict_universe_context ctx.uctx_local vars in
@@ -463,9 +450,9 @@ let restrict ctx vars =
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 =
@@ -483,7 +470,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
@@ -527,7 +513,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
@@ -536,14 +522,14 @@ 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.fresh_level () in
- let ctx' = Univ.ContextSet.add_universe u ctx 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 =
@@ -574,12 +560,11 @@ 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 open Univ in
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);
@@ -608,48 +593,47 @@ let make_flexible_variable ctx ~algebraic u =
uctx_univ_algebraic = avars'}
let make_nonalgebraic_variable ctx u =
- { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic }
+ { 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;
@@ -657,17 +641,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)
@@ -677,20 +661,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;
@@ -708,7 +692,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'
diff --git a/engine/uState.mli b/engine/uState.mli
index 5170184ef4..a358813825 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -64,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} *)
@@ -177,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:08:44 +0000