diff options
-rw-r--r-- | interp/notation.ml | 2 | ||||
-rw-r--r-- | interp/notation.mli | 2 | ||||
-rw-r--r-- | printing/ppconstr.ml | 17 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 7 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 24 |
6 files changed, 15 insertions, 41 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 1a2e7074f..b8f4f3201 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 * tolerability option +type unparsing_rule = unparsing list * precedence 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 352c20313..480979ccc 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 * tolerability option +type unparsing_rule = unparsing list * precedence 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 7fad6fb9a..1866ca504 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,16 +95,15 @@ end) = struct return unp pp1 pp2 | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> let cl = pop bll in - let pp1 = pr_binders (fun () -> aux sl) isopen cl in let pp2 = aux l in + let pp1 = pr_binders (fun () -> aux sl) isopen cl in return unp pp1 pp2 | UnpTerminal s as unp :: l -> - let pp1 = str s in let pp2 = aux l in + let pp1 = str s in return unp pp1 pp2 | UnpBox (b,sub) as unp :: l -> - let pp1 = aux sub in - let pp1 = ppcmd_of_box b pp1 in + let pp1 = ppcmd_of_box b (aux sub) in let pp2 = aux l in return unp pp1 pp2 | UnpCut cut as unp :: l -> @@ -115,12 +114,8 @@ end) = struct aux unps let pr_notation pr pr_binders s env = - 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 unpl, level = find_notation_printing_rule s in + print_hunks level pr pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 593a5df84..6ff1d3837 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -54,7 +54,3 @@ 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 d32758375..4e0d135d7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -106,10 +106,3 @@ 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 e0cdc1b62..7c1f05cd3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -479,14 +479,6 @@ 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." @@ -680,7 +672,7 @@ type syntax_extension = { synext_level : Notation.level; synext_notation : notation; synext_notgram : notation_grammar; - synext_unparsing : unparsing_rule; + synext_unparsing : unparsing list; synext_extra : (string * string) list; } @@ -699,7 +691,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 + ~extra:se.synext_extra (se.synext_unparsing, fst prec) let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -1059,7 +1051,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; @@ -1093,16 +1085,14 @@ 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) (lev,_) = - let unp = match fmt with +let make_pp_rule (n,typs,symbols,fmt) = + 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) in - let trailingprec = trailing_precedence typs lev symbols in - (unp, lev, trailingprec) + | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) 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 prec in + let pp_rule = make_pp_rule sy_data in let sy = { synext_level = prec; synext_notation = ntn; |