diff options
| author | Hugo Herbelin | 2020-02-11 16:06:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 16:06:45 +0100 |
| commit | 6975536db325a0f4dcbcb609dd8959d45fc19830 (patch) | |
| tree | 895e71bd5d99d838c34eac7696ac3e539b7ca3bf /parsing | |
| parent | 4c6c173447d5b7d04aa0fd4f51d27a078c675708 (diff) | |
| parent | 2c9d58c4680dd3c60dacf387a7ea457584bec42f (diff) | |
Merge PR #11235: Add syntax for non maximal implicit arguments
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
Diffstat (limited to 'parsing')
| -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 |