diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 63 |
1 files changed, 37 insertions, 26 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5edb7b80..7f3a3d10 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -29,7 +29,7 @@ let constr_kw = "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] -let _ = List.iter Lexer.add_keyword constr_kw +let _ = List.iter CLexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c @@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> - Errors.user_err_loc + CErrors.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with @@ -127,15 +127,12 @@ let name_colon = let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr sort global + GLOBAL: binder_constr lconstr constr operconstr universe_level sort global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: - [ [ id = Prim.ident -> id - - (* This is used in quotations and Syntax *) - | id = METAIDENT -> Id.of_string id ] ] + [ [ id = Prim.ident -> id ] ] ; Prim.name: [ [ "_" -> (!@loc, Anonymous) ] ] @@ -218,16 +215,13 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; record_declaration: - [ [ fs = record_fields -> CRecord (!@loc, None, fs) -(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) -(* CRecord (!@loc, Some c, fs) *) - ] ] + [ [ fs = record_fields -> CRecord (!@loc, fs) ] ] ; record_fields: @@ -267,14 +261,14 @@ GEXTEND Gram CLetTuple (!@loc,lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)]) + CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)]) + CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -304,10 +298,10 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 level; "}" -> Some l + [ [ "@{"; l = LIST1 universe_level; "}" -> Some l | -> None ] ] ; - level: + universe_level: [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None @@ -338,11 +332,10 @@ GEXTEND Gram br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ] ; case_item: - [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] - ; - pred_pattern: - [ [ ona = OPT ["as"; id=name -> id]; - ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ] + [ [ c=operconstr LEVEL "100"; + ona = OPT ["as"; id=name -> id]; + ty = OPT ["in"; t=pattern -> t] -> + (c,ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] @@ -386,14 +379,17 @@ GEXTEND Gram | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with - | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp) + | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) + | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc + (cases_pattern_expr_loc p, "compound_pattern", + Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) - | _ -> Errors.user_err_loc + | _ -> CErrors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Such pattern cannot have arguments.")) - |"@"; r = Prim.reference; lp = LIST1 NEXT -> - CPatCstr (!@loc, r, lp, []) ] + |"@"; r = Prim.reference; lp = LIST0 NEXT -> + CPatCstr (!@loc, r, Some lp, []) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ] | "0" @@ -405,6 +401,14 @@ GEXTEND Gram CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> CPatNotation(!@loc,"( _ )",([p],[]),[]) | _ -> p) + | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> + let p = + match p with + CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> + CPatNotation(!@loc,"( _ )",([p],[]),[]) + | _ -> p + in + CPatCast (!@loc, p, ty) | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (!@loc, String s) ] ] ; @@ -480,6 +484,13 @@ GEXTEND Gram List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + | "'"; p = pattern LEVEL "0" -> + let (p, ty) = + match p with + | CPatCast (_, p, ty) -> (p, Some ty) + | _ -> (p, None) + in + [LocalPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: |