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/constrextern.ml | 36 +--------- interp/notation.ml | 11 ++- interp/notation.mli | 2 +- intf/notation_term.ml | 5 +- parsing/egramcoq.ml | 6 +- parsing/egramcoq.mli | 2 +- test-suite/bugs/closed/5608.v | 33 +++++++++ test-suite/output/Notations3.out | 11 ++- test-suite/output/Notations3.v | 22 ++++-- theories/Init/Notations.v | 3 + vernac/metasyntax.ml | 142 +++++++++++++++++++-------------------- 11 files changed, 149 insertions(+), 124 deletions(-) create mode 100644 test-suite/bugs/closed/5608.v diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 54861ae4c..e85415bed 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args = let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) -let has_curly_brackets ntn = - String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 || - String.is_sub " { _ }" ntn (String.length ntn - 6) || - String.string_contains ~where:ntn ~what:" { _ } ") - -let rec wildcards ntn n = - if Int.equal n (String.length ntn) then [] - else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l -and spaces ntn n = - if Int.equal n (String.length ntn) then [] - else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1) - -let expand_curly_brackets loc mknot ntn l = - let ntn' = ref ntn in - let rec expand_ntn i = - function - | [] -> [] - | a::l -> - let a' = - let p = List.nth (wildcards !ntn' 0) i - 2 in - if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p - then begin - ntn' := - String.sub !ntn' 0 p ^ "_" ^ - String.sub !ntn' (p+5) (String.length !ntn' -p-5); - mknot (loc,"{ _ }",[a]) end - else a in - a' :: expand_ntn (i+1) l in - let l = expand_ntn 0 l in - (* side effect *) - mknot (loc,!ntn',l) - let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None @@ -367,9 +335,7 @@ let is_zero s = in aux 0 let make_notation_gen loc ntn mknot mkprim destprim l = - if has_curly_brackets ntn - then expand_curly_brackets loc mknot ntn l - else match ntn,List.map destprim l with + match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> mknot (loc,ntn,([mknot (loc,"( _ )",l)])) 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 () diff --git a/interp/notation.mli b/interp/notation.mli index e63ad10cd..5f6bfa35f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -21,7 +21,7 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list +type level = precedence * tolerability list * notation_var_internalization_type list type delimiters = string type scope type scopes (** = [scope_name list] *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cee96040b..084a1042c 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -88,11 +88,12 @@ type grammar_constr_prod_item = concat with last parsed list when true; additionally release the p last items as if they were parsed autonomously *) -type notation_grammar = { +type one_notation_grammar = { notgram_level : int; notgram_assoc : Extend.gram_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; notgram_typs : notation_var_internalization_type list; - notgram_onlyprinting : bool; } + +type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ec422c58d..1b38a013c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -464,7 +464,7 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () -let extend_constr_notation (_, ng) state = +let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> default_constr_levels | Some lev -> lev @@ -476,7 +476,7 @@ let extend_constr_notation (_, ng) state = let state = GramState.set state constr_levels levels in (r @ r', state) -let constr_grammar : (Notation.level * notation_grammar) grammar_command = +let constr_grammar : one_notation_grammar grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 248de3348..8e0469275 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -13,5 +13,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v new file mode 100644 index 000000000..f02eae69c --- /dev/null +++ b/test-suite/bugs/closed/5608.v @@ -0,0 +1,33 @@ +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). +Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). + +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Inductive base_type := TZ | TWord (logsz : nat). +Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type). +Context {var : base_type -> Type}. +Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : +flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type +interp_base_type y) + end. +Inductive exprf : flat_type -> Type := +| Var {t} (v : var t) : exprf (Tbase t) +| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : +exprf tC +| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). +Global Arguments Var {_} _. +Global Arguments LetIn {_} _ {_} _. +Global Arguments Pair {_} _ {_} _. +Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A +(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Definition foo := + (fun x3 => + (LetIn (Var x3) (fun x18 : var TZ + => (Pair (Var x18) (Var x18))))). +Print foo. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9ae74fd6..c66f80122 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -1,3 +1,5 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set [<0, 2 >] : nat * nat * (nat * nat) [<0, 2 >] @@ -109,9 +111,12 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) -{0, 1} +{{0, 1}} : nat * nat -{0, 1, 2} +{{0, 1, 2}} : nat * (nat * nat) -{0, 1, 2, 3} +{{0, 1, 2, 3}} : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dee0f70f7..58f9e15ab 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -1,3 +1,8 @@ +(**********************************************************************) +(* Check precedence, spacing, etc. in printing with curly brackets *) + +Check {x|x=0}+{True/\False}+{forall x, x=0}. + (**********************************************************************) (* Check printing of notations with several instances of a recursive pattern *) (* Was wrong but I could not trigger a problem due to the collision between *) @@ -161,10 +166,17 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). -(**********************************************************************) (* Test recursive notations with the recursive pattern repeated on the right *) -Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). -Check {0,1}. -Check {0,1,2}. -Check {0,1,2,3}. +Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..). +Check {{0,1}}. +Check {{0,1,2}}. +Check {{0,1,2,3}}. + +(* Test printing of #5608 *) + +Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := + (let x:=a in ( .. (b0,b1) .., b2)). +Check letpair x [1] = {0}; return (1,2,3,4). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index e67ae6a92..5e8d2faa5 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -66,6 +66,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99). (** Notations for sigma-types or subsets *) +Reserved Notation "{ A } + { B }" (at level 50, left associativity). +Reserved Notation "A + { B }" (at level 50, left associativity). + Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c0974d0a7..76c5dc1be 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -705,16 +705,22 @@ let recompute_assoc typs = (**************************************************************************) (* Registration of syntax extensions (parsing/printing, no interpretation)*) -let pr_arg_level from = function +let pr_arg_level from (lev,typ) = + let pplev = match lev with | (n,L) when Int.equal n from -> str "at next level" | (n,E) -> str "at level " ++ int n | (n,L) -> str "at level below " ++ int n | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" - -let pr_level ntn (from,args) = + | (n,_) -> str "Unknown level" in + let pptyp = match typ with + | NtnInternTypeConstr -> mt () + | NtnInternTypeBinder -> str " " ++ surround (str "binder") + | NtnInternTypeIdent -> str " " ++ surround (str "ident") in + pplev ++ pptyp + +let pr_level ntn (from,args,typs) = str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ - prlist_with_sep pr_comma (pr_arg_level from) args + prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs) let error_incompatible_level ntn oldprec prec = user_err @@ -736,12 +742,12 @@ let is_active_compat = function | None -> true | Some v -> 0 <= Flags.version_compare v !Flags.compat_version -type syntax_extension_obj = locality_flag * syntax_extension list +type syntax_extension_obj = locality_flag * syntax_extension let cache_one_syntax_extension se = let ntn = se.synext_notation in let prec = se.synext_level in - let onlyprint = se.synext_notgram.notgram_onlyprinting in + let onlyprint = fst se.synext_notgram in try let oldprec = Notation.level_of_notation ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec @@ -750,25 +756,24 @@ let cache_one_syntax_extension se = (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + if not onlyprint then List.iter Egramcoq.extend_constr_grammar (snd se.synext_notgram); (* Declare the notation rule *) Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram end let cache_syntax_extension (_, (_, sy)) = - List.iter cache_one_syntax_extension sy + cache_one_syntax_extension sy let subst_parsing_rule subst x = x let subst_printing_rule subst x = x let subst_syntax_extension (subst, (local, sy)) = - let map sy = { sy with - synext_notgram = subst_parsing_rule subst sy.synext_notgram; + (local, { sy with + synext_notgram = (fst sy.synext_notgram, List.map (subst_parsing_rule subst) (snd sy.synext_notgram)); synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - } in - (local, List.map map sy) + }) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -1091,8 +1096,10 @@ module SynData = struct (* Notation data for parsing *) level : int; - syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) - symbol list; (* symbols *) + pa_syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) + symbol list; (* symbols *) + pp_syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) + symbol list; (* symbols *) not_data : notation * (* notation *) (int * parenRelation) list * (* precedence *) bool; (* needs_squash *) @@ -1100,6 +1107,18 @@ module SynData = struct end +let find_subentry_types n assoc etyps symbols = + let innerlevel = NumLevel 200 in + let typs = + find_symbols + (NumLevel n,BorderProd(Left,assoc)) + (innerlevel,InternalProd) + (NumLevel n,BorderProd(Right,assoc)) + symbols in + let sy_typs = List.map (set_entry_type etyps) typs in + let prec = List.map (assoc_of_type n) sy_typs in + sy_typs, prec + let compute_syntax_data df modifiers = let open SynData in let open NotationMods in @@ -1115,26 +1134,23 @@ let compute_syntax_data df modifiers = (* Notations for interp and grammar *) let ntn_for_interp = make_notation_key symbols in - let symbols' = remove_curly_brackets symbols in - let ntn_for_grammar = make_notation_key symbols' in - if not onlyprint then check_rule_productivity symbols'; - - (* Misc *) - let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in - let msgs,n = find_precedence mods.level mods.etyps symbols' in - let innerlevel = NumLevel 200 in - let typs = - find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) - symbols' in + let symbols_for_grammar = remove_curly_brackets symbols in + let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in + let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in + if not onlyprint then check_rule_productivity symbols_for_grammar; + let msgs,n = find_precedence mods.level mods.etyps symbols in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in - let sy_typs = List.map (set_entry_type etyps) typs in - let prec = List.map (assoc_of_type n) sy_typs in + let sy_typs, prec = + find_subentry_types n assoc etyps symbols in + let sy_typs_for_grammar, prec_for_grammar = + if need_squash then + find_subentry_types n assoc etyps symbols_for_grammar + else + sy_typs, prec in let i_typs = set_internalization_type sy_typs in - let sy_data = (sy_typs,symbols') in + let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in + let pp_sy_data = (sy_typs,symbols) in let sy_fulldata = (ntn_for_grammar,prec,need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in let i_data = ntn_for_interp, df' in @@ -1155,7 +1171,8 @@ let compute_syntax_data df modifiers = intern_typs = i_typs; level = n; - syntax_data = sy_data; + pa_syntax_data = pa_sy_data; + pp_syntax_data = pp_sy_data; not_data = sy_fulldata; } @@ -1236,22 +1253,6 @@ let with_syntax_protection f x = (**********************************************************************) (* Recovering existing syntax *) -let contract_notation ntn = - if String.equal ntn "{ _ }" then ntn else - let rec aux ntn i = - if i <= String.length ntn - 5 then - let ntn' = - if String.is_sub "{ _ }" ntn i && - (i = 0 || ntn.[i-1] = ' ') && - (i = String.length ntn - 5 || ntn.[i+5] = ' ') - then - String.sub ntn 0 i ^ "_" ^ - String.sub ntn (i+5) (String.length ntn -i-5) - else ntn in - aux ntn' (i+1) - else ntn in - aux ntn 0 - exception NoSyntaxRule let recover_syntax ntn = @@ -1272,28 +1273,30 @@ let recover_syntax ntn = let recover_squash_syntax sy = let sq = recover_syntax "{ _ }" in - [sy; sq] + sy :: snd (sq.synext_notgram) -let recover_notation_syntax rawntn = - let ntn = contract_notation rawntn in +let recover_notation_syntax ntn = let sy = recover_syntax ntn in - let need_squash = not (String.equal ntn rawntn) in - let rules = if need_squash then recover_squash_syntax sy else [sy] in - sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting + let onlyprint,_ = sy.synext_notgram in + pi3 sy.synext_level, sy, onlyprint (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule i_typs level (typs,symbols) ntn onlyprint = +let make_pa_rule i_typs level (typs,symbols) ntn need_squash = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - { notgram_level = level; + let sy = { + notgram_level = level; notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; notgram_typs = i_typs; - notgram_onlyprinting = onlyprint; - } + } in + (* By construction, the rule for "{ _ }" is declared, but we need to + redeclare it because the file where it is declared needs not be open + when the current file opens (especially in presence of -nois) *) + if need_squash then recover_squash_syntax sy else [sy] let make_pp_rule level (typs,symbols) fmt = match fmt with @@ -1302,21 +1305,16 @@ let make_pp_rule level (typs,symbols) fmt = (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in - let ntn, prec, need_squash = sd.not_data in - let pa_rule = make_pa_rule sd.intern_typs sd.level sd.syntax_data ntn sd.only_printing in - let pp_rule = make_pp_rule sd.level sd.syntax_data sd.format in - let sy = { - synext_level = (sd.level, prec); - synext_notation = ntn; - synext_notgram = pa_rule; + let ntn_for_grammar, prec, need_squash = sd.not_data in + let pa_rule = make_pa_rule sd.intern_typs sd.level sd.pa_syntax_data ntn_for_grammar need_squash in + let pp_rule = make_pp_rule sd.level sd.pp_syntax_data sd.format in { + synext_level = (sd.level, prec, sd.intern_typs); + synext_notation = fst sd.info; + synext_notgram = (sd.only_printing,pa_rule); synext_unparsing = pp_rule; synext_extra = sd.extra; synext_compat = sd.compat; - } in - (* By construction, the rule for "{ _ }" is declared, but we need to - redeclare it because the file where it is declared needs not be open - when the current file opens (especially in presence of -nois) *) - if need_squash then recover_squash_syntax sy else [sy] + } (**********************************************************************) (* Main functions about notations *) -- cgit v1.2.3