aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml36
-rw-r--r--interp/notation.ml11
-rw-r--r--interp/notation.mli2
-rw-r--r--intf/notation_term.ml5
-rw-r--r--parsing/egramcoq.ml6
-rw-r--r--parsing/egramcoq.mli2
-rw-r--r--test-suite/bugs/closed/5608.v33
-rw-r--r--test-suite/output/Notations3.out11
-rw-r--r--test-suite/output/Notations3.v22
-rw-r--r--theories/Init/Notations.v3
-rw-r--r--vernac/metasyntax.ml142
11 files changed, 149 insertions, 124 deletions
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,4 +1,9 @@
(**********************************************************************)
+(* 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 *)
(* different instances of ".." *)
@@ -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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 12:16:29 +0000