print_record: diagnostic printing of record definitions
authorkleing
Sun Jan 10 19:37:21 2016 -0800 (2016-01-10)
changeset 6211786a31308a8e1
parent 62116 bc178c0fe1a1
child 62118 e60f1a925b4d
print_record: diagnostic printing of record definitions
src/HOL/Record.thy
src/HOL/Record_Benchmark/Record_Benchmark.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Mon Jan 11 00:04:23 2016 +0100
     1.2 +++ b/src/HOL/Record.thy	Sun Jan 10 19:37:21 2016 -0800
     1.3 @@ -10,7 +10,9 @@
     1.4  
     1.5  theory Record
     1.6  imports Quickcheck_Exhaustive
     1.7 -keywords "record" :: thy_decl
     1.8 +keywords
     1.9 +  "record" :: thy_decl and
    1.10 +  "print_record" :: diag
    1.11  begin
    1.12  
    1.13  subsection \<open>Introduction\<close>
     2.1 --- a/src/HOL/Record_Benchmark/Record_Benchmark.thy	Mon Jan 11 00:04:23 2016 +0100
     2.2 +++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Sun Jan 10 19:37:21 2016 -0800
     2.3 @@ -420,5 +420,8 @@
     2.4      (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*})
     2.5    done
     2.6  
     2.7 +print_record many_A
     2.8 +
     2.9 +print_record many_B
    2.10  
    2.11  end
    2.12 \ No newline at end of file
     3.1 --- a/src/HOL/Tools/record.ML	Mon Jan 11 00:04:23 2016 +0100
     3.2 +++ b/src/HOL/Tools/record.ML	Sun Jan 10 19:37:21 2016 -0800
     3.3 @@ -46,6 +46,9 @@
     3.4    val split_simp_tac: Proof.context -> thm list -> (term -> int) -> int -> tactic
     3.5    val split_wrapper: string * (Proof.context -> wrapper)
     3.6  
     3.7 +  val pretty_recT: Proof.context -> typ -> Pretty.T
     3.8 +  val string_of_record: Proof.context -> string -> string
     3.9 +
    3.10    val codegen: bool Config.T
    3.11    val updateN: string
    3.12    val ext_typeN: string
    3.13 @@ -2350,6 +2353,58 @@
    3.14  end;
    3.15  
    3.16  
    3.17 +(* printing *)
    3.18 +
    3.19 +local
    3.20 +
    3.21 +fun the_parent_recT (Type (parent, [Type (_, [unit as Type (_,[])])])) = Type (parent, [unit])
    3.22 +  | the_parent_recT (Type (extT, [T])) = Type (extT, [the_parent_recT T])
    3.23 +  | the_parent_recT T = raise TYPE ("Not a unit record scheme with parent: ", [T], [])
    3.24 +
    3.25 +in
    3.26 +
    3.27 +fun pretty_recT ctxt typ =
    3.28 +  let
    3.29 +    val thy = Proof_Context.theory_of ctxt
    3.30 +    val (fs, (_, moreT)) = get_recT_fields thy typ
    3.31 +    val _ = if moreT = HOLogic.unitT then () else raise TYPE ("Not a unit record scheme: ", [typ], [])
    3.32 +    val parent = if length (dest_recTs typ) >= 2 then SOME (the_parent_recT typ) else NONE
    3.33 +    val pfs = case parent of SOME p => fst (get_recT_fields thy p) | NONE => []
    3.34 +    val fs' = drop (length pfs) fs
    3.35 +    fun pretty_field (name, typ) = Pretty.block [
    3.36 +          Syntax.pretty_term ctxt (Const (name, typ)),
    3.37 +          Pretty.brk 1,
    3.38 +          Pretty.str "::",
    3.39 +          Pretty.brk 1,
    3.40 +          Syntax.pretty_typ ctxt typ
    3.41 +        ]
    3.42 +  in
    3.43 +    Pretty.block (Library.separate (Pretty.brk 1)
    3.44 +      ([Pretty.keyword1 "record", Syntax.pretty_typ ctxt typ, Pretty.str "="] @
    3.45 +        (case parent of
    3.46 +          SOME p => [Syntax.pretty_typ ctxt p, Pretty.str "+"]
    3.47 +        | NONE => [])) @
    3.48 +      Pretty.fbrk ::
    3.49 +      Pretty.fbreaks (map pretty_field fs'))
    3.50 +  end
    3.51 +
    3.52 +end
    3.53 +
    3.54 +fun string_of_record ctxt s =
    3.55 +  let
    3.56 +    val T = Syntax.read_typ ctxt s
    3.57 +  in
    3.58 +    Pretty.string_of (pretty_recT ctxt T)
    3.59 +      handle TYPE _ => error ("Unknown record: " ^ Syntax.string_of_typ ctxt T)
    3.60 +  end
    3.61 +
    3.62 +val print_record =
    3.63 +  let
    3.64 +    fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
    3.65 +         Print_Mode.with_modes modes (fn () => Output.writeln (string_of state arg)) ());
    3.66 +  in print_item (string_of_record o Toplevel.context_of) end
    3.67 +
    3.68 +
    3.69  (* outer syntax *)
    3.70  
    3.71  val _ =
    3.72 @@ -2360,4 +2415,11 @@
    3.73      >> (fn ((overloaded, x), (y, z)) =>
    3.74          Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
    3.75  
    3.76 -end;
    3.77 +val opt_modes =
    3.78 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
    3.79 +
    3.80 +val _ =
    3.81 +  Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
    3.82 +    (opt_modes -- Parse.typ >> print_record);
    3.83 +
    3.84 +end