1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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
(* object_kind , id *)
exception AlreadyDeclared of (string option * Id.t)
let _ = CErrors.register_handler (function
| AlreadyDeclared (kind, id) ->
Some
Pp.(seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
; Id.print id; str " already exists."])
| _ ->
None)
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 *)
type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
let check_exists_universe sp =
if Nametab.exists_universe sp then
raise (AlreadyDeclared (Some "Universe", Libnames.basename sp))
else ()
let qualify_univ i dp src id =
match src with
| BoundUniv | UnqualifiedUniv ->
i, Libnames.make_path dp id
| QualifiedUniv l ->
let dp = DirPath.repr dp in
Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
let do_univ_name ~check i dp src (id,univ) =
let i, sp = qualify_univ i dp src id in
if check then check_exists_universe sp;
Nametab.push_universe i sp univ
let cache_univ_names ((sp, _), (src, univs)) =
let depth = Lib.sections_depth () in
let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in
List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
let load_univ_names i ((sp, _), (src, univs)) =
List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs
let open_univ_names i ((sp, _), (src, univs)) =
List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs
let discharge_univ_names = function
| _, (BoundUniv, _) -> None
| _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
let input_univ_names : universe_name_decl -> Libobject.obj =
let open Libobject in
declare_object
{ (default_object "Global universe name state") with
cache_function = cache_univ_names;
load_function = load_univ_names;
open_function = simple_open open_univ_names;
discharge_function = discharge_univ_names;
subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
()
else
let l = let open GlobRef in match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
| IndRef (c, _) -> Label.to_id @@ MutInd.label c
| VarRef id ->
CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
| ConstructRef _ ->
CErrors.anomaly ~label:"declare_univ_binders"
Pp.(str "declare_univ_binders on a constructor reference")
in
let univs = Id.Map.fold (fun id univ univs ->
match Univ.Level.name univ with
| None -> assert false (* having Prop/Set/Var as binders is nonsense *)
| Some univ -> (id,univ)::univs) pl []
in
Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
let do_universe ~poly l =
let in_section = Global.sections_are_opened () in
let () =
if poly && not in_section then
CErrors.user_err ~hdr:"Constraint"
(Pp.str"Cannot declare polymorphic universes outside sections")
in
let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
Univ.LSet.empty l, Univ.Constraint.empty
in
let src = if poly then BoundUniv else UnqualifiedUniv in
let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
DeclareUctx.declare_universe_context ~poly ctx
let do_constraint ~poly l =
let open Univ in
let u_of_id x =
Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
in
let constraints = List.fold_left (fun acc (l, d, r) ->
let lu = u_of_id l and ru = u_of_id r in
Constraint.add (lu, d, ru) acc)
Constraint.empty l
in
let uctx = ContextSet.add_constraints constraints ContextSet.empty in
DeclareUctx.declare_universe_context ~poly uctx
|
