aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview.ml22
-rw-r--r--engine/termops.ml25
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml14
-rw-r--r--engine/uState.mli6
-rw-r--r--engine/univMinim.ml8
-rw-r--r--engine/univMinim.mli2
-rw-r--r--engine/univops.mli2
8 files changed, 50 insertions, 31 deletions
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 6d779e6a35..c51e753d46 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -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 00649ce042..99ac5f2ce8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,7 +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_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
}
@@ -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; }
@@ -443,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
@@ -455,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 =
@@ -600,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 6707826aae..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
@@ -90,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
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/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-03-08 07:11:42 +0000