diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 20 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/uState.mli | 3 | ||||
| -rw-r--r-- | engine/universes.ml | 4 |
5 files changed, 31 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index cfc9aa6351..06b257a9e5 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -750,6 +750,26 @@ let universe_context_set d = UState.context_set d.universes let universe_context ?names evd = UState.universe_context ?names evd.universes +open Misctypes +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let check_implication evd cstrs ctx = + let uctx = evar_universe_context evd in + let gr = UState.initial_graph uctx in + let grext = UGraph.merge_constraints cstrs gr in + let cstrs' = Univ.UContext.constraints ctx in + if UGraph.check_constraints cstrs' grext then () + else CErrors.user_err ~hdr:"check_univ_decl" + (str "Universe constraints are not implied by the ones declared.") + +let check_univ_decl evd decl = + let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in + let pl, ctx = universe_context ?names:pl evd in + if not decl.univdecl_extensible_constraints then + check_implication evd decl.univdecl_constraints ctx; + pl, ctx + let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } diff --git a/engine/evd.mli b/engine/evd.mli index 3f00a3b0b2..76fa69e313 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -552,6 +552,10 @@ val universe_context : ?names:(Id.t located) list -> evar_map -> val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 63bd247d56..312502491c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -97,6 +97,8 @@ let subst ctx = ctx.uctx_univ_variables let ugraph ctx = ctx.uctx_universes +let initial_graph ctx = ctx.uctx_initial_universes + let algebraics ctx = ctx.uctx_univ_algebraic let constrain_variables diff ctx = diff --git a/engine/uState.mli b/engine/uState.mli index d198fbfbe9..ba03058693 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst val ugraph : t -> UGraph.t (** The current graph extended with the local constraints *) +val initial_graph : t -> UGraph.t +(** The initial graph with just the declarations of new universes. *) + val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) diff --git a/engine/universes.ml b/engine/universes.ml index 719af43edf..91398d162c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,7 +14,7 @@ open Environ open Univ open Globnames -let pr_with_global_universes l = +let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l @@ -31,7 +31,7 @@ let universe_binders_of_global ref = let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table - + (* To disallow minimization to Set *) let set_minimization = ref true |