aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml13
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml15
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/evd.ml6
-rw-r--r--engine/evd.mli6
-rw-r--r--engine/termops.ml2
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml8
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univNames.ml21
-rw-r--r--engine/univNames.mli2
-rw-r--r--engine/universes.ml2
-rw-r--r--engine/universes.mli4
-rw-r--r--engine/univops.ml15
-rw-r--r--engine/univops.mli4
16 files changed, 62 insertions, 50 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 6810626ad..005ef1635 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n =
let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
if res then Some !cstrs else None
-let universes_of_constr env sigma c =
+let universes_of_constr sigma c =
let open Univ in
- let open Declarations in
let rec aux s c =
match kind sigma c with
| Const (c, u) ->
- begin match (Environ.lookup_constant c env).const_universes with
- | Polymorphic_const _ ->
LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
- | Monomorphic_const (univs, _) ->
- LSet.union s univs
- end
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- begin match (Environ.lookup_mind mind env).mind_universes with
- | Cumulative_ind _ | Polymorphic_ind _ ->
LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
- | Monomorphic_ind (univs,_) ->
- LSet.union s univs
- end
| Sort u ->
let sort = ESorts.kind sigma u in
if Sorts.is_small sort then s
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9d3e782b..913825a9f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
(** Gather the universes transitively used in the term, including in the
type of evars appearing in it. *)
-val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
(** {6 Substitutions} *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index cdc2897c8..0c044f20d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -510,6 +510,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
evdref := evd';
ev
+(* Safe interface to unification problems *)
+type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr
+
+let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
+ pbty == pbty' && env == env' &&
+ EConstr.eq_constr evd t1 t1' &&
+ EConstr.eq_constr evd t2 t2'
+
+let add_unification_pb ?(tail=false) pb evd =
+ let conv_pbs = Evd.conv_pbs evd in
+ if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
+ let (pbty,env,t1,t2) = pb in
+ Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
+ else evd
+
(* This assumes an evar with identity instance and generalizes it over only
the de Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 1003c4feb..8ce1b625f 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -214,6 +214,14 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
val compare_constructor_instances : evar_map ->
Univ.Instance.t -> Univ.Instance.t -> evar_map
+(** {6 Unification problems} *)
+type unification_pb = conv_pb * env * constr * constr
+
+(** [add_unification_pb ?tail pb sigma]
+ Add a unification problem [pb] to [sigma], if not already present.
+ Put it at the end of the list if [tail] is true, by default it is false. *)
+val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
+
(** {6 Removing hyps in evars'context}
raise OccurHypInSimpleClause if the removal breaks dependencies *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 7e0c397b2..945cba58f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -624,10 +624,11 @@ let set_universe_context evd uctx' =
(* TODO: make unique *)
let add_conv_pb ?(tail=false) pb d =
- (** MS: we have duplicates here, why? *)
if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
else {d with conv_pbs = pb::d.conv_pbs}
+let conv_pbs d = d.conv_pbs
+
let evar_source evk d = (find d evk).evar_source
let evar_ident evk evd = EvNames.ident evk evd.evar_names
@@ -897,6 +898,9 @@ let check_eq evd s s' =
let check_leq evd s s' =
UGraph.check_leq (UState.ugraph evd.universes) s s'
+let check_constraints evd csts =
+ UGraph.check_constraints csts (UState.ugraph evd.universes)
+
let fix_undefined_variables evd =
{ evd with universes = UState.fix_undefined_variables evd.universes }
diff --git a/engine/evd.mli b/engine/evd.mli
index 83fd00065..64db70451 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -441,7 +441,11 @@ type clbinding =
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * econstr * econstr
+
+(** The following two functions are for internal use only,
+ see [Evarutil.add_unification_pb] for a safe interface. *)
val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
+val conv_pbs : evar_map -> evar_constraint list
val extract_changed_conv_pbs : evar_map ->
(Evar.Set.t -> evar_constraint -> bool) ->
@@ -554,6 +558,8 @@ val set_eq_instances : ?flex:bool ->
val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
+val check_constraints : evar_map -> Univ.Constraint.t -> bool
+
val evar_universe_context : evar_map -> UState.t
val universe_context_set : evar_map -> Univ.ContextSet.t
val universe_subst : evar_map -> UnivSubst.universe_opt_subst
diff --git a/engine/termops.ml b/engine/termops.ml
index eacc36107..2db2e07bf 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -297,7 +297,7 @@ let has_no_evar sigma =
with Exit -> false
let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
+let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
let pr_evar_universe_context ctx =
let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index 255494031..f9aa6ba63 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
val is_Set : Evd.evar_map -> constr -> bool
val is_Type : Evd.evar_map -> constr -> bool
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
(** Combinators on judgments *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 0e3ecdbf5..81ab3dd66 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -295,15 +295,15 @@ let constrain_variables diff ctx =
in
{ ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
-let reference_of_level uctx =
+let qualid_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
+ try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
with Not_found | Option.IsNone ->
- UnivNames.reference_of_level l
+ UnivNames.qualid_of_level l
let pr_uctx_level uctx l =
- Libnames.pr_reference (reference_of_level uctx l)
+ Libnames.pr_qualid (qualid_of_level uctx l)
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index e7e5b39e0..a59e61b89 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -171,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6ffb4bcf0..a68840174 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -14,18 +14,19 @@ open Globnames
open Nametab
-let reference_of_level l = CAst.make @@
+let qualid_of_level l =
match Level.name l with
| Some (d, n as na) ->
- let qid =
- try Nametab.shortest_qualid_of_universe na
- with Not_found ->
- let name = Id.of_string_soft (string_of_int n) in
- Libnames.make_qualid d name
- in Libnames.Qualid qid
- | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+ begin
+ try Nametab.shortest_qualid_of_universe na
+ with Not_found ->
+ let name = Id.of_string_soft (string_of_int n) in
+ Libnames.make_qualid d name
+ end
+ | None ->
+ Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+
+let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
(** Global universe information outside the kernel, to handle
polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index c19aa19d5..837beac26 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
open Univ
val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
+val qualid_of_level : Level.t -> Libnames.qualid
(** Global universe information outside the kernel, to handle
polymorphic universes in sections that have to be discharged. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 70601987c..ee9668433 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders
type univ_name_list = UnivNames.univ_name_list
let pr_with_global_universes = UnivNames.pr_with_global_universes
-let reference_of_level = UnivNames.reference_of_level
+let reference_of_level = UnivNames.qualid_of_level
let add_global_universe = UnivNames.add_global_universe
diff --git a/engine/universes.mli b/engine/universes.mli
index 46ff33a47..29673de1e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -22,8 +22,8 @@ open Univ
val pr_with_global_universes : Level.t -> Pp.t
[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
-val reference_of_level : Level.t -> Libnames.reference
-[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
+val reference_of_level : Level.t -> Libnames.qualid
+[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
diff --git a/engine/univops.ml b/engine/univops.ml
index 3fd518490..7f9672f82 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -11,24 +11,13 @@
open Univ
open Constr
-let universes_of_constr env c =
- let open Declarations in
- let rec aux s c =
+let universes_of_constr c =
+ let rec aux s c =
match kind c with
| Const (c, u) ->
- begin match (Environ.lookup_constant c env).const_universes with
- | Polymorphic_const _ ->
LSet.fold LSet.add (Instance.levels u) s
- | Monomorphic_const (univs, _) ->
- LSet.union s univs
- end
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- begin match (Environ.lookup_mind mind env).mind_universes with
- | Cumulative_ind _ | Polymorphic_ind _ ->
LSet.fold LSet.add (Instance.levels u) s
- | Monomorphic_ind (univs,_) ->
- LSet.union s univs
- end
| Sort u when not (Sorts.is_small u) ->
let u = Sorts.univ_of_sort u in
LSet.fold LSet.add (Universe.levels u) s
diff --git a/engine/univops.mli b/engine/univops.mli
index 0b37ab975..57a53597b 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -11,8 +11,8 @@
open Constr
open Univ
-(** The universes of monomorphic constants appear. *)
-val universes_of_constr : Environ.env -> constr -> LSet.t
+(** Return the set of all universes appearing in [constr]. *)
+val universes_of_constr : constr -> LSet.t
(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
the universes in [keep]. The constraints [csts] are adjusted so
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 02:50:29 +0000