From 07428a659f22405ed5917cfd6690d0c0cd410f2f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 5 Jun 2024 14:02:13 +0200 Subject: [PATCH 1/2] Moving code around for reusability. --- engine/uState.ml | 68 ++++++++++++++++++++++++------------------------ 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/engine/uState.ml b/engine/uState.ml index 8942fba6944f..ed271ed38323 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -234,6 +234,40 @@ let is_empty uctx = ContextSet.is_empty uctx.local && UnivFlex.is_empty uctx.univ_variables +let id_of_level uctx l = + try (Level.Map.find l (snd (snd uctx.names))).uname + with Not_found -> None + +let id_of_qvar uctx l = + try (QVar.Map.find l (fst (snd uctx.names))).uname + with Not_found -> None + +let qualid_of_qvar_names (bind, (qrev,_)) l = + try Some (Libnames.qualid_of_ident (Option.get (QVar.Map.find l qrev).uname)) + with Not_found | Option.IsNone -> + None (* no global qvars *) + +let qualid_of_level_names (bind, (_,urev)) l = + try Some (Libnames.qualid_of_ident (Option.get (Level.Map.find l urev).uname)) + with Not_found | Option.IsNone -> + UnivNames.qualid_of_level bind l + +let qualid_of_level uctx l = qualid_of_level_names uctx.names l + +let pr_uctx_qvar_names names l = + match qualid_of_qvar_names names l with + | Some qid -> Libnames.pr_qualid qid + | None -> QVar.raw_pr l + +let pr_uctx_level_names names l = + match qualid_of_level_names names l with + | Some qid -> Libnames.pr_qualid qid + | None -> Level.raw_pr l + +let pr_uctx_level uctx l = pr_uctx_level_names uctx.names l + +let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l + let uname_union s t = if s == t then s else @@ -726,40 +760,6 @@ let constrain_variables diff uctx = let local, vars = UnivFlex.constrain_variables diff uctx.univ_variables uctx.local in { uctx with local; univ_variables = vars } -let id_of_level uctx l = - try (Level.Map.find l (snd (snd uctx.names))).uname - with Not_found -> None - -let id_of_qvar uctx l = - try (QVar.Map.find l (fst (snd uctx.names))).uname - with Not_found -> None - -let qualid_of_qvar_names (bind, (qrev,_)) l = - try Some (Libnames.qualid_of_ident (Option.get (QVar.Map.find l qrev).uname)) - with Not_found | Option.IsNone -> - None (* no global qvars *) - -let qualid_of_level_names (bind, (_,urev)) l = - try Some (Libnames.qualid_of_ident (Option.get (Level.Map.find l urev).uname)) - with Not_found | Option.IsNone -> - UnivNames.qualid_of_level bind l - -let qualid_of_level uctx l = qualid_of_level_names uctx.names l - -let pr_uctx_qvar_names names l = - match qualid_of_qvar_names names l with - | Some qid -> Libnames.pr_qualid qid - | None -> QVar.raw_pr l - -let pr_uctx_level_names names l = - match qualid_of_level_names names l with - | Some qid -> Libnames.pr_qualid qid - | None -> Level.raw_pr l - -let pr_uctx_level uctx l = pr_uctx_level_names uctx.names l - -let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l - type ('a, 'b, 'c) gen_universe_decl = { univdecl_qualities : 'a; univdecl_instance : 'b; (* Declared universes *) From 482f8510f388b886a4b9acc81f8b76d16d5385f9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 May 2024 01:28:14 +0200 Subject: [PATCH 2/2] Using more often names of universes in universe inconsistency message, if possible. --- engine/uState.ml | 20 +++++++++++++------- engine/univSubst.ml | 18 +++++++++--------- kernel/uGraph.ml | 13 +++++++++---- kernel/uGraph.mli | 3 ++- test-suite/output/UnivBinders.out | 3 +++ test-suite/output/UnivBinders.v | 8 ++++++++ 6 files changed, 44 insertions(+), 21 deletions(-) diff --git a/engine/uState.ml b/engine/uState.ml index ed271ed38323..acb10bd7dc61 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -32,7 +32,7 @@ open Quality let sort_inconsistency ?explain cst l r = let explain = Option.map (fun p -> UGraph.Other p) explain in - raise (UGraph.UniverseInconsistency (cst, l, r, explain)) + raise (UGraph.UniverseInconsistency (None, (cst, l, r, explain))) module QState : sig type t @@ -268,6 +268,12 @@ let pr_uctx_level uctx l = pr_uctx_level_names uctx.names l let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l +let merge_constraints uctx cstrs g = + try UGraph.merge_constraints cstrs g + with UGraph.UniverseInconsistency (_, i) -> + let printers = (pr_uctx_qvar uctx, pr_uctx_level uctx) in + raise (UGraph.UniverseInconsistency (Some printers, i)) + let uname_union s t = if s == t then s else @@ -314,7 +320,7 @@ let union uctx uctx' = (if local == uctx.local then uctx.universes else let cstrsr = ContextSet.constraints uctx'.local in - UGraph.merge_constraints cstrsr (declarenew uctx.universes)); + merge_constraints uctx cstrsr (declarenew uctx.universes)); minim_extra = extra} let context_set uctx = uctx.local @@ -407,7 +413,7 @@ let { Goptions.get = drop_weak_constraints } = let level_inconsistency cst l r = let mk u = Sorts.sort_of_univ @@ Universe.make u in - raise (UGraph.UniverseInconsistency (cst, mk l, mk r, None)) + raise (UGraph.UniverseInconsistency (None, (cst, mk l, mk r, None))) let nf_universe uctx u = UnivSubst.(subst_univs_universe (UnivFlex.normalize_univ_variable uctx.univ_variables)) u @@ -691,7 +697,7 @@ let add_universe_constraints uctx cstrs = { uctx with local = (univs, Constraints.union local local'); univ_variables = vars; - universes = UGraph.merge_constraints local' uctx.universes; + universes = merge_constraints uctx local' uctx.universes; sort_variables = sorts; minim_extra = extra; } @@ -851,7 +857,7 @@ let check_universe_context_set ~prefix levels names = let check_implication uctx cstrs cstrs' = let gr = initial_graph uctx in - let grext = UGraph.merge_constraints cstrs gr in + let grext = merge_constraints uctx cstrs gr in let cstrs' = Constraints.filter (fun c -> not (UGraph.check_constraint grext c)) cstrs' in if Constraints.is_empty cstrs' then () else CErrors.user_err @@ -973,7 +979,7 @@ let merge ?loc ~sideff rigid uctx uctx' = in let initial = declare uctx.initial_universes in let univs = declare uctx.universes in - let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in + let universes = merge_constraints uctx (ContextSet.constraints uctx') univs in let uctx = match rigid with | UnivRigid -> uctx @@ -1043,7 +1049,7 @@ let merge_seff uctx uctx' = in let initial_universes = declare uctx.initial_universes in let univs = declare uctx.universes in - let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in + let universes = merge_constraints uctx (ContextSet.constraints uctx') univs in { uctx with universes; initial_universes } let emit_side_effects eff u = diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 58ac1756cfbc..aeead6cbbe97 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -92,42 +92,42 @@ let enforce_eq_sort s1 s2 cst = match s1, s2 with | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2)) | ((Prop | SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) -> - raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) | (Set | Type _), (Set | Type _) -> enforce_eq (get_algebraic s1) (get_algebraic s2) cst | QSort (q1, u1), QSort (q2, u2) -> if QVar.equal q1 q2 then enforce_eq u1 u2 cst - else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) | (QSort _, (Set | Type _)) | ((Set | Type _), QSort _) -> - raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) let enforce_leq_sort s1 s2 cst = match s1, s2 with | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst | (Prop, (Set | Type _)) -> cst | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2)) | ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) -> - raise (UGraph.UniverseInconsistency (Le, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None))) | (Set | Type _), (Set | Type _) -> enforce_leq (get_algebraic s1) (get_algebraic s2) cst | QSort (q1, u1), QSort (q2, u2) -> if QVar.equal q1 q2 then enforce_leq u1 u2 cst - else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) | (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) -> - raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) let enforce_leq_alg_sort s1 s2 g = match s1, s2 with | (SProp, SProp) | (Prop, Prop) | (Set, Set) -> Constraints.empty, g | (Prop, (Set | Type _)) -> Constraints.empty, g | (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2)) | ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) -> - raise (UGraph.UniverseInconsistency (Le, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None))) | (Set | Type _), (Set | Type _) -> UGraph.enforce_leq_alg (get_algebraic s1) (get_algebraic s2) g | QSort (q1, u1), QSort (q2, u2) -> if QVar.equal q1 q2 then UGraph.enforce_leq_alg u1 u2 g - else raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) | (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) -> - raise (UGraph.UniverseInconsistency (Eq, s1, s2, None)) + raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None))) let enforce_univ_constraint (u,d,v) = match d with diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index aeedcd6b73de..eb2902800100 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -39,7 +39,8 @@ type explanation = | Path of path_explanation | Other of Pp.t -type univ_inconsistency = constraint_type * Sorts.t * Sorts.t * explanation option +type univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Level.t -> Pp.t) +type univ_inconsistency = univ_variable_printers option * (constraint_type * Sorts.t * Sorts.t * explanation option) exception UniverseInconsistency of univ_inconsistency @@ -102,7 +103,7 @@ let enforce_constraint cst g = match enforce_constraint0 cst g with let (u, c, v) = cst in let e = lazy (G.get_explanation cst g.graph) in let mk u = Sorts.sort_of_univ @@ Universe.make u in - raise (UniverseInconsistency (c, mk u, mk v, Some (Path e))) + raise (UniverseInconsistency (None, (c, mk u, mk v, Some (Path e)))) else g | Some g -> g @@ -152,7 +153,7 @@ let enforce_leq_alg u v g = | Inr ((u, c, v), g) -> let e = lazy (G.get_explanation (u, c, v) g.graph) in let mk u = Sorts.sort_of_univ @@ Universe.make u in - let e = UniverseInconsistency (c, mk u, mk v, Some (Path e)) in + let e = UniverseInconsistency (None, (c, mk u, mk v, Some (Path e))) in raise e module Bound = @@ -275,7 +276,11 @@ let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g open Pp -let explain_universe_inconsistency prq prl (o,u,v,p : univ_inconsistency) = +let explain_universe_inconsistency default_prq default_prl (printers, (o,u,v,p) : univ_inconsistency) = + let prq, prl = match printers with + | Some (prq, prl) -> prq, prl + | None -> default_prq, default_prl + in let pr_uni u = match u with | Sorts.Set -> str "Set" | Sorts.Prop -> str "Prop" diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 59191661b28b..323460491a8c 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -50,7 +50,8 @@ type explanation = | Path of path_explanation | Other of Pp.t -type univ_inconsistency = constraint_type * Sorts.t * Sorts.t * explanation option +type univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Level.t -> Pp.t) +type univ_inconsistency = univ_variable_printers option * (constraint_type * Sorts.t * Sorts.t * explanation option) exception UniverseInconsistency of univ_inconsistency diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 1484fa872270..37263a93680a 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -251,3 +251,6 @@ Arguments MutualI1' A%type_scope Arguments C1' A%type_scope p1 Arguments MutualI2' A%type_scope Arguments C2' A%type_scope p2 +File "./output/UnivBinders.v", line 208, characters 0-33: +The command has indeed failed with message: +Universe inconsistency. Cannot enforce a < a because a = a. diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 8a36a5773c95..b59831d2f6b5 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -200,3 +200,11 @@ with MutualI2' (A:Type) := C2' (p2 : MutualI1' A). Print MutualI2'. End MutualTypes. + +Module Inconsistency. + +Set Universe Polymorphism. +Definition g@{a b} := Type@{a} : Type@{b}. +Fail Definition h@{a} := g@{a a}. + +End Inconsistency.