aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation.mli2
-rw-r--r--printing/ppconstr.ml17
-rw-r--r--test-suite/output/Notations2.out4
-rw-r--r--test-suite/output/Notations2.v7
-rw-r--r--toplevel/metasyntax.ml24
6 files changed, 41 insertions, 15 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index b8f4f3201..1a2e7074f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -965,7 +965,7 @@ let pr_visibility prglob = function
(**********************************************************************)
(* Mapping notations to concrete syntax *)
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * precedence * tolerability option
type extra_unparsing_rules = (string * string) list
(* Concrete syntax for symbolic-extension table *)
let printing_rules =
diff --git a/interp/notation.mli b/interp/notation.mli
index 480979ccc..352c20313 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -194,7 +194,7 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
(** {6 Printing rules for notations} *)
(** Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * precedence * tolerability option
type extra_unparsing_rules = (string * string) list
val declare_notation_printing_rule :
notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1866ca504..7fad6fb9a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -85,8 +85,8 @@ end) = struct
mt ()
| UnpMetaVar (_, prec) as unp :: l ->
let c = pop env in
+ let pp1= pr (n, prec) c in
let pp2 = aux l in
- let pp1 = pr (n, prec) c in
return unp pp1 pp2
| UnpListMetaVar (_, prec, sl) as unp :: l ->
let cl = pop envlist in
@@ -95,15 +95,16 @@ end) = struct
return unp pp1 pp2
| UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
let cl = pop bll in
- let pp2 = aux l in
let pp1 = pr_binders (fun () -> aux sl) isopen cl in
+ let pp2 = aux l in
return unp pp1 pp2
| UnpTerminal s as unp :: l ->
- let pp2 = aux l in
let pp1 = str s in
+ let pp2 = aux l in
return unp pp1 pp2
| UnpBox (b,sub) as unp :: l ->
- let pp1 = ppcmd_of_box b (aux sub) in
+ let pp1 = aux sub in
+ let pp1 = ppcmd_of_box b pp1 in
let pp2 = aux l in
return unp pp1 pp2
| UnpCut cut as unp :: l ->
@@ -114,8 +115,12 @@ end) = struct
aux unps
let pr_notation pr pr_binders s env =
- let unpl, level = find_notation_printing_rule s in
- print_hunks level pr pr_binders env unpl, level
+ let unpl, level, trailing_level = find_notation_printing_rule s in
+ let pp = print_hunks level pr pr_binders env unpl in
+ let level = match trailing_level with
+ | Some (level',_) -> max level level'
+ | _ -> level in
+ pp, level
let pr_delimiters key strm =
strm ++ str ("%"^key)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d3837..593a5df84 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,7 @@ end
: ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
exist (Q x) y conj
: {x0 : A | Q x x0}
+fun x : nat => (## x) + x
+ : nat -> nat
+fun x : nat => ## x + x
+ : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7..d32758375 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,10 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
Check (exist (Q x) y conj).
+
+(* Check printing of notations that have arguments at higher level
+ than the notation itself *)
+
+Notation "## a" := (S a) (at level 0, a at level 100).
+Check fun x => (S x) + x.
+Check fun x => S (x + x).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7c1f05cd3..e0cdc1b62 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -479,6 +479,14 @@ let make_hunks etyps symbols from =
in make symbols
+let rec trailing_precedence etyps from = function
+ | [] -> assert false
+ | [NonTerminal id|SProdList (id,_)] ->
+ let typ = List.assoc id etyps in
+ Some (precedence_of_entry_type from typ)
+ | [Terminal _|Break _] -> None
+ | _ :: l -> trailing_precedence etyps from l
+
(* Build default printing rules from explicit format *)
let error_format () = error "The format does not match the notation."
@@ -672,7 +680,7 @@ type syntax_extension = {
synext_level : Notation.level;
synext_notation : notation;
synext_notgram : notation_grammar;
- synext_unparsing : unparsing list;
+ synext_unparsing : unparsing_rule;
synext_extra : (string * string) list;
}
@@ -691,7 +699,7 @@ let cache_one_syntax_extension se =
Egramcoq.extend_constr_grammar prec se.synext_notgram;
(* Declare the printing rule *)
Notation.declare_notation_printing_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, fst prec)
+ ~extra:se.synext_extra se.synext_unparsing
let cache_syntax_extension (_, (_, sy)) =
List.iter cache_one_syntax_extension sy
@@ -1051,7 +1059,7 @@ exception NoSyntaxRule
let recover_syntax ntn =
try
let prec = Notation.level_of_notation ntn in
- let pp_rule,_ = Notation.find_notation_printing_rule ntn in
+ let pp_rule= Notation.find_notation_printing_rule ntn in
let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
{ synext_level = prec;
@@ -1085,14 +1093,16 @@ let make_pa_rule i_typs (n,typs,symbols,_) ntn =
notgram_prods = prod;
notgram_typs = i_typs; }
-let make_pp_rule (n,typs,symbols,fmt) =
- match fmt with
+let make_pp_rule (n,typs,symbols,fmt) (lev,_) =
+ let unp = match fmt with
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
- | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
+ | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) in
+ let trailingprec = trailing_precedence typs lev symbols in
+ (unp, lev, trailingprec)
let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
let pa_rule = make_pa_rule i_typs sy_data ntn in
- let pp_rule = make_pp_rule sy_data in
+ let pp_rule = make_pp_rule sy_data prec in
let sy = {
synext_level = prec;
synext_notation = ntn;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 07:44:32 +0000