diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 83 | ||||
| -rw-r--r-- | interp/declare.mli | 3 |
2 files changed, 66 insertions, 20 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 8fc959b0ff..1aeb67afbb 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -458,33 +458,61 @@ let declare_universe_context poly ctx = used to distinguish universes declared in polymorphic sections, which are discharged and do not remain in scope. *) -type universe_decl = polymorphic * Nametab.universe_id +type universe_source = + | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) + | QualifiedUniv of Id.t (* global universe introduced by some global value *) + | UnqualifiedUniv (* other global universe *) -let add_universe p (dp, i) = +type universe_decl = universe_source * Nametab.universe_id + +let add_universe src (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 optpoly = match src with + | BoundUniv -> Some true + | UnqualifiedUniv -> Some false + | QualifiedUniv _ -> None + in + Option.iter (fun poly -> + let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in + Global.push_context_set poly ctx; + Universes.add_global_universe level poly; + if poly then Lib.add_section_context ctx) + optpoly 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") + if Nametab.exists_universe sp then + alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") else () -let cache_universe ((sp, _), (poly, id)) = +let qualify_univ src (sp,i as orig) = + match src with + | BoundUniv | UnqualifiedUniv -> orig + | QualifiedUniv l -> + let sp0, id = Libnames.repr_path sp in + let sp0 = DirPath.repr sp0 in + Libnames.make_path (DirPath.make (l::sp0)) id, i+1 + +let cache_universe ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,1) in let () = check_exists sp in - let () = Nametab.push_universe (Nametab.Until 1) sp id in - add_universe poly id + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe src id -let load_universe i ((sp, _), (poly, id)) = +let load_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in let () = Nametab.push_universe (Nametab.Until i) sp id in - add_universe poly id + add_universe src id -let open_universe i ((sp, _), (poly, id)) = +let open_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in let () = Nametab.push_universe (Nametab.Exactly i) sp id in - ()(** add_universe p id Necessary ? *) + () + +let discharge_universe = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x let input_universe : universe_decl -> Libobject.obj = declare_object @@ -492,12 +520,28 @@ let input_universe : universe_decl -> Libobject.obj = 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); + discharge_function = discharge_universe; 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 declare_univ_binders gr pl = + if Global.is_polymorphic gr then + Universes.register_universe_binders gr pl + else + let l = match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> id + | ConstructRef _ -> + anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + Id.Map.iter (fun id lvl -> + match Univ.Level.name lvl with + | None -> () + | Some na -> + ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na)))) + pl let do_universe poly l = let in_section = Lib.sections_are_opened () in @@ -511,7 +555,10 @@ let do_universe poly l = let lev = Universes.new_univ_id () in (id, lev)) l in - List.iter (add_universe poly) l + let src = if poly then BoundUniv else UnqualifiedUniv in + List.iter (fun (id,lev) -> + ignore(Lib.add_leaf id (input_universe (src, lev)))) + l type constraint_decl = polymorphic * Univ.constraints diff --git a/interp/declare.mli b/interp/declare.mli index 31883c9d78..f368d164e9 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -80,9 +80,8 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool - - (** Global universe contexts, names and constraints *) +val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit |