From f72a67569ec8cb9160d161699302b67919da5686 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 27 Jul 2017 14:54:41 +0200 Subject: Allow declaring universe constraints at definition level. Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. --- engine/evd.ml | 20 ++++++++++++++++++++ engine/evd.mli | 4 ++++ engine/uState.ml | 2 ++ engine/uState.mli | 3 +++ engine/universes.ml | 4 ++-- 5 files changed, 31 insertions(+), 2 deletions(-) (limited to 'engine') 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 -- cgit v1.2.3 From 8966c9241207b6f5d4ee38508246ee97ed006e72 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 31 Jul 2017 16:49:06 +0200 Subject: proof_global: cleanup and comment close_proof evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. --- engine/evd.mli | 2 +- engine/uState.ml | 28 ++++++++++++++++++---------- engine/uState.mli | 2 +- 3 files changed, 20 insertions(+), 12 deletions(-) (limited to 'engine') diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e313..8c3771cd94 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : diff --git a/engine/uState.ml b/engine/uState.ml index 312502491c..979a9b086b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,16 +101,6 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty - let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -242,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> diff --git a/engine/uState.mli b/engine/uState.mli index ba03058693..0b67bb71f8 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -108,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t -- cgit v1.2.3 From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 9 Sep 2017 14:00:42 +0200 Subject: Don't lose names in UState.universe_context. We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. --- engine/evd.ml | 25 +++------------ engine/evd.mli | 8 ++--- engine/uState.ml | 92 ++++++++++++++++++++++++++++++++++--------------------- engine/uState.mli | 8 ++++- 4 files changed, 71 insertions(+), 62 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 06b257a9e5..f1b5419dec 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -748,27 +748,10 @@ let evar_universe_context d = d.universes 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 universe_context ~names ~extensible evd = + UState.universe_context ~names ~extensible evd.universes + +let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl 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 8c3771cd94..abcabe8157 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -547,15 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> +val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.universe_context 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 check_univ_decl : evar_map -> UState.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 979a9b086b..13a9bb3732 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -257,41 +257,63 @@ let pr_uctx_level uctx = with Not_found | Option.IsNone -> Universes.pr_with_global_universes l -let universe_context ?names ctx = - match names with - | None -> [], Univ.ContextSet.to_context ctx.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels ctx.uctx_local in - let newinst, map, left = - List.fold_right - (fun (loc,id) (newinst, map, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") - in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) - pl ([], [], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in - info.uloc - with Not_found -> None - in - user_err ?loc ~hdr:"universe_context" - ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) - else - let inst = Univ.Instance.of_array (Array.of_list newinst) in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) - in map, ctx +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let universe_context ~names ~extensible ctx = + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err ?loc ~hdr:"universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.LSet.remove l acc)) + names ([], levels) + in + if not extensible && not (Univ.LSet.is_empty left) then + let n = Univ.LSet.cardinal left in + let loc = + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + info.uloc + with Not_found -> None + in + user_err ?loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + else + let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let inst = Array.append (Array.of_list newinst) left in + let inst = Univ.Instance.of_array inst in + let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints ctx.uctx_local) in + map, ctx + +let check_implication uctx cstrs ctx = + let gr = 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 uctx decl = + let open Misctypes in + let pl, ctx = universe_context + ~names:decl.univdecl_instance + ~extensible:decl.univdecl_extensible_instance + uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx decl.univdecl_constraints ctx; + pl, ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index 0b67bb71f8..21145e7e67 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -120,7 +120,13 @@ val normalize : t -> t (** {5 TODO: Document me} *) -val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context +val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> + (Id.t * Univ.Level.t) list * Univ.universe_context + +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context val update_sigma_env : t -> Environ.env -> t -- cgit v1.2.3 From 3c964a60d698134c21adc77cbb69ce1528350682 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 9 Sep 2017 14:54:42 +0200 Subject: Document UState.universe_context. --- engine/uState.mli | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/uState.mli b/engine/uState.mli index 21145e7e67..c44f2c1d74 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -118,8 +118,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** {5 TODO: Document me} *) +(** [universe_context names extensible ctx] + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to [names] come + first in the order defined by that list. + + If [extensible] is false, check that the universes of [names] are + the only local universes. + Also return the association list of universe names and universes + (including those not in [names]). *) val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context @@ -128,6 +137,8 @@ type universe_decl = val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context +(** {5 TODO: Document me} *) + val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) -- cgit v1.2.3