The Coq mailing list

[tom.prince AT ualberta.net]

From: Tom Prince 
<tom.prince AT ualberta.net>

This adds two option tables 'Printing Record' and 'Printing Constructor'
that forces a given type to always be printed as a record, or with a
constructor, regardless of the setting of 'Printing Records'.
---

And this is that patch that controls printing by type.

 CHANGES                      |    2 +
 doc/refman/RefMan-ext.tex    |   11 ++++++++-
 ide/coq_commands.ml          |    4 +++
 interp/constrextern.ml       |   53 ++++++++++++++++++++++++++++++++++++++++-
 test-suite/output/Record.out |    8 ++++++
 test-suite/output/Record.v   |   10 ++++++++
 tools/coq-syntax.el          |    2 +
 7 files changed, 87 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index 649c43f..dc98c45 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,8 @@ Specification language and notations
 - Added support for recursive notations with binders (allows for instance
   to write "exists x y z, P").
 - Structure/Record printing can be disable by "Unset Printing Records".
+  In addition, it can be controlled on type by type basis using
+  "Add Printing Record" or "Add Printing Constructor".
 
 Tactics
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 182a509..3429baf 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -200,10 +200,19 @@ Definition b := {| x := 5; y := 3 |}.
 Definition c := {| y := 3; x := 5 |}.
 \end{coq_example}
 
-This syntax can be disabled for printing by
+This syntax can be disabled globally for printing by
 \begin{quote}
 {\tt Unset Printing Records.}
 \end{quote}
+For a given type, one can override this using either
+\begin{quote}
+{\tt Add Printing Record {\ident}.}
+\end{quote}
+to get record syntax or
+\begin{quote}
+{\tt Add Printing Constructor {\ident}.}
+\end{quote}
+to get constructor syntax.
 
 This syntax can also be used for pattern matching.
 
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 623b334..b9e1414 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -14,8 +14,10 @@ let commands = [
    "Add LoadPath";
    "Add ML Path";
    "Add Morphism";
+   "Add Printing Constructor";
    "Add Printing If";
    "Add Printing Let";
+   "Add Printing Record";
    "Add Rec LoadPath";
    "Add Rec ML Path";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
@@ -92,8 +94,10 @@ let commands = [
    "Record";
    "Remark";
    "Remove LoadPath";
+   "Remove Printing Constructor";
    "Remove Printing If";
    "Remove Printing Let";
+   "Remove Printing Record";
    "Require";
    "Require Export";
    "Require Import";
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f23f975..fa92f92 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -74,6 +74,49 @@ let without_symbols f = Flags.with_option print_no_symbol f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 
 (**********************************************************************)
+(* Control printing of records *)
+
+let is_record indsp =
+  try
+    let _ = Recordops.lookup_structure indsp in
+    true
+  with Not_found -> false
+
+let encode_record r =
+  let indsp = global_inductive r in
+  if not (is_record indsp) then
+    user_err_loc (loc_of_reference r,"encode_record",
+    str "This type is not a structure type.");
+  indsp
+
+module PrintingRecordRecord =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Record"
+    let title = "Types leading to pretty-printing using record notation: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using record notation"
+      else " are not printed using record notation")
+  end)
+
+module PrintingRecordConstructor =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Constructor"
+    let title = "Types leading to pretty-printing using constructor form: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using constructor form"
+      else " are not printed using constructor form")
+  end)
+
+module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord)
+module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
+
+(**********************************************************************)
 (* Various externalisation functions *)
 
 let insert_delimiters e = function
@@ -299,7 +342,7 @@ let rec extern_cases_pattern_in_scope 
(scopes:local_scopes) vars pat =
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       let p =
        try
-         if !Flags.raw_print then raise Exit;
+          if !Flags.raw_print then raise Exit;
          let projs = Recordops.lookup_projections (fst cstrsp) in
          let rec ip projs args acc =
            match projs with
@@ -550,9 +593,15 @@ let rec extern inctx scopes vars r =
               extern_args (extern true) (snd scopes) vars args subscopes in
             begin
               try
-                if !Flags.raw_print or not !Flags.record_print then raise 
Exit;
+                 if !Flags.raw_print then raise Exit;
                 let cstrsp = match ref with ConstructRef c -> c | _ -> raise 
Not_found in
                 let struc = Recordops.lookup_structure (fst cstrsp) in
+                 if PrintingRecord.active (fst cstrsp) then
+                   ()
+                 else if PrintingConstructor.active (fst cstrsp) then
+                   raise Exit
+                 else if not !Flags.record_print then
+                   raise Exit;
                 let projs = struc.Recordops.s_PROJ in
                 let locals = struc.Recordops.s_PROJKIND in
                 let rec cut args n =
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index a3c63ea..36d643a 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -2,7 +2,15 @@
      : test
 {| field := 5 |}
      : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
 build 5
      : test
 build 5
      : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 4ae4338..6aa3df9 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -1,11 +1,21 @@
 Record test := build { field : nat }.
+Record test_r := build_r { field_r : nat }.
+Record test_c := build_c { field_c : nat }.
+
+Add Printing Constructor test_c.
+Add Printing Record test_r.
 
 Set Printing Records.
 
 Check build 5.
 Check {| field := 5 |}.
 
+Check build_r 5.
+Check build_c 5.
+
 Unset Printing Records.
 
 Check build 5.
 Check {| field := 5 |}.
+Check build_r 5.
+Check build_c 5.
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index bc0e18e..8630fb3 100644
--- a/tools/coq-syntax.el
+++ b/tools/coq-syntax.el
@@ -417,8 +417,10 @@
      ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
      ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism")
      ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
+     ("Add Printing Constructor" nil "Add Printing Constructor #." t 
"Add\\s-+Printing\\s-+Constructor")
      ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
      ("Add Printing Let" nil "Add Printing Let #." t 
"Add\\s-+Printing\\s-+Let")
+     ("Add Printing Record" nil "Add Printing Record #." t 
"Add\\s-+Printing\\s-+Record")
      ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil 
"Add\\s-+Rec\\s-+LoadPath")
      ("Add Rec ML Path" nil "Add Rec ML Path #." nil 
"Add\\s-+Rec\\s-+ML\\s-+Path")
      ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
-- 
1.7.5.2