formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
authorhaftmann
Mon Jan 05 18:39:32 2015 +0100 (2015-01-05)
changeset 59296002d817b4c37
parent 59295 bab968955925
child 59297 7ca42387fbf5
child 59301 9089639ba348
formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Pure/Tools/class_deps.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jan 05 23:33:39 2015 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jan 05 18:39:32 2015 +0100
     1.3 @@ -49,6 +49,9 @@
     1.4    (*tactics*)
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_tac: Proof.context -> thm list -> tactic
     1.7 +
     1.8 +  (*diagnostics*)
     1.9 +  val pretty_body: theory -> class -> Pretty.T list
    1.10  end;
    1.11  
    1.12  structure Class: CLASS =
    1.13 @@ -725,5 +728,15 @@
    1.14    Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
    1.15      "apply some intro/elim rule");
    1.16  
    1.17 +
    1.18 +(** diagnostics **)
    1.19 +
    1.20 +fun pretty_body thy c =
    1.21 +  let
    1.22 +    val cs = (#params o Axclass.get_info thy) c;
    1.23 +    val fix_args = map (fn (c, T) => ((Binding.name o Long_Name.base_name) c, SOME T, NoSyn)) cs; 
    1.24 +    val fixes = if null fix_args then [] else [Element.Fixes fix_args];
    1.25 +  in maps (Element.pretty_ctxt (init c thy)) (fixes @ Locale.hyp_spec_of thy c) end;
    1.26 +
    1.27  end;
    1.28  
     2.1 --- a/src/Pure/Isar/expression.ML	Mon Jan 05 23:33:39 2015 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Mon Jan 05 18:39:32 2015 +0100
     2.3 @@ -762,6 +762,10 @@
     2.4            [(Attrib.internal o K) Locale.witness_add])])) defs)
     2.5    | defines_to_notes _ e = e;
     2.6  
     2.7 +fun is_hyp (elem as Assumes asms) = true
     2.8 +  | is_hyp (elem as Defines defs) = true
     2.9 +  | is_hyp _ = false;
    2.10 +
    2.11  fun gen_add_locale prep_decl
    2.12      binding raw_predicate_binding raw_import raw_body thy =
    2.13    let
    2.14 @@ -798,6 +802,8 @@
    2.15          map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
    2.16      val asm = if is_some b_statement then b_statement else a_statement;
    2.17  
    2.18 +    val hyp_spec = filter is_hyp body_elems;
    2.19 +
    2.20      val notes =
    2.21        if is_some asm then
    2.22          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
    2.23 @@ -820,7 +826,7 @@
    2.24  
    2.25      val loc_ctxt = thy'
    2.26        |> Locale.register_locale binding (extraTs, params)
    2.27 -          (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    2.28 +          (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
    2.29        |> Named_Target.init name
    2.30        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    2.31  
     3.1 --- a/src/Pure/Isar/locale.ML	Mon Jan 05 23:33:39 2015 +0100
     3.2 +++ b/src/Pure/Isar/locale.ML	Mon Jan 05 18:39:32 2015 +0100
     3.3 @@ -33,6 +33,7 @@
     3.4      (string * sort) list * ((string * typ) * mixfix) list ->
     3.5      term option * term list ->
     3.6      thm option * thm option -> thm list ->
     3.7 +    Element.context_i list ->
     3.8      declaration list ->
     3.9      (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
    3.10      (string * morphism) list -> theory -> theory
    3.11 @@ -82,6 +83,7 @@
    3.12      morphism -> theory -> theory
    3.13  
    3.14    (* Diagnostic *)
    3.15 +  val hyp_spec_of: theory -> string -> Element.context_i list
    3.16    val print_locales: theory -> unit
    3.17    val print_locale: theory -> bool -> xstring * Position.T -> unit
    3.18    val print_registrations: Proof.context -> xstring * Position.T -> unit
    3.19 @@ -124,6 +126,8 @@
    3.20      (* assumptions (as a single predicate expression) and defines *)
    3.21    intros: thm option * thm option,
    3.22    axioms: thm list,
    3.23 +  hyp_spec: Element.context_i list,
    3.24 +    (* diagnostic device: theorem part of hypothetical body as specified by the user *)
    3.25    (** dynamic part **)
    3.26    syntax_decls: (declaration * serial) list,
    3.27      (* syntax declarations *)
    3.28 @@ -135,22 +139,22 @@
    3.29      (* mixin part of dependencies *)
    3.30  };
    3.31  
    3.32 -fun mk_locale ((parameters, spec, intros, axioms),
    3.33 +fun mk_locale ((parameters, spec, intros, axioms, hyp_spec),
    3.34      ((syntax_decls, notes), (dependencies, mixins))) =
    3.35 -  Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
    3.36 +  Loc {parameters = parameters, spec = spec, intros = intros, axioms = axioms, hyp_spec = hyp_spec,
    3.37      syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins};
    3.38  
    3.39 -fun map_locale f (Loc {parameters, spec, intros, axioms,
    3.40 +fun map_locale f (Loc {parameters, spec, intros, axioms, hyp_spec,
    3.41      syntax_decls, notes, dependencies, mixins}) =
    3.42 -  mk_locale (f ((parameters, spec, intros, axioms),
    3.43 +  mk_locale (f ((parameters, spec, intros, axioms, hyp_spec),
    3.44      ((syntax_decls, notes), (dependencies, mixins))));
    3.45  
    3.46  fun merge_locale
    3.47 - (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies, mixins},
    3.48 + (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins},
    3.49    Loc {syntax_decls = syntax_decls', notes = notes',
    3.50        dependencies = dependencies', mixins = mixins', ...}) =
    3.51      mk_locale
    3.52 -      ((parameters, spec, intros, axioms),
    3.53 +      ((parameters, spec, intros, axioms, hyp_spec),
    3.54          ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
    3.55            merge (eq_snd op =) (notes, notes')),
    3.56              (merge (eq_snd op =) (dependencies, dependencies'),
    3.57 @@ -184,10 +188,10 @@
    3.58      SOME (Loc loc) => loc
    3.59    | NONE => error ("Unknown locale " ^ quote name));
    3.60  
    3.61 -fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
    3.62 +fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy =
    3.63    thy |> Locales.map (Name_Space.define (Context.Theory thy) true
    3.64      (binding,
    3.65 -      mk_locale ((parameters, spec, intros, axioms),
    3.66 +      mk_locale ((parameters, spec, intros, axioms, hyp_spec),
    3.67          ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
    3.68            (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
    3.69              Inttab.empty)))) #> snd);
    3.70 @@ -647,6 +651,8 @@
    3.71  
    3.72  (*** diagnostic commands and interfaces ***)
    3.73  
    3.74 +fun hyp_spec_of thy = #hyp_spec o the_locale thy;
    3.75 +
    3.76  fun print_locales thy =
    3.77    Pretty.block
    3.78      (Pretty.breaks
     4.1 --- a/src/Pure/Tools/class_deps.ML	Mon Jan 05 23:33:39 2015 +0100
     4.2 +++ b/src/Pure/Tools/class_deps.ML	Mon Jan 05 18:39:32 2015 +0100
     4.3 @@ -15,6 +15,7 @@
     4.4  
     4.5  fun gen_visualize prep_sort ctxt raw_super raw_sub =
     4.6    let
     4.7 +    val thy = Proof_Context.theory_of ctxt;
     4.8      val super = prep_sort ctxt raw_super;
     4.9      val sub = Option.map (prep_sort ctxt) raw_sub;
    4.10      val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    4.11 @@ -26,11 +27,12 @@
    4.12      val (_, algebra) =
    4.13        Sorts.subalgebra (Context.pretty ctxt)
    4.14          (le_super andf sub_le) (K NONE) original_algebra;
    4.15 +    fun pretty_body_of c = if Class.is_class thy c then Class.pretty_body thy c else [];
    4.16    in
    4.17      Sorts.classes_of algebra
    4.18      |> Graph.dest
    4.19      |> map (fn ((c, _), ds) =>
    4.20 -        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds))
    4.21 +        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) (pretty_body_of c)), ds))
    4.22      |> Graph_Display.display_graph
    4.23    end;
    4.24