diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 45 |
1 files changed, 22 insertions, 23 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7e5933cea2..9f12db649b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -120,7 +120,7 @@ let name_colon = | _ -> err ()) | _ -> err ()) -let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None +let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family @@ -155,9 +155,15 @@ GEXTEND Gram | "Type" -> Sorts.InType ] ] ; + universe_expr: + [ [ id = global; "+"; n = natural -> Some (id,n) + | id = global -> Some (id,0) + | "_" -> None + ] ] + ; universe: - [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids - | id = name -> [id] + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids + | u = universe_expr -> [u] ] ] ; lconstr: @@ -210,9 +216,11 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c.CAst.v with | CPrim (Numeral (n,true)) -> - CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) + CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c + | "{"; c = binder_constr ; "}" -> + CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) | "`{"; c = operconstr LEVEL "200"; "}" -> CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> @@ -261,17 +269,17 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -307,8 +315,9 @@ GEXTEND Gram universe_level: [ [ "Set" -> GSet | "Prop" -> GProp - | "Type" -> GType None - | id = name -> GType (Some id) + | "Type" -> GType UUnknown + | "_" -> GType UAnonymous + | id = global -> GType (UNamed id) ] ] ; fix_constr: @@ -355,7 +364,7 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ] + [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; @@ -378,19 +387,9 @@ GEXTEND Gram | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ p = pattern; "as"; id = ident -> - CAst.make ~loc:!@loc @@ CPatAlias (p, id) - | p = pattern; lp = LIST1 NEXT -> - (let open CAst in match p with - | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) - | { v = CPatCstr (r, None, l2); loc } -> - CErrors.user_err ?loc ~hdr:"compound_pattern" - (Pp.str "Nested applications not supported.") - | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) - | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp) - | _ -> CErrors.user_err - ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" - (Pp.str "Such pattern cannot have arguments.")) + [ p = pattern; "as"; na = name -> + CAst.make ~loc:!@loc @@ CPatAlias (p, na) + | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp | "@"; r = Prim.reference; lp = LIST0 NEXT -> CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA |