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