aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--doc/refman/RefMan-ext.tex11
-rw-r--r--ide/coq_commands.ml4
-rw-r--r--interp/constrextern.ml53
-rw-r--r--test-suite/output/Record.out16
-rw-r--r--test-suite/output/Record.v21
-rw-r--r--tools/coq-syntax.el2
7 files changed, 106 insertions, 3 deletions
diff --git a/CHANGES b/CHANGES
index 909151f3c..98a8c78d1 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 182a50959..3429bafab 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 623b334e0..b9e141455 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 f23f9750c..fa92f9221 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
new file mode 100644
index 000000000..36d643a44
--- /dev/null
+++ b/test-suite/output/Record.out
@@ -0,0 +1,16 @@
+{| field := 5 |}
+ : 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
new file mode 100644
index 000000000..6aa3df983
--- /dev/null
+++ b/test-suite/output/Record.v
@@ -0,0 +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 bc0e18e57..8630fb3a9 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")
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 16:56:09 +0000