diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 20:50:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
| tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /interp/notation.ml | |
| parent | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (diff) | |
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 13ff960f6..ea7ef21b1 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in @@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with - | NtnParsedAsConstr, NtnParsedAsConstr -> true - | NtnParsedAsIdent, NtnParsedAsIdent -> true - | NtnParsedAsPattern, NtnParsedAsPattern -> true - | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true |