Skip to content

Commit 26bf881

Browse files
TDiazTTDiazT
committed
feat: Use Univ / Univ@{s;l} / Univ@{l} for sort polymorphism
fix: Make implicit Type not collapse with flag
1 parent d424a8f commit 26bf881

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

65 files changed

+450
-451
lines changed

‎doc/sphinx/language/core/sorts.rst‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ Sorts
1717
| SProp
1818
| Type
1919
| Type @%{ _ %}
20-
| Type @%{ {? @qualid {| %| | ; } } @universe %}
20+
| Univ @%{ @qualid ; @universe_opt %}
21+
| Univ
2122
universe ::= max ( {+, @universe_expr } )
22-
| _
2323
| @universe_expr
2424
universe_expr ::= @universe_name {? + @natural }
2525
| @natural

‎doc/tools/docgram/common.edit_mlg‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,6 @@ DELETE: [
168168
| test_variance_ident
169169
| test_qualid_with_or_lpar_or_rbrac
170170
| test_leftsquarebracket_equal
171-
| test_old_sort_qvar
172171
| test_sort_qvar
173172
| test_ltac2_ident
174173
| test_doublepipe_univ_decl
@@ -336,10 +335,8 @@ scope_delimiter: [
336335
]
337336

338337
sort: [
339-
| REPLACE "Type" "@{" reference ";" universe "}"
340-
| WITH "Type" "@{" OPT [ qualid [ "|" | ";" ] ] universe "}"
341338
| DELETE "Type" "@{" universe "}"
342-
| DELETE "Type" "@{" reference "|" universe "}"
339+
| DELETE "Univ" "@{" universe "}"
343340
]
344341

345342
term100: [

‎doc/tools/docgram/fullGrammar‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,10 @@ sort: [
2727
| "SProp"
2828
| "Type"
2929
| "Type" "@{" "_" "}"
30-
| "Type" "@{" test_old_sort_qvar reference "|" universe "}"
31-
| "Type" "@{" test_sort_qvar reference ";" universe "}"
3230
| "Type" "@{" universe "}"
31+
| "Univ" "@{" test_sort_qvar reference ";" universe_opt "}"
32+
| "Univ" "@{" universe "}"
33+
| "Univ"
3334
]
3435

3536
sort_quality_or_set: [
@@ -62,9 +63,13 @@ universe_expr: [
6263
| natural
6364
]
6465

66+
universe_opt: [
67+
| universe
68+
| "_"
69+
]
70+
6571
universe: [
6672
| "max" "(" LIST1 universe_expr SEP "," ")"
67-
| "_"
6873
| universe_expr
6974
]
7075

‎doc/tools/docgram/orderedGrammar‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -280,12 +280,12 @@ sort: [
280280
| "SProp"
281281
| "Type"
282282
| "Type" "@{" "_" "}"
283-
| "Type" "@{" OPT [ qualid [ "|" | ";" ] ] universe "}"
283+
| "Univ" "@{" qualid ";" universe_opt "}"
284+
| "Univ"
284285
]
285286

286287
universe: [
287288
| "max" "(" LIST1 universe_expr SEP "," ")"
288-
| "_"
289289
| universe_expr
290290
]
291291

@@ -294,6 +294,11 @@ universe_expr: [
294294
| natural
295295
]
296296

297+
universe_opt: [
298+
| universe
299+
| "_"
300+
]
301+
297302
universe_name: [
298303
| qualid
299304
| "Set"

‎interp/constrexpr_ops.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ open Constrexpr
2121
(* Universes *)
2222

2323
let expr_Type_sort = None, UAnonymous {rigid=UnivRigid}
24+
let expr_Univ_sort = Some (CQAnon None), UAnonymous { rigid = UnivFlexible false }
2425
let expr_SProp_sort = None, UNamed [CSProp, 0]
2526
let expr_Prop_sort = None, UNamed [CProp, 0]
2627
let expr_Set_sort = None, UNamed [CSet, 0]

‎interp/constrexpr_ops.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ open Constrexpr
1515
(** Constrexpr_ops: utilities on [constr_expr] *)
1616

1717
val expr_Type_sort : sort_expr
18+
val expr_Univ_sort : sort_expr
1819
val expr_SProp_sort : sort_expr
1920
val expr_Prop_sort : sort_expr
2021
val expr_Set_sort : sort_expr

‎parsing/g_constr.mlg‎

Lines changed: 12 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -80,16 +80,10 @@ let test_array_closing =
8080
lk_kw "|" >> lk_kw "]" >> check_no_space
8181
end
8282

83-
let test_old_sort_qvar =
84-
let open Procq.Lookahead in
85-
to_entry "test_old_sort_qvar" begin
86-
lk_ident >> lk_list lk_field >> lk_kw "|"
87-
end
88-
8983
let test_sort_qvar =
9084
let open Procq.Lookahead in
9185
to_entry "test_sort_qvar" begin
92-
lk_ident >> lk_list lk_field >> lk_kw ";"
86+
(lk_ident <+> lk_kw "Type") >> lk_list lk_field >> lk_kws [";"]
9387
end
9488

9589
let warn_old_sort_syntax =
@@ -149,14 +143,11 @@ GRAMMAR EXTEND Gram
149143
| "SProp" -> { None, UNamed [CSProp, 0] }
150144
| "Type" -> { None, UAnonymous {rigid=UnivRigid} }
151145
| "Type"; "@{"; "_"; "}" -> { None, UAnonymous {rigid=UnivFlexible false} }
152-
| "Type"; "@{"; test_old_sort_qvar; q = reference; pipe_loc = [ "|" -> { loc } ]; u = universe; "}" -> {
153-
warn_old_sort_syntax ~loc:pipe_loc ();
154-
Some (CQVar q), u
155-
}
156-
| "Type"; "@{"; test_sort_qvar; q = reference; ";"; u = universe; "}" -> {
157-
Some (CQVar q), u
158-
}
159-
| "Type"; "@{"; u = universe; "}" -> { None, u } ] ]
146+
| "Type"; "@{"; u = universe; "}" -> { None, UNamed u }
147+
| "Univ"; "@{"; test_sort_qvar; q = reference; ";"; u = universe_opt; "}" -> { Some (CQVar q), u }
148+
| "Univ"; "@{"; u = universe; "}" -> { Some (CQAnon (Some loc)), UNamed u }
149+
| "Univ" -> { Some (CQAnon (Some loc)), UAnonymous {rigid=UnivFlexible false} }
150+
] ]
160151
;
161152
sort_quality_or_set:
162153
[ [ "Prop" -> { UnivGen.QualityOrSet.prop }
@@ -183,10 +174,13 @@ GRAMMAR EXTEND Gram
183174
[ [ id = universe_name; n = universe_increment -> { (id,n) }
184175
| n = natural -> { CSet, n } ] ]
185176
;
177+
universe_opt:
178+
[ [ u = universe -> { UNamed u }
179+
| "_" -> { UAnonymous { rigid = UnivFlexible false } } ] ]
180+
;
186181
universe:
187-
[ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
188-
| "_" -> { UAnonymous { rigid = UnivFlexible false } }
189-
| u = universe_expr -> { UNamed [u] } ] ]
182+
[ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
183+
| u = universe_expr -> { [u] } ] ]
190184
;
191185
lconstr:
192186
[ [ c = term LEVEL "200" -> { c } ] ]

‎pretyping/pretyping.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@ type pretype_flags = {
256256

257257
let glob_opt_qvar ?loc ~flags sigma = function
258258
| None ->
259-
if flags.unconstrained_sorts || (not @@ PolyFlags.collapse_sort_variables flags.poly) then
259+
if flags.unconstrained_sorts then
260260
let sigma, q = new_quality_variable ?loc sigma in
261261
sigma, Some q
262262
else sigma, None

‎printing/ppconstr.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,8 @@ let pr_sort_expr : sort_expr -> Pp.t = function
242242
| None, UNamed [CProp, 0] -> tag_type (str "Prop")
243243
| None, UNamed [CSet, 0] -> tag_type (str "Set")
244244
| None, UAnonymous {rigid=UnivRigid} -> tag_type (str "Type")
245-
| u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_quality_univ u)
245+
| None, u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
246+
| u -> hov 0 (tag_type (str "Univ") ++ pr_univ_annot pr_quality_univ u)
246247

247248
let pr_qualid sp =
248249
let (sl, id) = repr_qualid sp in

‎test-suite/bugs/bug_11133.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,16 @@ Module Type Universe.
22
Parameter U : nat.
33
End Universe.
44

5-
Module Univ_prop (Univ : Universe).
6-
Include Univ.
5+
Module Univ_prop (U : Universe).
6+
Include U.
77
End Univ_prop.
88

9-
Module Monad (Univ : Universe).
10-
Module UP := Univ_prop Univ.
9+
Module Monad (U : Universe).
10+
Module UP := Univ_prop U.
1111
End Monad.
1212

13-
Module Rules (Univ:Universe).
14-
Module MP := Monad Univ.
13+
Module Rules (U : Universe).
14+
Module MP := Monad U.
1515
Include MP.
1616
Import UP.
1717
Definition M := UP.U. (* anomaly here *)

0 commit comments

Comments
 (0)