diff options
| author | Pierre-Marie Pédrot | 2017-11-02 16:33:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-11-02 16:40:57 +0100 |
| commit | 2d0336671971489f217d666afde6537295b8c44a (patch) | |
| tree | 31835815b50cc8f52865c4ba0545ba944531df86 /src | |
| parent | 7e7964ddcc41363151d95cddd1a68b3dc70bb070 (diff) | |
Factorizing entries for patterns with type constraints.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index fca1b3045c..080fba7103 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -127,9 +127,19 @@ GEXTEND Gram [ "_" -> Loc.tag ~loc:!@loc @@ CPatVar Anonymous | "()" -> Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), []) | id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id - | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> - Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl) ] - ] + | "("; p = atomic_tac2pat; ")" -> p + ] ] + ; + atomic_tac2pat: + [ [ -> + Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), []) + | p = tac2pat; ":"; t = tac2type -> + Loc.tag ~loc:!@loc @@ CPatCnv (p, t) + | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," -> + let pl = p :: pl in + Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl) + | p = tac2pat -> p + ] ] ; tac2expr: [ "6" RIGHTA @@ -257,12 +267,7 @@ GEXTEND Gram | l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ] ; input_fun: - [ [ b = tac2pat LEVEL "0" -> b - | "("; b = tac2pat; t = OPT [ ":"; t = tac2type -> t ]; ")" -> - match t with - | None -> b - | Some t -> Loc.tag ~loc:!@loc @@ CPatCnv (b, t) - ] ] + [ [ b = tac2pat LEVEL "0" -> b ] ] ; tac2def_body: [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr -> |