From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:32:02 +0200 Subject: Adding patterns in the category of binders for notations. For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"... --- parsing/g_constr.ml4 | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) (limited to 'parsing/g_constr.ml4') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index db68a75e09..4c55f3ec65 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -387,17 +387,7 @@ GEXTEND Gram | "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; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp | "@"; r = Prim.reference; lp = LIST0 NEXT -> CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- parsing/g_constr.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'parsing/g_constr.ml4') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 4c55f3ec65..c2ce003f13 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 @@ -216,7 +216,7 @@ 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 = operconstr LEVEL "200"; "}" -> @@ -385,8 +385,8 @@ GEXTEND Gram | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ p = pattern; "as"; id = ident -> - CAst.make ~loc:!@loc @@ CPatAlias (p, id) + [ 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, []) ] -- cgit v1.2.3 From 0af54860172efe1aa5da419b81e4cb34348320ee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:42:41 +0100 Subject: Trying a hack to support {'pat|P} without breaking compatibility. Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not. --- parsing/g_constr.ml4 | 2 ++ 1 file changed, 2 insertions(+) (limited to 'parsing/g_constr.ml4') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c2ce003f13..9f12db649b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -219,6 +219,8 @@ GEXTEND Gram 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"; ")" -> -- cgit v1.2.3