diff options
Diffstat (limited to 'engine/univNames.ml')
-rw-r--r-- | engine/univNames.ml | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml new file mode 100644 index 000000000..6ffb4bcf0 --- /dev/null +++ b/engine/univNames.ml @@ -0,0 +1,105 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Univ +open Globnames +open Nametab + + +let reference_of_level l = CAst.make @@ + match Level.name l with + | Some (d, n as na) -> + let qid = + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + in Libnames.Qualid qid + | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) + +let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) + +(** Global universe information outside the kernel, to handle + polymorphic universe names in sections that have to be discharged. *) + +let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) + +let add_global_universe u p = + match Level.name u with + | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map + | None -> () + +let is_polymorphic l = + match Level.name l with + | Some n -> + (try Nametab.UnivIdMap.find n !universe_map + with Not_found -> false) + | None -> false + +(** Local universe names of polymorphic references *) + +type universe_binders = Univ.Level.t Names.Id.Map.t + +let empty_binders = Id.Map.empty + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref : universe_binders = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> Names.Id.Map.empty + +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 : GlobRef.t * 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 ubinders = UnivIdMap.fold (fun lvl poly ubinders -> + let qid = Nametab.shortest_qualid_of_universe lvl in + let level = Level.make (fst lvl) (snd lvl) in + if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders + else ubinders) + !universe_map ubinders + in + if not (Id.Map.is_empty ubinders) + then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + +type univ_name_list = Names.lname list + +let universe_binders_with_opt_names ref levels = function + | None -> universe_binders_of_global ref + | Some udecl -> + if Int.equal(List.length levels) (List.length udecl) + then + List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with + | Anonymous -> acc + | Name na -> Names.Id.Map.add na lvl acc) + empty_binders udecl levels + else + CErrors.user_err ~hdr:"universe_binders_with_opt_names" + Pp.(str "Universe instance should have length " ++ int (List.length levels)) |