aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml3
-rw-r--r--engine/eConstr.mli1
-rw-r--r--engine/evarutil.ml30
-rw-r--r--engine/evarutil.mli17
-rw-r--r--engine/evd.ml15
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/logic_monad.ml7
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/namegen.ml3
-rw-r--r--engine/proofview.ml24
-rw-r--r--engine/proofview.mli15
-rw-r--r--engine/termops.ml4
-rw-r--r--engine/uState.ml151
-rw-r--r--engine/uState.mli17
-rw-r--r--engine/univGen.ml8
-rw-r--r--engine/univGen.mli3
-rw-r--r--engine/univMinim.ml10
-rw-r--r--engine/univMinim.mli2
-rw-r--r--engine/univops.mli2
19 files changed, 182 insertions, 136 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 23d066df58..46a80239cf 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c))
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 mkFloat f = of_kind (Float f)
let mkRef (gr,u) = let open GlobRef in match gr with
| ConstRef c -> mkConstU (c,u)
@@ -334,7 +335,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 _ | Int _) -> ()
+ | Construct _ | Int _ | Float _) -> ()
| 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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2afce38db7..90f50b764c 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> Sorts.relevance -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
+val mkFloat : Float64.t -> t
val mkRef : GlobRef.t * EInstance.t -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ea71be8e43..5444d88e47 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -661,26 +661,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
(* spiwack: a few functions to gather evars on which goals depend. *)
let queue_set q is_dependent set =
Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term evm q is_dependent c =
- queue_set q is_dependent (evars_of_term evm c)
+let queue_term q is_dependent c =
+ queue_set q is_dependent (evar_nodes_of_term c)
let process_dependent_evar q acc evm is_dependent e =
let evi = Evd.find evm e in
(* Queues evars appearing in the types of the goal (conclusion, then
hypotheses), they are all dependent. *)
- queue_term evm q true evi.evar_concl;
+ queue_term q true evi.evar_concl;
List.iter begin fun decl ->
let open NamedDecl in
- queue_term evm q true (NamedDecl.get_type decl);
+ queue_term q true (NamedDecl.get_type decl);
match decl with
| LocalAssum _ -> ()
- | LocalDef (_,b,_) -> queue_term evm q true b
+ | LocalDef (_,b,_) -> queue_term q true b
end (EConstr.named_context_of_val evi.evar_hyps);
match evi.evar_body with
| Evar_empty ->
if is_dependent then Evar.Map.add e None acc else acc
| Evar_defined b ->
- let subevars = evars_of_term evm b in
+ let subevars = evar_nodes_of_term b in
(* evars appearing in the definition of an evar [e] are marked
as dependent when [e] is dependent itself: if [e] is a
non-dependent goal, then, unless they are reach from another
@@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' =
in
Evd.add_universe_constraints evd soft
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extension of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+ [t] and [u] up to existential variable instantiation and
+ equalisable universes. The term [t] is interpreted in [evd] while
+ [u] is interpreted in [extended_evd]. The universe constraints in
+ [extended_evd] are assumed to be an extension of those in [evd]. *)
+let eq_constr_univs_test ~evd ~extended_evd t u =
(* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
let open Evd in
let t = EConstr.Unsafe.to_constr t
@@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u =
in
let ans =
UnivProblem.eq_constr_univs_infer_with
- (fun t -> kind_of_term_upto sigma1 t)
- (fun u -> kind_of_term_upto sigma2 u)
- (universes sigma2) fold t u sigma2
+ (fun t -> kind_of_term_upto evd t)
+ (fun u -> kind_of_term_upto extended_evd u)
+ (universes extended_evd) fold t u extended_evd
in
match ans with None -> false | Some _ -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e9d579af32..7877b94582 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
val kind_of_term_upto : evar_map -> Constr.constr ->
(Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extension of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+ [t] and [u] up to existential variable instantiation and
+ equalisable universes. The term [t] is interpreted in [evd] while
+ [u] is interpreted in [extended_evd]. The universe constraints in
+ [extended_evd] are assumed to be an extension of those in [evd]. *)
+val eq_constr_univs_test :
+ evd:Evd.evar_map ->
+ extended_evd:Evd.evar_map ->
+ constr ->
+ constr ->
+ bool
(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
[Inl sigma'] where [sigma'] is [sigma] augmented with universe
diff --git a/engine/evd.ml b/engine/evd.ml
index b621a3fe2f..f051334f69 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -702,7 +702,7 @@ let empty = {
}
let from_env e =
- { empty with universes = UState.make (Environ.universes e) }
+ { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
let from_ctx ctx = { empty with universes = ctx }
@@ -864,7 +864,7 @@ let universe_subst evd =
UState.subst evd.universes
let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
- {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
+ {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
let merge_universe_subst evd subst =
{evd with universes = UState.merge_subst evd.universes subst }
@@ -1403,7 +1403,16 @@ end
let evars_of_term evd c =
let rec evrec acc c =
- match MiniEConstr.kind evd c with
+ let c = MiniEConstr.whd_evar evd c in
+ match kind c with
+ | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | _ -> Constr.fold evrec acc c
+ in
+ evrec Evar.Set.empty c
+
+let evar_nodes_of_term c =
+ let rec evrec acc c =
+ match kind c with
| Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
| _ -> Constr.fold evrec acc c
in
diff --git a/engine/evd.mli b/engine/evd.mli
index 132f7bc745..5ab53947f7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
val evars_of_term : evar_map -> econstr -> Evar.Set.t
(** including evars in instances of evars *)
+val evar_nodes_of_term : econstr -> Evar.Set.t
+ (** same as evars_of_term but also including defined evars.
+ For use in printing dependent evars *)
+
val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 7c06bb59f1..3c383b2e00 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -30,7 +30,7 @@
exception Exception of exn
(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
@@ -38,7 +38,6 @@ exception Timeout
exception TacticFailure of exn
let _ = CErrors.register_handler begin function
- | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
| Exception e -> CErrors.print e
| TacticFailure e -> CErrors.print e
| _ -> raise CErrors.Unhandled
@@ -99,7 +98,7 @@ struct
let print_char = fun c -> (); fun () -> print_char c
let timeout = fun n t -> (); fun () ->
- Control.timeout n t () (Exception Timeout)
+ Control.timeout n t () (Exception Tac_Timeout)
let make f = (); fun () ->
try f ()
@@ -108,7 +107,7 @@ struct
Util.iraise (Exception e, info)
(** Use the current logger. The buffer is also flushed. *)
- let print_debug s = make (fun _ -> Feedback.msg_info s)
+ let print_debug s = make (fun _ -> Feedback.msg_debug s)
let print_info s = make (fun _ -> Feedback.msg_info s)
let print_warning s = make (fun _ -> Feedback.msg_warning s)
let print_notice s = make (fun _ -> Feedback.msg_notice s)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 90c920439a..75920455ce 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -30,7 +30,7 @@
exception Exception of exn
(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 89c2fade62..b850f38b4d 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).binder_name with Name id -> id | _ -> assert false)
- | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
+ | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
in
hdrec c
@@ -165,6 +165,7 @@ let hdchar env sigma c =
| Evar _ (* We could do better... *)
| Meta _ | Case (_, _, _, _) -> "y"
| Int _ -> "i"
+ | Float _ -> "f"
in
hdrec 0 c
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8b5bd4cd80..d6f5aab1d1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -849,7 +849,8 @@ let give_up =
module Progress = struct
- let eq_constr = Evarutil.eq_constr_univs_test
+ let eq_constr evd extended_evd =
+ Evarutil.eq_constr_univs_test ~evd ~extended_evd
(** equality function on hypothesis contexts *)
let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -879,10 +880,10 @@ module Progress = struct
eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
(** Equality function on goals *)
- let goal_equal evars1 gl1 evars2 gl2 =
- let evi1 = Evd.find evars1 gl1 in
- let evi2 = Evd.find evars2 gl2 in
- eq_evar_info evars1 evars2 evi1 evi2
+ let goal_equal ~evd ~extended_evd evar extended_evar =
+ let evi = Evd.find evd evar in
+ let extended_evi = Evd.find extended_evd extended_evar in
+ eq_evar_info evd extended_evd evi extended_evi
end
@@ -899,17 +900,17 @@ let tclPROGRESS t =
let test =
quick_test ||
Util.List.for_all2eq begin fun i f ->
- Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
+ Progress.goal_equal ~evd:initial.solution
+ ~extended_evd:final.solution (drop_state i) (drop_state f)
end initial.comb final.comb
in
if not test then
tclUNIT res
else
- tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+ tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
-exception Timeout
let _ = CErrors.register_handler begin function
- | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+ | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
| _ -> raise CErrors.Unhandled
end
@@ -934,7 +935,8 @@ let tclTIMEOUT n t =
end
begin let open Logic_monad.NonLogical in function (e, info) ->
match e with
- | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+ | 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 ~info e
@@ -1245,7 +1247,7 @@ module V82 = struct
let top_evars initial { solution=sigma; } =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evd.evars_of_term sigma c)
+ Evar.Set.elements (Evd.evar_nodes_of_term c)
in
CList.flatten (CList.map evars_of_initial initial)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index f90f02f3e1..764a4a0058 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,14 +398,23 @@ val give_up : unit tactic
val tclPROGRESS : 'a tactic -> 'a tactic
module Progress : sig
- val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether
+ the [evar_info] from [evd] corresponding to [evar] is equal to that
+ from [extended_evd] corresponding to [extended_evar], up to
+ existential variable instantiation and equalisable universes. The
+ universe constraints in [extended_evd] are assumed to be an
+ extension of the universe constraints in [evd]. *)
+ val goal_equal :
+ evd:Evd.evar_map ->
+ extended_evd:Evd.evar_map ->
+ Evar.t ->
+ Evar.t ->
+ bool
end
(** Checks for interrupts *)
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
diff --git a/engine/termops.ml b/engine/termops.ml
index 2ab2f60421..90fa8546ce 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -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 _ | Int _) -> c
+ | Construct _ | Int _ | Float _) -> 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 _ | Int _) -> cstr
+ | Construct _ | Int _ | Float _) -> cstr
| Cast (c,k, t) ->
let c' = f l c in
let t' = f l t in
diff --git a/engine/uState.ml b/engine/uState.ml
index 5ed016e0d0..ba17cdde93 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,6 +34,7 @@ type 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_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
uctx_weak_constraints : UPairSet.t
}
@@ -47,6 +48,7 @@ let empty =
uctx_univ_variables = LMap.empty;
uctx_univ_algebraic = LSet.empty;
uctx_universes = initial_sprop_cumulative;
+ uctx_universes_lbound = Univ.Level.set;
uctx_initial_universes = initial_sprop_cumulative;
uctx_weak_constraints = UPairSet.empty; }
@@ -54,10 +56,12 @@ 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 make ~lbound 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}
+ { empty with
+ uctx_universes = u;
+ uctx_universes_lbound = lbound;
+ uctx_initial_universes = u}
let is_empty ctx =
ContextSet.is_empty ctx.uctx_local &&
@@ -83,7 +87,7 @@ let union ctx ctx' =
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 =
- LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+ LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g
in
let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
@@ -99,6 +103,7 @@ let union ctx ctx' =
else
let cstrsr = ContextSet.constraints ctx'.uctx_local in
UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
+ uctx_universes_lbound = ctx.uctx_universes_lbound;
uctx_weak_constraints = weak}
let context_set ctx = ctx.uctx_local
@@ -173,6 +178,7 @@ exception UniversesDiffer
let drop_weak_constraints = ref false
+
let process_universe_constraints ctx cstrs =
let open UnivSubst in
let open UnivProblem in
@@ -231,22 +237,21 @@ let process_universe_constraints ctx cstrs =
else
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 Universe.level l, Universe.level r with
- | Some l, Some r ->
- Constraint.add (l, Le, r) local
- | _ -> local
- else
- begin match Universe.level r with
- | None -> user_err Pp.(str "Algebraic universe on the right")
- | Some r' ->
- if Level.is_small r' then
+ begin match Univ.Universe.level r with
+ | None ->
+ if UGraph.check_leq univs l r then local
+ else user_err Pp.(str "Algebraic universe on the right")
+ | Some r' ->
+ if Level.is_small r' then
if not (Universe.is_levels l)
- then
+ then (* l contains a +1 and r=r' small so l <= r impossible *)
raise (UniverseInconsistency (Le, l, r, None))
else
+ if UGraph.check_leq univs l r then match Univ.Universe.level l with
+ | Some l ->
+ Univ.Constraint.add (l, Le, r') local
+ | None -> local
+ else
let levels = Universe.levels l in
let fold l' local =
let l = Universe.make l' in
@@ -255,8 +260,12 @@ let process_universe_constraints ctx cstrs =
else raise (UniverseInconsistency (Le, l, r, None))
in
LSet.fold fold levels local
- else
- enforce_leq l r local
+ else
+ match Univ.Universe.level l with
+ | Some l ->
+ Univ.Constraint.add (l, Le, r') local
+ | None ->
+ if UGraph.check_leq univs l r then local else enforce_leq l r local
end
| ULub (l, r) ->
equalize_variables true (Universe.make l) l (Universe.make r) r local
@@ -431,18 +440,19 @@ let check_univ_decl ~poly uctx decl =
(ContextSet.constraints uctx.uctx_local);
ctx
-let restrict_universe_context (univs, csts) keep =
+let restrict_universe_context ~lbound (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 = LSet.fold (fun v g -> if Level.is_small v then g else
+ UGraph.add_universe v ~lbound ~strict: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
+ not ((Level.equal 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 =
@@ -450,17 +460,9 @@ let restrict ctx vars =
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
+ let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }
-let demote_seff_univs universes uctx =
- let open Entries in
- match universes with
- | Polymorphic_entry _ -> uctx
- | Monomorphic_entry (univs, _) ->
- let seff = LSet.union uctx.uctx_seff_univs univs in
- { uctx with uctx_seff_univs = seff }
-
type rigid =
| UnivRigid
| UnivFlexible of bool (** Is substitution by an algebraic ok? *)
@@ -475,10 +477,9 @@ 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 ~extend rigid uctx ctx' =
+let merge ?loc ~sideff rigid uctx ctx' =
let levels = ContextSet.levels ctx' in
let uctx =
- if not extend then uctx else
match rigid with
| UnivRigid -> uctx
| UnivFlexible b ->
@@ -487,25 +488,23 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
else LMap.add u None accu
in
let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
- if b then
- { uctx with uctx_univ_variables = uvars';
- uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
- else { uctx with uctx_univ_variables = uvars' }
+ if b then
+ { uctx with uctx_univ_variables = uvars';
+ uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
+ else { uctx with uctx_univ_variables = uvars' }
in
- let uctx_local =
- if not extend then uctx.uctx_local
- else ContextSet.append ctx' uctx.uctx_local in
+ let uctx_local = ContextSet.append ctx' uctx.uctx_local in
let declare g =
LSet.fold (fun u g ->
- try UGraph.add_universe u false g
- with UGraph.AlreadyDeclared when sideff -> g)
- levels g
+ try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+ with UGraph.AlreadyDeclared when sideff -> g)
+ levels g
in
let uctx_names =
let fold u accu =
let modify _ info = match info.uloc with
- | None -> { info with uloc = loc }
- | Some _ -> info
+ | None -> { info with uloc = loc }
+ | Some _ -> info
in
try LMap.modify u modify accu
with Not_found -> LMap.add u { uname = None; uloc = loc } accu
@@ -521,9 +520,36 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
let merge_subst uctx s =
{ uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
+let demote_seff_univs univs uctx =
+ let seff = LSet.union uctx.uctx_seff_univs univs in
+ { uctx with uctx_seff_univs = seff }
+
+let merge_seff uctx ctx' =
+ let levels = ContextSet.levels ctx' in
+ let declare g =
+ LSet.fold (fun u g ->
+ try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+ with UGraph.AlreadyDeclared -> g)
+ levels g
+ in
+ let initial = declare uctx.uctx_initial_universes in
+ let univs = declare uctx.uctx_universes in
+ let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+ { uctx with uctx_universes;
+ uctx_initial_universes = initial }
+
let emit_side_effects eff u =
- let uctxs = Safe_typing.universes_of_private eff in
- List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
+ let uctx = Safe_typing.universes_of_private eff in
+ let u = demote_seff_univs (fst uctx) u in
+ merge_seff u uctx
+
+let update_sigma_env uctx env =
+ let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
+ let eunivs =
+ { uctx with uctx_initial_universes = univs;
+ uctx_universes = univs }
+ in
+ merge_seff eunivs eunivs.uctx_local
let new_univ_variable ?loc rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
@@ -544,16 +570,17 @@ let new_univ_variable ?loc rigid name
| None -> add_uctx_loc u loc uctx.uctx_names
in
let initial =
- UGraph.add_universe u false uctx.uctx_initial_universes
+ UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes
in
let uctx' =
{uctx' with uctx_names = names; uctx_local = ctx';
- uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+ uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false
+ u uctx.uctx_universes;
uctx_initial_universes = initial}
in uctx', u
-let make_with_initial_binders e us =
- let uctx = make e in
+let make_with_initial_binders ~lbound e us =
+ let uctx = make ~lbound e in
List.fold_left
(fun uctx { CAst.loc; v = id } ->
fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
@@ -561,10 +588,10 @@ let make_with_initial_binders e us =
let add_global_univ uctx u =
let initial =
- UGraph.add_universe u true uctx.uctx_initial_universes
+ UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
in
let univs =
- UGraph.add_universe u true uctx.uctx_universes
+ UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
in
{ uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
uctx_initial_universes = initial;
@@ -679,8 +706,9 @@ let refresh_undefined_univ_variables uctx =
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 = LSet.fold (fun u g -> UGraph.add_universe u false g)
- (ContextSet.levels ctx') g in
+ let lbound = uctx.uctx_universes_lbound in
+ let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict: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;
@@ -688,14 +716,16 @@ let refresh_undefined_univ_variables uctx =
uctx_seff_univs = uctx.uctx_seff_univs;
uctx_univ_variables = vars; uctx_univ_algebraic = alg;
uctx_universes = univs;
+ uctx_universes_lbound = lbound;
uctx_initial_universes = initial;
uctx_weak_constraints = weak; } in
uctx', subst
let minimize uctx =
let open UnivMinim in
+ let lbound = uctx.uctx_universes_lbound in
let ((vars',algs'), us') =
- normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
+ normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
in
if ContextSet.equal us' uctx.uctx_local then uctx
@@ -709,20 +739,13 @@ let minimize uctx =
uctx_univ_variables = vars';
uctx_univ_algebraic = algs';
uctx_universes = universes;
+ uctx_universes_lbound = lbound;
uctx_initial_universes = uctx.uctx_initial_universes;
uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
let universe_of_name uctx s =
UNameMap.find s (fst uctx.uctx_names)
-let update_sigma_env uctx env =
- let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
- let eunivs =
- { uctx with uctx_initial_universes = univs;
- uctx_universes = univs }
- in
- merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
-
let pr_weak prl {uctx_weak_constraints=weak} =
let open Pp in
prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
diff --git a/engine/uState.mli b/engine/uState.mli
index 9689f2e961..23ef84c55d 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
val empty : t
-val make : UGraph.t -> t
+val make : lbound:Univ.Level.t -> UGraph.t -> t
-val make_with_initial_binders : UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
val is_empty : t -> bool
@@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
(** {5 Unification} *)
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context lbound (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
+val restrict_universe_context : lbound:Univ.Level.t -> 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
@@ -100,8 +100,6 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
-val demote_seff_univs : Entries.universes_entry -> t -> t
-
type rigid =
| UnivRigid
| UnivFlexible of bool (** Is substitution by an algebraic ok? *)
@@ -110,10 +108,15 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
+val demote_seff_univs : Univ.LSet.t -> t -> t
+(** Mark the universes as not local any more, because they have been
+ globally declared by some side effect. You should be using
+ emit_side_effects instead. *)
+
val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b1ed3b2694..1fe09270ba 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
| IsGlobal gr -> fresh_global_instance env gr
-let global_of_constr c =
- match kind c with
- | Const (c, u) -> GlobRef.ConstRef c, u
- | Ind (i, u) -> GlobRef.IndRef i, u
- | Construct (c, u) -> GlobRef.ConstructRef c, u
- | Var id -> GlobRef.VarRef id, Instance.empty
- | _ -> raise Not_found
-
let fresh_sort_in_family = function
| InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 1c8735bfa8..1b351c61c4 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -54,9 +54,6 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const
val fresh_universe_context_set_instance : ContextSet.t ->
universe_level_subst * ContextSet.t
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> GlobRef.t puniverses
-
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an error on polymorphic constants/inductives:
the constraints should be properly added to an evd.
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1b7c33b9c1..30fdd28997 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -269,11 +269,11 @@ 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 normalize_context_set ~lbound g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
(* 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
+ Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
in
let smallles = if get_set_minimization ()
then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
@@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak =
let csts, partition =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
- let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+ let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g)
ctx UGraph.initial_universes
in
let add_soft u g =
if not (Level.is_small u || LSet.mem u ctx)
- then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+ then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g
else g
in
let g = Constraint.fold
@@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak =
(* We ignore the trivial Prop/Set <= i constraints. *)
let noneqs =
Constraint.filter
- (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+ (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
(Level.is_prop l && d == Lt && Level.is_set r)))
csts
in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 21f6efe86a..72b432e62f 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
-val normalize_context_set : UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
universe_opt_subst (* The defined and undefined variables *) ->
LSet.t (* univ variables that can be substituted by algebraics *) ->
UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 6cc7868a38..1f1edbed16 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
val universes_of_constr : constr -> LSet.t
[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> 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 13:02:29 +0000