formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML

--- a/src/Pure/Isar/class.ML	Mon Jan 05 23:33:39 2015 +0100
+++ b/src/Pure/Isar/class.ML	Mon Jan 05 18:39:32 2015 +0100
@@ -49,6 +49,9 @@
   (*tactics*)
   val intro_classes_tac: thm list -> tactic
   val default_intro_tac: Proof.context -> thm list -> tactic
+
+  (*diagnostics*)
+  val pretty_body: theory -> class -> Pretty.T list
 end;
 
 structure Class: CLASS =
@@ -725,5 +728,15 @@
   Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
     "apply some intro/elim rule");
 
+
+(** diagnostics **)
+
+fun pretty_body thy c =
+  let
+    val cs = (#params o Axclass.get_info thy) c;
+    val fix_args = map (fn (c, T) => ((Binding.name o Long_Name.base_name) c, SOME T, NoSyn)) cs; 
+    val fixes = if null fix_args then [] else [Element.Fixes fix_args];
+  in maps (Element.pretty_ctxt (init c thy)) (fixes @ Locale.hyp_spec_of thy c) end;
+
 end;
 

--- a/src/Pure/Isar/expression.ML	Mon Jan 05 23:33:39 2015 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Jan 05 18:39:32 2015 +0100
@@ -762,6 +762,10 @@
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
+fun is_hyp (elem as Assumes asms) = true
+  | is_hyp (elem as Defines defs) = true
+  | is_hyp _ = false;
+
 fun gen_add_locale prep_decl
     binding raw_predicate_binding raw_import raw_body thy =
   let
@@ -798,6 +802,8 @@
         map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
     val asm = if is_some b_statement then b_statement else a_statement;
 
+    val hyp_spec = filter is_hyp body_elems;
+
     val notes =
       if is_some asm then
         [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
@@ -820,7 +826,7 @@
 
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
-          (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
+          (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
       |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 

--- a/src/Pure/Isar/locale.ML	Mon Jan 05 23:33:39 2015 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Jan 05 18:39:32 2015 +0100
@@ -33,6 +33,7 @@
     (string * sort) list * ((string * typ) * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
+    Element.context_i list ->
     declaration list ->
     (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
@@ -82,6 +83,7 @@
     morphism -> theory -> theory
 
   (* Diagnostic *)
+  val hyp_spec_of: theory -> string -> Element.context_i list
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
@@ -124,6 +126,8 @@
     (* assumptions (as a single predicate expression) and defines *)
   intros: thm option * thm option,
   axioms: thm list,
+  hyp_spec: Element.context_i list,
+    (* diagnostic device: theorem part of hypothetical body as specified by the user *)
   (** dynamic part **)
   syntax_decls: (declaration * serial) list,
     (* syntax declarations *)
@@ -135,22 +139,22 @@
     (* mixin part of dependencies *)
 };
 
-fun mk_locale ((parameters, spec, intros, axioms),
+fun mk_locale ((parameters, spec, intros, axioms, hyp_spec),
     ((syntax_decls, notes), (dependencies, mixins))) =
-  Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
+  Loc {parameters = parameters, spec = spec, intros = intros, axioms = axioms, hyp_spec = hyp_spec,
     syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins};
 
-fun map_locale f (Loc {parameters, spec, intros, axioms,
+fun map_locale f (Loc {parameters, spec, intros, axioms, hyp_spec,
     syntax_decls, notes, dependencies, mixins}) =
-  mk_locale (f ((parameters, spec, intros, axioms),
+  mk_locale (f ((parameters, spec, intros, axioms, hyp_spec),
     ((syntax_decls, notes), (dependencies, mixins))));
 
 fun merge_locale
- (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies, mixins},
+ (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins},
   Loc {syntax_decls = syntax_decls', notes = notes',
       dependencies = dependencies', mixins = mixins', ...}) =
     mk_locale
-      ((parameters, spec, intros, axioms),
+      ((parameters, spec, intros, axioms, hyp_spec),
         ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
           merge (eq_snd op =) (notes, notes')),
             (merge (eq_snd op =) (dependencies, dependencies'),
@@ -184,10 +188,10 @@
     SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name));
 
-fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
+fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy =
   thy |> Locales.map (Name_Space.define (Context.Theory thy) true
     (binding,
-      mk_locale ((parameters, spec, intros, axioms),
+      mk_locale ((parameters, spec, intros, axioms, hyp_spec),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
           (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
             Inttab.empty)))) #> snd);
@@ -647,6 +651,8 @@
 
 (*** diagnostic commands and interfaces ***)
 
+fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+
 fun print_locales thy =
   Pretty.block
     (Pretty.breaks

--- a/src/Pure/Tools/class_deps.ML	Mon Jan 05 23:33:39 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Mon Jan 05 18:39:32 2015 +0100
@@ -15,6 +15,7 @@
 
 fun gen_visualize prep_sort ctxt raw_super raw_sub =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val super = prep_sort ctxt raw_super;
     val sub = Option.map (prep_sort ctxt) raw_sub;
     val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
@@ -26,11 +27,12 @@
     val (_, algebra) =
       Sorts.subalgebra (Context.pretty ctxt)
         (le_super andf sub_le) (K NONE) original_algebra;
+    fun pretty_body_of c = if Class.is_class thy c then Class.pretty_body thy c else [];
   in
     Sorts.classes_of algebra
     |> Graph.dest
     |> map (fn ((c, _), ds) =>
-        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds))
+        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) (pretty_body_of c)), ds))
     |> Graph_Display.display_graph
   end;