From 765392492df2f5e065b2b5e706b6620846337cc0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 21 Sep 2017 00:53:10 +0200 Subject: Universe binders survive sections, modules and compilation. --- engine/universes.ml | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'engine/universes.ml') diff --git a/engine/universes.ml b/engine/universes.ml index 194de2cee..f2942be6d 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -32,9 +32,37 @@ let universe_binders_of_global ref : universe_binders = let l = Refmap.find ref !universe_binders_table in l with Not_found -> Names.Id.Map.empty -let register_universe_binders ref l = +let cache_ubinder (_,(ref,l)) = universe_binders_table := Refmap.add ref l !universe_binders_table +let subst_ubinder (subst,(ref,l as orig)) = + let ref' = fst (Globnames.subst_global subst ref) in + if ref == ref' then orig else ref', l + +let discharge_ubinder (_,(ref,l)) = + Some (Lib.discharge_global ref, l) + +let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj = + let open Libobject in + declare_object { (default_object "universe binder") with + cache_function = cache_ubinder; + load_function = (fun _ x -> cache_ubinder x); + classify_function = (fun x -> Substitute x); + subst_function = subst_ubinder; + discharge_function = discharge_ubinder; + rebuild_function = (fun x -> x); } + +let register_universe_binders ref ubinders = + (* Add the polymorphic (section) universes *) + let open Names in + let ubinders = Idmap.fold (fun id (poly,lvl) ubinders -> + if poly then Id.Map.add id lvl ubinders + else ubinders) + (fst (Global.global_universe_names ())) ubinders + in + if not (Id.Map.is_empty ubinders) + then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + type univ_name_list = Name.t Loc.located list let universe_binders_with_opt_names ref levels = function -- cgit v1.2.3