From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Dec 2017 10:11:41 +0100 Subject: Proper nametab handling of global universe names They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced --- interp/declare.ml | 88 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 53 insertions(+), 35 deletions(-) (limited to 'interp/declare.ml') diff --git a/interp/declare.ml b/interp/declare.ml index 1b4645aff..8fc959b0f 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -453,28 +453,51 @@ let input_universe_context : universe_context_decl -> Libobject.obj = let declare_universe_context poly ctx = Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) -(* Discharged or not *) -type universe_decl = polymorphic * Universes.universe_binders - -let cache_universes (p, l) = - let glob = Global.global_universe_names () in - let glob', ctx = - Id.Map.fold (fun id lev ((idl,lid),ctx) -> - ((Id.Map.add id (p, lev) idl, - Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) - l (glob, Univ.ContextSet.empty) - in - cache_universe_context (p, ctx); - Global.set_global_universe_names glob' +(** Global universes are not substitutive objects but global objects + bound at the *library* or *module* level. The polymorphic flag is + used to distinguish universes declared in polymorphic sections, which + are discharged and do not remain in scope. *) + +type universe_decl = polymorphic * Nametab.universe_id + +let add_universe p (dp, i) = + let level = Univ.Level.make dp i in + let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in + Global.push_context_set p ctx; + Universes.add_global_universe level p; + if p then Lib.add_section_context ctx + +let check_exists sp = + let depth = sections_depth () in + let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in + if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists") + else () -let input_universes : universe_decl -> Libobject.obj = +let cache_universe ((sp, _), (poly, id)) = + let () = check_exists sp in + let () = Nametab.push_universe (Nametab.Until 1) sp id in + add_universe poly id + +let load_universe i ((sp, _), (poly, id)) = + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe poly id + +let open_universe i ((sp, _), (poly, id)) = + let () = Nametab.push_universe (Nametab.Exactly i) sp id in + ()(** add_universe p id Necessary ? *) + +let input_universe : universe_decl -> Libobject.obj = declare_object { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> cache_universes pi); - load_function = (fun _ (_, pi) -> cache_universes pi); + cache_function = cache_universe; + load_function = load_universe; + open_function = open_universe; discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); - classify_function = (fun a -> Keep a) } + subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let add_universe poly (id, lev) = + ignore(Lib.add_leaf id (input_universe (poly, lev))) let do_universe poly l = let in_section = Lib.sections_are_opened () in @@ -484,11 +507,11 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.fold_left (fun acc (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - Id.Map.add id lev acc) Id.Map.empty l + List.map (fun (l, id) -> + let lev = Universes.new_univ_id () in + (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (poly, l)) + List.iter (add_universe poly) l type constraint_decl = polymorphic * Univ.constraints @@ -510,20 +533,15 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } +let loc_of_glob_level = function + | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n + | _ -> None + let do_constraint poly l = - let open Misctypes in let u_of_id x = - match x with - | GProp -> Loc.tag (false, Univ.Level.prop) - | GSet -> Loc.tag (false, Univ.Level.set) - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"Constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - let names, _ = Global.global_universe_names () in - try loc, Id.Map.find id names - with Not_found -> - user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id) + let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in + let loc = loc_of_glob_level x in + loc, Universes.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -541,7 +559,7 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in check_poly ?loc:ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l -- cgit v1.2.3