blob: f806a9f4f76291a0de8ee84f101e67de16dfc6e3 (
plain)
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
Set Universe Polymorphism.
Set Printing Universes.
(* Unset Strict Universe Declaration. *)
(* universe binders on inductive types and record projections *)
Inductive Empty@{u} : Type@{u} := .
Print Empty.
Set Primitive Projections.
Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
Print PWrap.
Print punwrap.
Unset Primitive Projections.
Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
Print RWrap.
Print runwrap.
(* universe binders also go on the constants for operational typeclasses. *)
Class Wrap@{u} (A:Type@{u}) := wrap : A.
Print Wrap.
Print wrap.
(* Instance in lemma mode used to ignore the binders. *)
Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
Print bar.
Unset Strict Universe Declaration.
(* The universes in the binder come first, then the extra universes in
order of appearance. *)
Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
Print foo.
Check Type@{i} -> Type@{j}.
Eval cbv in Type@{i} -> Type@{j}.
Set Strict Universe Declaration.
(* Binders even work with monomorphic definitions! *)
Monomorphic Definition mono@{u} := Type@{u}.
Print mono.
Check mono.
Check Type@{mono.u}.
Module mono.
Fail Monomorphic Universe u.
Monomorphic Universe MONOU.
Monomorphic Definition monomono := Type@{MONOU}.
Check monomono.
Monomorphic Inductive monoind@{i} : Type@{i} := .
Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}.
End mono.
Check mono.monomono. (* qualified MONOU *)
Import mono.
Check monomono. (* unqualified MONOU *)
Check mono. (* still qualified mono.u *)
Monomorphic Constraint Set < Top.mono.u.
Module mono2.
Monomorphic Universe u.
End mono2.
Fail Monomorphic Definition mono2@{u} := Type@{u}.
Module SecLet.
Unset Universe Polymorphism.
Section foo.
(* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
Unset Strict Universe Declaration.
Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
Definition bobmorane := tt -> ff.
End foo.
Print bobmorane. (*
bobmorane@{Top.15 Top.16 ff.u ff.v} =
let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
: Type@{max(Top.15,ff.u)}
(* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
ff.v < ff.u
*)
bobmorane is universe polymorphic
*)
End SecLet.
(* fun x x => foo is nonsense with local binders *)
Fail Definition fo@{u u} := Type@{u}.
(* Using local binders for printing. *)
Print foo@{E M N}.
(* Underscores discard the name if there's one. *)
Print foo@{_ _ _}.
(* Also works for inductives and records. *)
Print Empty@{E}.
Print PWrap@{E}.
(* Also works for About. *)
About punwrap@{K}.
(* Instance length check. *)
Fail Print foo@{E}.
Fail Print mono@{E}.
(* Not everything can be printed with custom universe names. *)
Fail Print Coq.Init.Logic@{E}.
(* Nice error when constraints are impossible. *)
Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
(* Universe binders survive through compilation, sections and modules. *)
Require TestSuite.bind_univs.
Print bind_univs.mono.
Print bind_univs.poly.
Section SomeSec.
Universe u.
Definition insec@{v} := Type@{u} -> Type@{v}.
Print insec.
End SomeSec.
Print insec.
Module SomeMod.
Definition inmod@{u} := Type@{u}.
Print inmod.
End SomeMod.
Print SomeMod.inmod.
Import SomeMod.
Print inmod.
Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
Module SomeFunct (In : SomeTyp).
Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
End SomeFunct.
Module Applied := SomeFunct(SomeMod).
Print Applied.infunct.
(* Multi-axiom declaration
In polymorphic mode the domain Type gets separate universes for the
different axioms, but all axioms have to declare all universes. In
polymorphic mode they get the same universes, ie the type is only
interpd once. *)
Axiom axfoo@{i+} axbar : Type -> Type@{i}.
Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
About axfoo. About axbar. About axfoo'. About axbar'.
Fail Axiom failfoo failbar@{i} : Type.
|
