aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml4
-rw-r--r--engine/evarutil.ml10
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml41
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/namegen.ml32
-rw-r--r--engine/proofview.ml22
-rw-r--r--engine/termops.ml33
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml50
-rw-r--r--engine/uState.mli13
-rw-r--r--engine/univMinim.ml8
-rw-r--r--engine/univMinim.mli2
-rw-r--r--engine/univSubst.ml2
-rw-r--r--engine/univops.mli2
15 files changed, 128 insertions, 99 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 4508633858..ca681e58f8 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -355,7 +355,7 @@ let iter_with_full_binders sigma g f n c =
| Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
- | Evar (_,l) -> Array.Fun1.iter f n l
+ | Evar (_,l) -> List.iter (fun c -> f n c) l
| Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
@@ -717,7 +717,7 @@ let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq
let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
let of_existential : Constr.existential -> existential =
- let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+ let gen : type a b. (a,b) eq -> 'c * b list -> 'c * a list = fun Refl x -> x in
gen unsafe_eq
let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fdcdfe11f4..5fcadfcef7 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -200,7 +200,7 @@ let make_pure_subst evi args =
match args with
| a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
| _ -> anomaly (Pp.str "Instance does not match its signature."))
- (evar_filtered_context evi) (Array.rev_to_list args,[]))
+ (evar_filtered_context evi) (List.rev args,[]))
(*------------------------------------*
* functional operations on evar sets *
@@ -448,7 +448,7 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
- evd, mkEvar (newevk,Array.of_list instance)
+ evd, mkEvar (newevk, instance)
let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
@@ -506,7 +506,7 @@ let generalize_evar_over_rels sigma (ev,args) =
List.fold_left2
(fun (c,inst as x) a d ->
if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
- (evi.evar_concl,[]) (Array.to_list args) sign
+ (evi.evar_concl,[]) args sign
(************************************)
(* Removing a dependency in an evar *)
@@ -594,7 +594,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
(* No dependency at all, we can keep this ev's context hyp *)
(ri, true::filter)
with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
- ctxt (Array.to_list l) (Id.Map.empty,[]) in
+ ctxt l (Id.Map.empty,[]) in
(* Check if some rid to clear in the context of ev has dependencies
in the type of ev and adjust the source of the dependency *)
let _nconcl =
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
match EConstr.kind evd c with
| Evar (n, l) ->
let acc = Evar.Set.add n acc in
- Array.fold_left evrec acc l
+ List.fold_left evrec acc l
| _ -> EConstr.fold evd evrec acc c
in
evrec Evar.Set.empty t
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 1dec63aaf0..b5c7ccb283 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -88,7 +88,7 @@ val new_evar_instance :
named_context_val -> evar_map -> types ->
constr list -> evar_map * constr
-val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
+val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
diff --git a/engine/evd.ml b/engine/evd.ml
index 65fe261ff4..5642145f6d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -233,32 +233,27 @@ exception NotInstantiatedEvar
(* Note: let-in contributes to the instance *)
let evar_instance_array test_id info args =
- let len = Array.length args in
- let rec instrec filter ctxt i = match filter, ctxt with
- | [], [] ->
- if Int.equal i len then []
- else instance_mismatch ()
- | false :: filter, _ :: ctxt ->
- instrec filter ctxt i
- | true :: filter, d :: ctxt ->
- if i < len then
- let c = Array.unsafe_get args i in
- if test_id d c then instrec filter ctxt (succ i)
- else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
- else instance_mismatch ()
+ let rec instrec filter ctxt args = match filter, ctxt, args with
+ | [], [], [] -> []
+ | false :: filter, _ :: ctxt, args ->
+ instrec filter ctxt args
+ | true :: filter, d :: ctxt, c :: args ->
+ if test_id d c then instrec filter ctxt args
+ else (NamedDecl.get_id d, c) :: instrec filter ctxt args
| _ -> instance_mismatch ()
in
match Filter.repr (evar_filter info) with
| None ->
- let map i d =
- if (i < len) then
- let c = Array.unsafe_get args i in
- if test_id d c then None else Some (NamedDecl.get_id d, c)
- else instance_mismatch ()
+ let rec instance ctxt args = match ctxt, args with
+ | [], [] -> []
+ | d :: ctxt, c :: args ->
+ if test_id d c then instance ctxt args
+ else (NamedDecl.get_id d, c) :: instance ctxt args
+ | _ -> instance_mismatch ()
in
- List.map_filter_i map (evar_context info)
+ instance (evar_context info) args
| Some filter ->
- instrec filter (evar_context info) 0
+ instrec filter (evar_context info) args
let make_evar_instance_array info args =
evar_instance_array (NamedDecl.get_id %> isVarId) info args
@@ -794,7 +789,7 @@ let restrict evk filter ?candidates ?src evd =
| _ -> Evar.Set.add evk evd.last_mods in
let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
let ctxt = Filter.filter_list filter (evar_context evar_info) in
- let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
+ let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
let body = mkEvar(evk',id_inst) in
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
@@ -1405,7 +1400,7 @@ let evars_of_term evd c =
let rec evrec acc c =
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)
+ | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
| _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
@@ -1413,7 +1408,7 @@ let evars_of_term evd 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)
+ | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
| _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
diff --git a/engine/evd.mli b/engine/evd.mli
index bbdb63a467..c6c4a71b22 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -247,9 +247,9 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
val existential_opt_value0 : evar_map -> existential -> constr option
val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
- 'a array -> (Id.t * 'a) list
+ 'a list -> (Id.t * 'a) list
-val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
+val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr
val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
evar_map -> evar_map -> evar_map
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 370f35f6ed..c4472050f8 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -219,22 +219,22 @@ let get_mangle_names =
~key:["Mangle";"Names"]
~value:false
-let mangle_names_prefix = ref (Id.of_string "_0")
-
-let set_prefix x = mangle_names_prefix := forget_subscript x
-
-let () = Goptions.(
- declare_string_option
- { optdepr = false;
- optkey = ["Mangle";"Names";"Prefix"];
- optread = (fun () -> Id.to_string !mangle_names_prefix);
- optwrite = begin fun x ->
- set_prefix
- (try Id.of_string x
- with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")))
- end })
-
-let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id
+let mangle_names_prefix =
+ Goptions.declare_interpreted_string_option_and_ref
+ ~depr:false
+ ~key:["Mangle";"Names";"Prefix"]
+ ~value:(Id.of_string "_0")
+ (fun x ->
+ (try
+ Id.of_string x
+ with
+ | CErrors.UserError _ ->
+ CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))
+ ) |> forget_subscript
+ )
+ (fun x -> Id.to_string x)
+
+let mangle_id id = if get_mangle_names () then mangle_names_prefix () else id
(* Looks for next "good" name by lifting subscript *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..de38104ecd 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -261,13 +261,9 @@ module Monad = Proof
(** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
+let tclZERO ?(info=Exninfo.null) e =
if not (CErrors.noncritical e) then
CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
- let info = match info with
- | None -> Exninfo.null
- | Some info -> info
- in
Proof.zero (e, info)
(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
@@ -323,9 +319,10 @@ let tclEXACTLY_ONCE e t =
split t >>= function
| Nil (e, info) -> tclZERO ~info e
| Cons (x,k) ->
- Proof.split (k (e, Exninfo.null)) >>= function
- | Nil _ -> tclUNIT x
- | _ -> tclZERO MoreThanOneSuccess
+ let info = Exninfo.null in
+ Proof.split (k (e, Exninfo.null)) >>= function
+ | Nil _ -> tclUNIT x
+ | _ -> tclZERO ~info MoreThanOneSuccess
(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
@@ -359,7 +356,7 @@ end
is restored at the end of the tactic). If the range [i]-[j] is not
valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
let tclFOCUS ?nosuchgoal i j t =
- let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
+ let nosuchgoal ~info = Option.default (tclZERO ~info (NoSuchGoals (j+1-i))) nosuchgoal in
let open Proof in
Pv.get >>= fun initial ->
try
@@ -368,7 +365,9 @@ let tclFOCUS ?nosuchgoal i j t =
t >>= fun result ->
Pv.modify (fun next -> unfocus context next) >>
return result
- with CList.IndexOutOfRange -> nosuchgoal
+ with CList.IndexOutOfRange as exn ->
+ let _, info = Exninfo.capture exn in
+ nosuchgoal ~info
let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
@@ -907,7 +906,8 @@ let tclPROGRESS t =
if not test then
tclUNIT res
else
- tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
+ let info = Exninfo.reify () in
+ tclZERO ~info (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
let _ = CErrors.register_handler begin function
| Logic_monad.Tac_Timeout ->
diff --git a/engine/termops.ml b/engine/termops.ml
index 16f2a87c1e..c51e753d46 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
if b' == b then c
else mkProj (p, b')
| Evar (e,al) ->
- let al' = Array.map_left (f l) al in
- if Array.for_all2 (==) al' al then c
+ let al' = List.map_left (f l) al in
+ if List.for_all2 (==) al' al then c
else mkEvar (e, al')
| Case (ci,p,b,bl) ->
(* In v8 concrete syntax, predicate is after the term to match! *)
@@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
let c' = f l c in
if c' == c then cstr else mkProj (p, c')
| Evar (e,al) ->
- let al' = Array.map (f l) al in
- if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+ let al' = List.map (f l) al in
+ if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
| Case (ci,p,c,bl) when userview ->
let p' = map_return_predicate_with_full_binders sigma g f l ci p in
let c' = f l c in
@@ -803,23 +803,29 @@ let occur_evar sigma n c =
let occur_in_global env id constr =
let vars = vars_of_global env constr in
- if Id.Set.mem id vars then raise Occur
+ Id.Set.mem id vars
let occur_var env sigma id c =
let rec occur_rec c =
match EConstr.destRef sigma c with
- | gr, _ -> occur_in_global env id gr
+ | gr, _ -> if occur_in_global env id gr then raise Occur
| exception DestKO -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
+exception OccurInGlobal of GlobRef.t
+
+let occur_var_indirectly env sigma id c =
+ let var = GlobRef.VarRef id in
+ let rec occur_rec c =
+ match EConstr.destRef sigma c with
+ | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr)
+ | exception DestKO -> EConstr.iter sigma occur_rec c
+ in
+ try occur_rec c; None with OccurInGlobal gr -> Some gr
+
let occur_var_in_decl env sigma hyp decl =
- let open NamedDecl in
- match decl with
- | LocalAssum (_,typ) -> occur_var env sigma hyp typ
- | LocalDef (_, body, typ) ->
- occur_var env sigma hyp typ ||
- occur_var env sigma hyp body
+ NamedDecl.exists (occur_var env sigma hyp) decl
let local_occur_var sigma id c =
let rec occur c = match EConstr.kind sigma c with
@@ -828,6 +834,9 @@ let local_occur_var sigma id c =
in
try occur c; false with Occur -> true
+let local_occur_var_in_decl sigma hyp decl =
+ NamedDecl.exists (local_occur_var sigma hyp) decl
+
(* returns the list of free debruijn indices in a term *)
let free_rels sigma m =
diff --git a/engine/termops.mli b/engine/termops.mli
index 4e77aa9b3b..709fa361a9 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool
val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
+val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option
val occur_var_in_decl :
env -> Evd.evar_map ->
Id.t -> named_declaration -> bool
(** As {!occur_var} but assume the identifier not to be a section variable *)
val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
+val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool
val free_rels : Evd.evar_map -> constr -> Int.Set.t
diff --git a/engine/uState.ml b/engine/uState.ml
index d532129dc5..99ac5f2ce8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,12 +34,12 @@ 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_universes_lbound : UGraph.Bound.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
}
-let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes
let empty =
{ uctx_names = UNameMap.empty, LMap.empty;
@@ -48,7 +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_universes_lbound = UGraph.Bound.Set;
uctx_initial_universes = initial_sprop_cumulative;
uctx_weak_constraints = UPairSet.empty; }
@@ -57,11 +57,11 @@ let elaboration_sprop_cumul =
~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
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_universes_lbound = lbound;
- uctx_initial_universes = u}
+ let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in
+ { empty with
+ uctx_universes = u;
+ uctx_universes_lbound = lbound;
+ uctx_initial_universes = u}
let is_empty ctx =
ContextSet.is_empty ctx.uctx_local &&
@@ -176,8 +176,11 @@ let instantiate_variable l b v =
exception UniversesDiffer
-let drop_weak_constraints = ref false
-
+let drop_weak_constraints =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Cumulativity";"Weak";"Constraints"]
+ ~value:false
let process_universe_constraints ctx cstrs =
let open UnivSubst in
@@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs =
| ULub (l, r) ->
equalize_variables true (Universe.make l) l (Universe.make r) r local
| UWeak (l, r) ->
- if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local
+ if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
| UEq (l, r) -> equalize_universes l r local
in
let local =
@@ -440,6 +443,10 @@ let check_univ_decl ~poly uctx decl =
(ContextSet.constraints uctx.uctx_local);
ctx
+let is_bound l lbound = match lbound with
+| 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
if LSet.is_empty removed then univs, csts
@@ -452,7 +459,7 @@ let restrict_universe_context ~lbound (univs, csts) keep =
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.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+ 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 =
@@ -524,6 +531,14 @@ let demote_seff_univs univs uctx =
let seff = LSet.union uctx.uctx_seff_univs univs in
{ uctx with uctx_seff_univs = seff }
+let demote_global_univs env uctx =
+ let env_ugraph = Environ.universes env in
+ let global_univs = UGraph.domain env_ugraph in
+ let global_constraints, _ = UGraph.constraints_of_universes env_ugraph in
+ let promoted_uctx =
+ ContextSet.(of_set global_univs |> add_constraints global_constraints) in
+ { uctx with uctx_local = ContextSet.diff uctx.uctx_local promoted_uctx }
+
let merge_seff uctx ctx' =
let levels = ContextSet.levels ctx' in
let declare g =
@@ -544,10 +559,11 @@ let emit_side_effects eff u =
merge_seff u uctx
let update_sigma_env uctx env =
- let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
+ let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in
let eunivs =
- { uctx with uctx_initial_universes = univs;
- uctx_universes = univs }
+ { uctx with
+ uctx_initial_universes = univs;
+ uctx_universes = univs }
in
merge_seff eunivs eunivs.uctx_local
@@ -588,10 +604,10 @@ let make_with_initial_binders ~lbound e us =
let add_global_univ uctx u =
let initial =
- UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
+ UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes
in
let univs =
- UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
+ UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes
in
{ uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
uctx_initial_universes = initial;
diff --git a/engine/uState.mli b/engine/uState.mli
index 3959373ead..533a501b59 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
val empty : t
-val make : lbound:Univ.Level.t -> UGraph.t -> t
+val make : lbound:UGraph.Bound.t -> UGraph.t -> t
-val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
val is_empty : t -> bool
@@ -69,8 +69,6 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry
(** {5 Constraints handling} *)
-val drop_weak_constraints : bool ref
-
val add_constraints : t -> Univ.Constraint.t -> t
(**
@raise UniversesDiffer when universes differ
@@ -92,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
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 : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.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
@@ -112,6 +110,11 @@ 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_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 *)
+
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
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c05a7a800d..4dd7fe7e70 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -267,12 +267,16 @@ let minimize_univ_variables ctx us algs left right cstrs =
module UPairs = OrderedType.UnorderedPair(Univ.Level)
module UPairSet = Set.Make (UPairs)
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
(* TODO check is_small/sprop *)
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.equal l lbound || Level.is_sprop l)) csts
+ Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
in
let smallles = if get_set_minimization ()
then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
@@ -299,7 +303,7 @@ let normalize_context_set ~lbound 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.equal l lbound) ||
+ (fun (l,d,r) -> not ((d == Le && is_bound 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 2a46d87609..58853e47b8 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 : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:UGraph.Bound.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/univSubst.ml b/engine/univSubst.ml
index 6000650ad9..a691239ee2 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,7 +131,7 @@ let nf_evars_and_universes_opt_subst f subst =
let rec aux c =
match kind c with
| Evar (evk, args) ->
- let args = Array.map aux args in
+ let args = List.map aux args in
(match try f (evk, args) with Not_found -> None with
| None -> mkEvar (evk, args)
| Some c -> aux c)
diff --git a/engine/univops.mli b/engine/univops.mli
index 02a731ad49..d0145f5643 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 : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.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-04 21:50:03 +0000