src/Pure/attribute.ML
author wenzelm
Sat Apr 04 11:43:39 1998 +0200 (1998-04-04)
changeset 4790 5adb93457e39
parent 4780 f4ff003bc7ee
child 4792 8e3c2dddb9c8
permissions -rw-r--r--
removed simple;
added fail, untag;
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
  val print_attributes: theory -> unit
wenzelm@4780
    14
end;
wenzelm@4780
    15
wenzelm@4780
    16
signature ATTRIBUTE =
wenzelm@4780
    17
sig
wenzelm@4780
    18
  include BASIC_ATTRIBUTE
wenzelm@4780
    19
  val thm_of: tthm -> thm
wenzelm@4780
    20
  val tthm_of: thm -> tthm
wenzelm@4790
    21
  val fail: string -> string -> 'a
wenzelm@4780
    22
  val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
wenzelm@4780
    23
  val pretty_tthm: tthm -> Pretty.T
wenzelm@4780
    24
  val tag: tag -> 'a attribute
wenzelm@4790
    25
  val untag: tag -> 'a attribute
wenzelm@4780
    26
  val lemma: tag
wenzelm@4780
    27
  val assumption: tag
wenzelm@4780
    28
  val tag_lemma: 'a attribute
wenzelm@4780
    29
  val tag_assumption: 'a attribute
wenzelm@4780
    30
  val setup: theory -> theory
wenzelm@4790
    31
  val global_attr: theory -> (xstring * string list) -> theory attribute
wenzelm@4790
    32
  val local_attr: theory -> (xstring * string list) -> local_theory attribute
wenzelm@4780
    33
  val add_attrs: (bstring * ((string list -> theory attribute) *
wenzelm@4790
    34
      (string list -> local_theory attribute))) list -> theory -> theory
wenzelm@4780
    35
end;
wenzelm@4780
    36
wenzelm@4780
    37
structure Attribute: ATTRIBUTE =
wenzelm@4780
    38
struct
wenzelm@4780
    39
wenzelm@4780
    40
wenzelm@4780
    41
(** tags and attributes **)
wenzelm@4780
    42
wenzelm@4780
    43
type tag = string * string list;
wenzelm@4780
    44
type tthm = thm * tag list;
wenzelm@4780
    45
type 'a attribute = 'a * tthm -> 'a * tthm;
wenzelm@4780
    46
wenzelm@4780
    47
fun thm_of (thm, _) = thm;
wenzelm@4780
    48
fun tthm_of thm = (thm, []);
wenzelm@4780
    49
wenzelm@4790
    50
wenzelm@4790
    51
(* apply attributes *)
wenzelm@4790
    52
wenzelm@4790
    53
exception FAIL of string * string;
wenzelm@4790
    54
wenzelm@4790
    55
fun fail name msg = raise FAIL (name, msg);
wenzelm@4790
    56
wenzelm@4790
    57
fun warn_failed (name, msg) =
wenzelm@4790
    58
  warning ("Invocation of " ^ quote name ^ " attribute failed: " ^ msg);
wenzelm@4790
    59
wenzelm@4790
    60
fun apply (x, []) = x
wenzelm@4790
    61
  | apply (x, f :: fs) = apply (f x handle FAIL info => (warn_failed info; x), fs);
wenzelm@4780
    62
wenzelm@4780
    63
wenzelm@4780
    64
(* display tagged theorems *)
wenzelm@4780
    65
wenzelm@4780
    66
fun pretty_tag (name, []) = Pretty.str name
wenzelm@4780
    67
  | pretty_tag (name, args) = Pretty.block
wenzelm@4780
    68
      [Pretty.str name, Pretty.list "(" ")" (map Pretty.str args)];
wenzelm@4780
    69
wenzelm@4780
    70
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
wenzelm@4780
    71
wenzelm@4780
    72
fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
wenzelm@4780
    73
  | pretty_tthm (thm, tags) = Pretty.block
wenzelm@4780
    74
      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
wenzelm@4780
    75
wenzelm@4780
    76
wenzelm@4780
    77
(* basic attributes *)
wenzelm@4780
    78
wenzelm@4790
    79
fun tag tg (x, (thm, tags)) = (x, (thm, tg ins tags));
wenzelm@4790
    80
fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
wenzelm@4780
    81
wenzelm@4780
    82
val lemma = ("lemma", []);
wenzelm@4780
    83
val assumption = ("assumption", []);
wenzelm@4780
    84
fun tag_lemma x = tag lemma x;
wenzelm@4780
    85
fun tag_assumption x = tag assumption x;
wenzelm@4780
    86
wenzelm@4780
    87
wenzelm@4780
    88
wenzelm@4780
    89
(** theory data **)
wenzelm@4780
    90
wenzelm@4780
    91
(* data kind 'attributes' *)
wenzelm@4780
    92
wenzelm@4780
    93
val attributesK = "Pure/attributes";
wenzelm@4780
    94
wenzelm@4780
    95
exception Attributes of
wenzelm@4780
    96
  {space: NameSpace.T,
wenzelm@4780
    97
   attrs:
wenzelm@4780
    98
    ((string list -> theory attribute) *
wenzelm@4790
    99
     (string list -> local_theory attribute)) Symtab.table};
wenzelm@4780
   100
wenzelm@4780
   101
fun print_attributes thy = Display.print_data thy attributesK;
wenzelm@4780
   102
wenzelm@4780
   103
wenzelm@4780
   104
(* setup *)
wenzelm@4780
   105
wenzelm@4780
   106
local
wenzelm@4780
   107
  val empty = Attributes {space = NameSpace.empty, attrs = Symtab.empty};
wenzelm@4780
   108
wenzelm@4780
   109
  fun prep_ext (x as Attributes _) = x;
wenzelm@4780
   110
wenzelm@4780
   111
  fun merge (Attributes {space = space1, attrs = attrs1},
wenzelm@4780
   112
      Attributes {space = space2, attrs = attrs2}) =
wenzelm@4780
   113
    Attributes {
wenzelm@4780
   114
      space = NameSpace.merge (space1, space2),
wenzelm@4780
   115
      attrs = Symtab.merge (K true) (attrs1, attrs2)};
wenzelm@4780
   116
wenzelm@4780
   117
  fun print _ (Attributes {space, attrs}) =
wenzelm@4780
   118
   (Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
wenzelm@4780
   119
    Pretty.writeln (Pretty.strs ("attributes:" :: map fst (Symtab.dest attrs))));
wenzelm@4780
   120
in
wenzelm@4780
   121
  val setup = Theory.init_data [(attributesK, (empty, prep_ext, merge, print))];
wenzelm@4780
   122
end;
wenzelm@4780
   123
wenzelm@4780
   124
wenzelm@4780
   125
(* get data record *)
wenzelm@4780
   126
wenzelm@4780
   127
fun get_attributes_sg sg =
wenzelm@4780
   128
  (case Sign.get_data sg attributesK of
wenzelm@4780
   129
    Attributes x => x
wenzelm@4780
   130
  | _ => sys_error "get_attributes_sg");
wenzelm@4780
   131
wenzelm@4780
   132
val get_attributes = get_attributes_sg o Theory.sign_of;
wenzelm@4780
   133
wenzelm@4780
   134
wenzelm@4780
   135
(* get global / local attributes *)
wenzelm@4780
   136
wenzelm@4790
   137
fun attrs which thy (raw_name, args) =
wenzelm@4780
   138
  let
wenzelm@4780
   139
    val {space, attrs} = get_attributes thy;
wenzelm@4780
   140
    val name = NameSpace.intern space raw_name;
wenzelm@4780
   141
  in
wenzelm@4780
   142
    (case Symtab.lookup (attrs, name) of
wenzelm@4780
   143
      None => error ("Unknown attribute: " ^ quote name)
wenzelm@4780
   144
    | Some p => which p args)
wenzelm@4780
   145
  end;
wenzelm@4780
   146
wenzelm@4780
   147
val global_attr = attrs fst;
wenzelm@4780
   148
val local_attr = attrs snd;
wenzelm@4780
   149
wenzelm@4780
   150
wenzelm@4780
   151
(* add_attrs *)
wenzelm@4780
   152
wenzelm@4780
   153
fun add_attrs raw_attrs thy =
wenzelm@4780
   154
  let
wenzelm@4780
   155
    val full = Sign.full_name (Theory.sign_of thy);
wenzelm@4780
   156
    val new_attrs = map (apfst full) raw_attrs;
wenzelm@4780
   157
wenzelm@4780
   158
    val {space, attrs} = get_attributes thy;
wenzelm@4780
   159
    val space' = NameSpace.extend (space, map fst new_attrs);
wenzelm@4780
   160
    val attrs' = Symtab.extend (attrs, new_attrs)
wenzelm@4780
   161
      handle Symtab.DUPS dups =>
wenzelm@4780
   162
        error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
wenzelm@4780
   163
  in
wenzelm@4780
   164
    Theory.put_data (attributesK, Attributes {space = space', attrs = attrs'}) thy
wenzelm@4780
   165
  end;
wenzelm@4780
   166
wenzelm@4780
   167
wenzelm@4780
   168
end;
wenzelm@4780
   169
wenzelm@4780
   170
wenzelm@4780
   171
structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
wenzelm@4780
   172
open BasicAttribute;