diff options
| author | SimonBoulier | 2019-12-02 12:52:39 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-02-04 16:07:21 +0100 |
| commit | a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 (patch) | |
| tree | 536f901c47c0080a5bc6a2d3b92adaefbfc8490f /parsing/g_constr.mlg | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
Diffstat (limited to 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index af1e973261..dcc3a87b11 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> - { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } + { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; @@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" -> { [CLocalDef (id,c,Some t)] } | "{"; id = name; "}" -> - { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" -> - { [CLocalAssum (id::idl,Default Implicit,c)] } + { [CLocalAssum (id::idl,Default MaxImplicit,c)] } | "{"; id = name; ":"; c = lconstr; "}" -> - { [CLocalAssum ([id],Default Implicit,c)] } + { [CLocalAssum ([id],Default MaxImplicit,c)] } | "{"; id = name; idl = LIST1 name; "}" -> - { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + | "["; id = name; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" -> + { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] } + | "["; id = name; ":"; c = lconstr; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit,c)] } + | "["; id = name; idl = LIST1 name; "]" -> + { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc } + | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" -> + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with |