diff options
Diffstat (limited to 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 38 |
1 files changed, 23 insertions, 15 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index bd88570224..79cfe33b12 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -133,7 +133,8 @@ let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None } GRAMMAR EXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + GLOBAL: binder_constr lconstr constr operconstr + universe_level universe_name sort sort_family global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; @@ -153,11 +154,12 @@ GRAMMAR EXTEND Gram [ [ c = lconstr -> { c } ] ] ; sort: - [ [ "Set" -> { GSet } - | "Prop" -> { GProp } - | "SProp" -> { GSProp } - | "Type" -> { GType [] } - | "Type"; "@{"; u = universe; "}" -> { GType u } + [ [ "Set" -> { UNamed [GSet,0] } + | "Prop" -> { UNamed [GProp,0] } + | "SProp" -> { UNamed [GSProp,0] } + | "Type" -> { UAnonymous {rigid=true} } + | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} } + | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ] ; sort_family: @@ -167,11 +169,17 @@ GRAMMAR EXTEND Gram | "Type" -> { Sorts.InType } ] ] ; + universe_increment: + [ [ "+"; n = natural -> { n } + | -> { 0 } ] ] + ; + universe_name: + [ [ id = global -> { GType id } + | "Set" -> { GSet } + | "Prop" -> { GProp } ] ] + ; universe_expr: - [ [ id = global; "+"; n = natural -> { Some (id,n) } - | id = global -> { Some (id,0) } - | "_" -> { None } - ] ] + [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ] ; universe: [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } @@ -328,12 +336,12 @@ GRAMMAR EXTEND Gram | -> { None } ] ] ; universe_level: - [ [ "Set" -> { GSet } + [ [ "Set" -> { UNamed GSet } (* no parsing SProp as a level *) - | "Prop" -> { GProp } - | "Type" -> { GType UUnknown } - | "_" -> { GType UAnonymous } - | id = global -> { GType (UNamed id) } + | "Prop" -> { UNamed GProp } + | "Type" -> { UAnonymous {rigid=true} } + | "_" -> { UAnonymous {rigid=false} } + | id = global -> { UNamed (GType id) } ] ] ; fix_constr: |