From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- pretyping/pretyping.ml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3470b0f1..ffbc21a5e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -181,9 +181,8 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = match s with | Anonymous -> new_univ_level_variable ?loc anon_rigidity evd - | Name s -> - let s = Id.to_string s in - let names, _ = Global.global_universe_names () in + | Name id -> + let s = Id.to_string id in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") @@ -197,17 +196,17 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = in evd, level else try - let level = Evd.universe_of_name evd s in - evd, level + let level = Evd.universe_of_name evd id in + evd, level with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Id.Map.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:s univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + try + let names, _ = Global.global_universe_names () in + evd, snd (Id.Map.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in -- cgit v1.2.3 From f8e639f3b81ae142f5b529be1ad90210fc259375 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 28 Sep 2017 22:28:21 +0200 Subject: Fix interpretation of global universes in univdecl constraints. Also nicer error when the constraints are impossible. --- pretyping/pretyping.ml | 30 +++++++++++++++++++++++------- pretyping/pretyping.mli | 3 +++ pretyping/univdecls.ml | 22 +++++----------------- test-suite/output/UnivBinders.out | 2 ++ test-suite/output/UnivBinders.v | 4 ++++ test-suite/success/polymorphism.v | 4 ++++ 6 files changed, 41 insertions(+), 24 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ffbc21a5e..a9bff5bf6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -177,6 +177,14 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) +let interp_known_universe_level evd id = + try + let level = Evd.universe_of_name evd id in + level + with Not_found -> + let names, _ = Global.global_universe_names () in + snd (Id.Map.find id names) + let interp_universe_level_name ~anon_rigidity evd (loc, s) = match s with | Anonymous -> @@ -195,13 +203,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = with UGraph.AlreadyDeclared -> evd in evd, level else - try - let level = Evd.universe_of_name evd id in - evd, level - with Not_found -> - try - let names, _ = Global.global_universe_names () in - evd, snd (Id.Map.find id names) + try evd, interp_known_universe_level evd id with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ?loc ~name:id univ_rigid evd @@ -218,6 +220,15 @@ let interp_universe ?loc evd = function (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l +let interp_known_level_info ?loc evd = function + | None | Some (_, Anonymous) -> + user_err ?loc ~hdr:"interp_known_level_info" + (str "Anonymous universes not allowed here.") + | Some (loc, Name id) -> + try interp_known_universe_level evd id + with Not_found -> + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id) + let interp_level_info ?loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ?loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) @@ -466,6 +477,11 @@ let pretype_id pretype k0 loc env evdref lvar id = (*************************************************************************) (* Main pretyping function *) +let interp_known_glob_level ?loc evd = function + | GProp -> Univ.Level.prop + | GSet -> Univ.Level.set + | GType s -> interp_known_level_info ?loc evd s + let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b2735ee22..d0fb5cad9 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -20,6 +20,9 @@ open Glob_term open Ltac_pretype open Evardefine +val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> + Misctypes.glob_level -> Univ.Level.t + (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index a5266125a..3cf32d7ff 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -6,9 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open CErrors open Names +open CErrors (** Local universes and constraints declarations *) type universe_decl = @@ -22,27 +21,16 @@ let default_univ_decl = univdecl_extensible_constraints = true } let interp_univ_constraints env evd cstrs = - let open Misctypes in - let u_of_id x = - match x with - | Misctypes.GProp -> Loc.tag Univ.Level.prop - | GSet -> Loc.tag Univ.Level.set - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"interp_constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - try loc, Evd.universe_of_name evd id - with Not_found -> - user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id) - in let interp (evd,cstrs) (u, d, u') = - let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in let cstr = (ul,d,u'l) in let cstrs' = Univ.Constraint.add cstr cstrs in try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in evd, cstrs' with Univ.UniverseInconsistency e -> - user_err ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *)) + user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) in List.fold_left interp (evd,Univ.Constraint.empty) cstrs diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a2857294b..9eb162fc0 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -86,6 +86,8 @@ The command has indeed failed with message: Universe instance should have length 0 The command has indeed failed with message: This object does not support universe names. +The command has indeed failed with message: +Cannot enforce v < u because u < gU < gV < v Monomorphic bind_univs.mono = Type@{u} : Type@{u+1} (* {u} |= *) diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 013f215b5..a65a1fdf3 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -56,6 +56,10 @@ Fail Print mono@{E}. (* Not everything can be printed with custom universe names. *) Fail Print Coq.Init.Logic@{E}. +(* Nice error when constraints are impossible. *) +Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. +Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. + (* Universe binders survive through compilation, sections and modules. *) Require bind_univs. Print bind_univs.mono. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index c09a60a4d..b3f9a4994 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -202,6 +202,10 @@ Module binders. exact Type@{i}. Qed. + Monomorphic Universe M. + Fail Definition with_mono@{u|} : Type@{M} := Type@{u}. + Definition with_mono@{u|u < M} : Type@{M} := Type@{u}. + End binders. Section cats. -- cgit v1.2.3