src/Pure/attribute.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5835 5b79fbf1a65f
child 5872 df19e1de5c8a
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/attribute.ML
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     4
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     5
Theorem tags and attributes.
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     6
*)
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     7
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     8
signature BASIC_ATTRIBUTE =
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
     9
sig
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    10
  type tag
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    11
  type tthm
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    12
  type 'a attribute
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    13
end;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    14
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    15
signature ATTRIBUTE =
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    16
sig
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    17
  include BASIC_ATTRIBUTE
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    18
  val thm_of: tthm -> thm
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    19
  val tthm_of: thm -> tthm
5835
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    20
  val lift_modifier: ('a * thm list -> 'b) -> 'a * tthm list -> 'b
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    21
  val rule: ('b -> 'a) -> ('a -> thm -> thm) -> 'b attribute
4850
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    22
  val none: 'a -> 'a * 'b attribute list
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    23
  val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    24
  val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    25
  val fail: string -> string -> 'a
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    26
  val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
4850
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    27
  val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    28
  val pretty_tthm: tthm -> Pretty.T
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    29
  val tag: tag -> 'a attribute
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    30
  val untag: tag -> 'a attribute
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    31
  val lemma: tag
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    32
  val assumption: tag
5194
650bf0ce0229 added internal;
wenzelm
parents: 5023
diff changeset
    33
  val internal: tag
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    34
  val tag_lemma: 'a attribute
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    35
  val tag_assumption: 'a attribute
5194
650bf0ce0229 added internal;
wenzelm
parents: 5023
diff changeset
    36
  val tag_internal: 'a attribute
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    37
end;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    38
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    39
structure Attribute: ATTRIBUTE =
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    40
struct
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    41
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    42
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    43
(** tags and attributes **)
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    44
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    45
type tag = string * string list;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    46
type tthm = thm * tag list;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    47
type 'a attribute = 'a * tthm -> 'a * tthm;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    48
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    49
fun thm_of (thm, _) = thm;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    50
fun tthm_of thm = (thm, []);
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    51
5835
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    52
fun lift_modifier f (x, tthms) = f (x, map thm_of tthms);
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    53
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    54
fun rule get_data f (x, (thm, tags)) = (x, (f (get_data x) thm, tags));
5b79fbf1a65f added lift_modifier, rule;
wenzelm
parents: 5559
diff changeset
    55
4850
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    56
fun none x = (x, []);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    57
fun no_attrs (x, y) = ((x, (y, [])), []);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    58
fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    59
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    60
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    61
(* apply attributes *)
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    62
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    63
exception FAIL of string * string;
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    64
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    65
fun fail name msg = raise FAIL (name, msg);
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    66
5023
c12c438a89db moved attributes theory data to Isar/isar_thy.ML;
wenzelm
parents: 5005
diff changeset
    67
(* FIXME error (!!?), push up the warning (??) *)
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    68
fun warn_failed (name, msg) =
4797
d66477d29598 tuned fail;
wenzelm
parents: 4792
diff changeset
    69
  warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    70
4850
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    71
fun apply (x_th, []) = x_th
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    72
  | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    73
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    74
fun applys ((x, []), _) = (x, [])
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    75
  | applys ((x, th :: ths), atts) =
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    76
      let
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    77
        val (x', th') = apply ((x, th), atts);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    78
        val (x'', ths') = applys ((x', ths), atts);
050481f41e28 added none: 'a -> 'a * 'b attribute list;
wenzelm
parents: 4797
diff changeset
    79
      in (x'', th' :: ths') end;
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    80
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    81
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    82
(* display tagged theorems *)
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    83
5559
95e8692fda23 tuned pretty_tag;
wenzelm
parents: 5194
diff changeset
    84
fun pretty_tag (name, args) = Pretty.strs (name :: args);
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    85
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    86
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    87
fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    88
  | pretty_tthm (thm, tags) = Pretty.block
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    89
      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    90
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    91
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    92
(* basic attributes *)
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    93
5559
95e8692fda23 tuned pretty_tag;
wenzelm
parents: 5194
diff changeset
    94
fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
4790
5adb93457e39 removed simple;
wenzelm
parents: 4780
diff changeset
    95
fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    96
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    97
val lemma = ("lemma", []);
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
    98
val assumption = ("assumption", []);
5194
650bf0ce0229 added internal;
wenzelm
parents: 5023
diff changeset
    99
val internal = ("internal", []);
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   100
fun tag_lemma x = tag lemma x;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   101
fun tag_assumption x = tag assumption x;
5194
650bf0ce0229 added internal;
wenzelm
parents: 5023
diff changeset
   102
fun tag_internal x = tag internal x;
4780
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   103
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   104
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   105
end;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   106
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   107
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   108
structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
f4ff003bc7ee Theorem tags and attributes.
wenzelm
parents:
diff changeset
   109
open BasicAttribute;