From f442efebd8354b233827e4991a80d27082c772e1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Jul 2017 20:04:46 +0200 Subject: A little reorganization of notations + a fix to #5608. - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation. --- interp/notation.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index c07a00943..c7bf0e36b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -41,7 +41,7 @@ open Context.Named.Declaration (**********************************************************************) (* Scope of symbols *) -type level = precedence * tolerability list +type level = precedence * tolerability list * notation_var_internalization_type list type delimiters = string type notation_location = (DirPath.t * DirPath.t) * string @@ -83,11 +83,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with | Prec l1, Prec l2 -> Int.equal l1 l2 | _ -> false -let level_eq (l1, t1) (l2, t2) = +let notation_var_internalization_type_eq v1 v2 = match v1, v2 with +| NtnInternTypeConstr, NtnInternTypeConstr -> true +| NtnInternTypeBinder, NtnInternTypeBinder -> true +| NtnInternTypeIdent, NtnInternTypeIdent -> true +| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false + +let level_eq (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + && List.equal notation_var_internalization_type_eq u1 u2 let declare_scope scope = try let _ = String.Map.find scope !scope_map in () -- cgit v1.2.3