Notation: option to attach extra pretty printing rules to notations

so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).

Available syntax:
- all in one:
  Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
  Format Notation "a /\ b" "latex" "#1 \wedge #2".

9 files changed, 76 insertions, 33 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index e765701d48..93e6f31c03 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -940,17 +940,28 @@ let pr_visibility prglob = function
 (* Mapping notations to concrete syntax *)
 
 type unparsing_rule = unparsing list * precedence
-
+type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let printing_rules =
-  ref (String.Map.empty : unparsing_rule String.Map.t)
+  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
 
-let declare_notation_printing_rule ntn unpl =
-  printing_rules := String.Map.add ntn unpl !printing_rules
+let declare_notation_printing_rule ntn ~extra unpl =
+  printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
 
 let find_notation_printing_rule ntn =
-  try String.Map.find ntn !printing_rules
+  try fst (String.Map.find ntn !printing_rules)
   with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
+let find_notation_extra_printing_rules ntn =
+  try snd (String.Map.find ntn !printing_rules)
+  with Not_found -> []
+let add_notation_extra_printing_rule ntn k v =
+  try
+    printing_rules := 
+      let p, pp = String.Map.find ntn !printing_rules in
+      String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+  with Not_found ->
+    user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
+      str "No such Notation.")
 
 (**********************************************************************)
 (* Synchronisation with reset *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 95e176064c..961e1e12ea 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -185,8 +185,12 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
-val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+type extra_unparsing_rules = (string * string) list
+val declare_notation_printing_rule :
+  notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
 (** Rem: printing rules for primitive token are canonical *)
 
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index e670f68c21..2c73a974b5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -206,7 +206,7 @@ type syntax_modifier =
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing of Flags.compat_version
-  | SetFormat of string located
+  | SetFormat of string * string located
 
 type proof_end =
   | Admitted
@@ -290,6 +290,7 @@ type vernac_expr =
   | VernacNotation of
       obsolete_locality * constr_expr * (lstring * syntax_modifier list) *
       scope_name option
+  | VernacNotationAddFormat of string * string * string
 
   (* Gallina *)
   | VernacDefinition of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 955179ba0d..cabb09dc3e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1026,6 +1026,8 @@ GEXTEND Gram
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
            VernacNotation (local,c,(s,modl),sc)
+     | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
+           VernacNotationAddFormat (n,s,fmt)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
@@ -1072,7 +1074,11 @@ GEXTEND Gram
         SetOnlyParsing Flags.Current
       | IDENT "compat"; s = STRING ->
         SetOnlyParsing (Coqinit.get_compat_version s)
-      | IDENT "format"; s = [s = STRING -> (!@loc,s)] -> SetFormat s
+      | IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
+                        s2 = OPT [s = STRING -> (!@loc,s)] ->
+          begin match s1, s2 with
+          | (_,k), Some s -> SetFormat(k,s)
+          | s, None -> SetFormat ("text",s) end
       | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
         lev = level -> SetItemLevel (x::l,lev)
       | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8ca05f2cad..b841c19cc3 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -344,7 +344,8 @@ let pr_syntax_modifier = function
   | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
   | SetOnlyParsing Flags.Current -> str"only parsing"
   | SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"")
-  | SetFormat s -> str"format " ++ pr_located qs s
+  | SetFormat("text",s) -> str"format " ++ pr_located qs s
+  | SetFormat(k,s) -> str"format " ++ qs k ++ spc() ++ pr_located qs s
 
 let pr_syntax_modifiers = function
   | [] -> mt()
@@ -571,6 +572,8 @@ let rec pr_vernac = function
   | VernacSyntaxExtension (_,(s,l)) ->
       str"Reserved Notation" ++ spc() ++ pr_located qs s ++
       pr_syntax_modifiers l
+  | VernacNotationAddFormat(s,k,v) ->
+      str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
 
   (* Gallina *)
   | VernacDefinition (d,id,b) -> (* A verifier... *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 794fabc910..e810e59072 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -178,7 +178,7 @@ let rec classify_vernac e =
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
-    | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ 
+    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
     | VernacDeclareTacticDefinition _ | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c674fddb4c..905df5f2bc 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -790,6 +790,7 @@ type syntax_extension = {
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
+  synext_extra : (string * string) list;
 }
 
 type syntax_extension_obj = locality_flag * syntax_extension list
@@ -806,7 +807,8 @@ let cache_one_syntax_extension se =
     (* Declare the parsing rule *)
     Egramcoq.extend_constr_grammar prec se.synext_notgram;
     (* Declare the printing rule *)
-    Notation.declare_notation_printing_rule ntn (se.synext_unparsing, fst prec)
+    Notation.declare_notation_printing_rule ntn
+      ~extra:se.synext_extra (se.synext_unparsing, fst prec)
 
 let cache_syntax_extension (_, (_, sy)) =
   List.iter cache_one_syntax_extension sy
@@ -839,38 +841,40 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
 
 let interp_modifiers modl =
   let onlyparsing = ref false in
-  let rec interp assoc level etyps format = function
+  let rec interp assoc level etyps format extra = function
     | [] ->
-	(assoc,level,etyps,!onlyparsing,format)
+	(assoc,level,etyps,!onlyparsing,format,extra)
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
 	  error (s^" is already assigned to an entry or constr level.");
-	interp assoc level ((id,typ)::etyps) format l
+	interp assoc level ((id,typ)::etyps) format extra l
     | SetItemLevel ([],n) :: l ->
-	interp assoc level etyps format l
+	interp assoc level etyps format extra l
     | SetItemLevel (s::idl,n) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
 	  error (s^" is already assigned to an entry or constr level.");
 	let typ = ETConstr (n,()) in
-	interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
+	interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
 	if not (Option.is_empty level) then error "A level is given more than once.";
-	interp assoc (Some n) etyps format l
+	interp assoc (Some n) etyps format extra l
     | SetAssoc a :: l ->
 	if not (Option.is_empty assoc) then error"An associativity is given more than once.";
-	interp (Some a) level etyps format l
+	interp (Some a) level etyps format extra l
     | SetOnlyParsing _ :: l ->
 	onlyparsing := true;
-	interp assoc level etyps format l
-    | SetFormat s :: l ->
+	interp assoc level etyps format extra l
+    | SetFormat ("text",s) :: l ->
 	if not (Option.is_empty format) then error "A format is given more than once.";
-	interp assoc level etyps (Some s) l
-  in interp None None [] None modl
+	interp assoc level etyps (Some s) extra l
+    | SetFormat (k,(_,s)) :: l ->
+	interp assoc level etyps format ((k,s) :: extra) l
+  in interp None None [] None [] modl
 
 let check_infix_modifiers modifiers =
-  let (assoc,level,t,b,fmt) = interp_modifiers modifiers in
+  let (assoc,level,t,b,fmt,extra) = interp_modifiers modifiers in
   if not (List.is_empty t) then
     error "Explicit entry level or type unexpected in infix notation."
 
@@ -1035,7 +1039,7 @@ let remove_curly_brackets l =
   in aux true l
 
 let compute_syntax_data df modifiers =
-  let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
+  let (assoc,n,etyps,onlyparse,fmt,extra) = interp_modifiers modifiers in
   let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
   let toks = split_notation_string df in
   let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -1062,16 +1066,16 @@ let compute_syntax_data df modifiers =
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
   (* Return relevant data for interpretation and for parsing/printing *)
-  (msgs,i_data,i_typs,sy_fulldata)
+  (msgs,i_data,i_typs,sy_fulldata,extra)
 
 let compute_pure_syntax_data df mods =
-  let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data df mods in
+  let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
   let msgs =
     if onlyparse then
       (msg_warning,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
-  msgs, sy_data
+  msgs, sy_data, extra
 
 (**********************************************************************)
 (* Registration of notations interpretation                            *)
@@ -1154,11 +1158,13 @@ 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_extra_rules = Notation.find_notation_extra_printing_rules ntn in
     let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
     { synext_level = prec;
       synext_notation = ntn;
       synext_notgram = pa_rule;
-      synext_unparsing = pp_rule; }
+      synext_unparsing = pp_rule;
+      synext_extra = pp_extra_rules }
   with Not_found ->
     raise NoSyntaxRule
 
@@ -1190,7 +1196,7 @@ let make_pp_rule (n,typs,symbols,fmt) =
   | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
   | 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) =
+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 sy = {
@@ -1198,6 +1204,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
     synext_notation = ntn;
     synext_notgram = pa_rule;
     synext_unparsing = pp_rule;
+    synext_extra = extra;
   } 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
@@ -1212,9 +1219,9 @@ let to_map l =
   List.fold_left fold Id.Map.empty l
 
 let add_notation_in_scope local df c mods scope =
-  let (msgs,i_data,i_typs,sy_data) = compute_syntax_data df mods in
+  let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
   (* Prepare the parsing and printing rules *)
-  let sy_rules = make_syntax_rules sy_data in
+  let sy_rules = make_syntax_rules sy_data extra in
   (* Prepare the interpretation *)
   let (onlyparse, recvars,mainvars, df') = i_data in
   let i_vars = make_internalization_vars recvars mainvars i_typs in
@@ -1276,8 +1283,8 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
 (* Notations without interpretation (Reserved Notation) *)
 
 let add_syntax_extension local ((loc,df),mods) =
-  let msgs, sy_data = compute_pure_syntax_data df mods in
-  let sy_rules = make_syntax_rules sy_data in
+  let msgs, sy_data, extra = compute_pure_syntax_data df mods in
+  let sy_rules = make_syntax_rules sy_data extra in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
@@ -1311,6 +1318,13 @@ let add_notation local c ((loc,df),modifiers) sc =
   in
   Dumpglob.dump_notation (loc,df') sc true
 
+let add_notation_extra_printing_rule df k v =
+  let notk = 
+    let dfs = split_notation_string df in
+    let _,_, symbs = analyze_notation_tokens dfs in
+    make_notation_key symbs in
+  Notation.add_notation_extra_printing_rule notk k v
+
 (* Infix notations *)
 
 let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f48c4a700c..07428c86fa 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -34,6 +34,8 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
 val add_notation : locality_flag -> constr_expr ->
   (lstring * syntax_modifier list) -> scope_name option -> unit
 
+val add_notation_extra_printing_rule : string -> string -> string -> unit
+
 (** Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9aa43bd420..63253d54ea 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1770,6 +1770,8 @@ let interp ?proof locality poly c =
   | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc
   | VernacNotation (local,c,infpl,sc) ->
       vernac_notation locality local c infpl sc
+  | VernacNotationAddFormat(n,k,v) ->
+      Metasyntax.add_notation_extra_printing_rule n k v
 
   (* Gallina *)
   | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d