# HG changeset patch
# User kleing
# Date 1452483441 28800
# Node ID 86a31308a8e18a21fccb07e3a6a4e0470f00618f
# Parent  bc178c0fe1a1b13dd17bbe2936797149462a8b5b
print_record: diagnostic printing of record definitions

diff -r bc178c0fe1a1 -r 86a31308a8e1 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Jan 11 00:04:23 2016 +0100
+++ b/src/HOL/Record.thy	Sun Jan 10 19:37:21 2016 -0800
@@ -10,7 +10,9 @@
 
 theory Record
 imports Quickcheck_Exhaustive
-keywords "record" :: thy_decl
+keywords
+  "record" :: thy_decl and
+  "print_record" :: diag
 begin
 
 subsection \<open>Introduction\<close>
diff -r bc178c0fe1a1 -r 86a31308a8e1 src/HOL/Record_Benchmark/Record_Benchmark.thy
--- a/src/HOL/Record_Benchmark/Record_Benchmark.thy	Mon Jan 11 00:04:23 2016 +0100
+++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Sun Jan 10 19:37:21 2016 -0800
@@ -420,5 +420,8 @@
     (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   done
 
+print_record many_A
+
+print_record many_B
 
 end
\ No newline at end of file
diff -r bc178c0fe1a1 -r 86a31308a8e1 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Jan 11 00:04:23 2016 +0100
+++ b/src/HOL/Tools/record.ML	Sun Jan 10 19:37:21 2016 -0800
@@ -46,6 +46,9 @@
   val split_simp_tac: Proof.context -> thm list -> (term -> int) -> int -> tactic
   val split_wrapper: string * (Proof.context -> wrapper)
 
+  val pretty_recT: Proof.context -> typ -> Pretty.T
+  val string_of_record: Proof.context -> string -> string
+
   val codegen: bool Config.T
   val updateN: string
   val ext_typeN: string
@@ -2350,6 +2353,58 @@
 end;
 
 
+(* printing *)
+
+local
+
+fun the_parent_recT (Type (parent, [Type (_, [unit as Type (_,[])])])) = Type (parent, [unit])
+  | the_parent_recT (Type (extT, [T])) = Type (extT, [the_parent_recT T])
+  | the_parent_recT T = raise TYPE ("Not a unit record scheme with parent: ", [T], [])
+
+in
+
+fun pretty_recT ctxt typ =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val (fs, (_, moreT)) = get_recT_fields thy typ
+    val _ = if moreT = HOLogic.unitT then () else raise TYPE ("Not a unit record scheme: ", [typ], [])
+    val parent = if length (dest_recTs typ) >= 2 then SOME (the_parent_recT typ) else NONE
+    val pfs = case parent of SOME p => fst (get_recT_fields thy p) | NONE => []
+    val fs' = drop (length pfs) fs
+    fun pretty_field (name, typ) = Pretty.block [
+          Syntax.pretty_term ctxt (Const (name, typ)),
+          Pretty.brk 1,
+          Pretty.str "::",
+          Pretty.brk 1,
+          Syntax.pretty_typ ctxt typ
+        ]
+  in
+    Pretty.block (Library.separate (Pretty.brk 1)
+      ([Pretty.keyword1 "record", Syntax.pretty_typ ctxt typ, Pretty.str "="] @
+        (case parent of
+          SOME p => [Syntax.pretty_typ ctxt p, Pretty.str "+"]
+        | NONE => [])) @
+      Pretty.fbrk ::
+      Pretty.fbreaks (map pretty_field fs'))
+  end
+
+end
+
+fun string_of_record ctxt s =
+  let
+    val T = Syntax.read_typ ctxt s
+  in
+    Pretty.string_of (pretty_recT ctxt T)
+      handle TYPE _ => error ("Unknown record: " ^ Syntax.string_of_typ ctxt T)
+  end
+
+val print_record =
+  let
+    fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
+         Print_Mode.with_modes modes (fn () => Output.writeln (string_of state arg)) ());
+  in print_item (string_of_record o Toplevel.context_of) end
+
+
 (* outer syntax *)
 
 val _ =
@@ -2360,4 +2415,11 @@
     >> (fn ((overloaded, x), (y, z)) =>
         Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
 
-end;
+val opt_modes =
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
+
+val _ =
+  Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
+    (opt_modes -- Parse.typ >> print_record);
+
+end