diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 09:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:06 +0100 |
| commit | edd0d22429354a5f2c703a8c7bd1f775e2f97d9e (patch) | |
| tree | 865fd16d40f5641cac233f951f951a9a4502159f /plugins/ssrmatching | |
| parent | 398358618bb3eabfe822b79c669703c1c33b67e6 (diff) | |
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.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 17409595a..71e8b4ac4 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -916,7 +916,7 @@ let glob_cpattern gs p = | k, (v, Some t) as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else match t.CAst.v with - | CNotation("( _ in _ )", ([t1; t2], [], [])) -> + | CNotation("( _ in _ )", ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -924,11 +924,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation("( _ as _ )", ([t1; t2], [], [])) -> + | CNotation("( _ as _ )", ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; |