src/Pure/attribute.ML
author wenzelm
Wed Apr 29 11:24:58 1998 +0200 (1998-04-29)
changeset 4850 050481f41e28
parent 4797 d66477d29598
child 4918 f66f67577cf3
permissions -rw-r--r--
added none: 'a -> 'a * 'b attribute list;
added no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list;
added no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list;
added applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list);
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@4850
    21
  val none: 'a -> 'a * 'b attribute list
wenzelm@4850
    22
  val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
wenzelm@4850
    23
  val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
wenzelm@4790
    24
  val fail: string -> string -> 'a
wenzelm@4780
    25
  val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
wenzelm@4850
    26
  val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
wenzelm@4780
    27
  val pretty_tthm: tthm -> Pretty.T
wenzelm@4780
    28
  val tag: tag -> 'a attribute
wenzelm@4790
    29
  val untag: tag -> 'a attribute
wenzelm@4780
    30
  val lemma: tag
wenzelm@4780
    31
  val assumption: tag
wenzelm@4780
    32
  val tag_lemma: 'a attribute
wenzelm@4780
    33
  val tag_assumption: 'a attribute
wenzelm@4780
    34
  val setup: theory -> theory
wenzelm@4790
    35
  val global_attr: theory -> (xstring * string list) -> theory attribute
wenzelm@4790
    36
  val local_attr: theory -> (xstring * string list) -> local_theory attribute
wenzelm@4780
    37
  val add_attrs: (bstring * ((string list -> theory attribute) *
wenzelm@4790
    38
      (string list -> local_theory attribute))) list -> theory -> theory
wenzelm@4780
    39
end;
wenzelm@4780
    40
wenzelm@4780
    41
structure Attribute: ATTRIBUTE =
wenzelm@4780
    42
struct
wenzelm@4780
    43
wenzelm@4780
    44
wenzelm@4780
    45
(** tags and attributes **)
wenzelm@4780
    46
wenzelm@4780
    47
type tag = string * string list;
wenzelm@4780
    48
type tthm = thm * tag list;
wenzelm@4780
    49
type 'a attribute = 'a * tthm -> 'a * tthm;
wenzelm@4780
    50
wenzelm@4780
    51
fun thm_of (thm, _) = thm;
wenzelm@4780
    52
fun tthm_of thm = (thm, []);
wenzelm@4780
    53
wenzelm@4850
    54
fun none x = (x, []);
wenzelm@4850
    55
fun no_attrs (x, y) = ((x, (y, [])), []);
wenzelm@4850
    56
fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
wenzelm@4850
    57
wenzelm@4790
    58
wenzelm@4790
    59
(* apply attributes *)
wenzelm@4790
    60
wenzelm@4790
    61
exception FAIL of string * string;
wenzelm@4790
    62
wenzelm@4790
    63
fun fail name msg = raise FAIL (name, msg);
wenzelm@4790
    64
wenzelm@4790
    65
fun warn_failed (name, msg) =
wenzelm@4797
    66
  warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
wenzelm@4790
    67
wenzelm@4850
    68
fun apply (x_th, []) = x_th
wenzelm@4850
    69
  | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
wenzelm@4850
    70
wenzelm@4850
    71
fun applys ((x, []), _) = (x, [])
wenzelm@4850
    72
  | applys ((x, th :: ths), atts) =
wenzelm@4850
    73
      let
wenzelm@4850
    74
        val (x', th') = apply ((x, th), atts);
wenzelm@4850
    75
        val (x'', ths') = applys ((x', ths), atts);
wenzelm@4850
    76
      in (x'', th' :: ths') end;
wenzelm@4780
    77
wenzelm@4780
    78
wenzelm@4780
    79
(* display tagged theorems *)
wenzelm@4780
    80
wenzelm@4780
    81
fun pretty_tag (name, []) = Pretty.str name
wenzelm@4780
    82
  | pretty_tag (name, args) = Pretty.block
wenzelm@4780
    83
      [Pretty.str name, Pretty.list "(" ")" (map Pretty.str args)];
wenzelm@4780
    84
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@4790
    94
fun tag tg (x, (thm, tags)) = (x, (thm, tg ins tags));
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@4780
    99
fun tag_lemma x = tag lemma x;
wenzelm@4780
   100
fun tag_assumption x = tag assumption x;
wenzelm@4780
   101
wenzelm@4780
   102
wenzelm@4780
   103
wenzelm@4780
   104
(** theory data **)
wenzelm@4780
   105
wenzelm@4780
   106
(* data kind 'attributes' *)
wenzelm@4780
   107
wenzelm@4780
   108
val attributesK = "Pure/attributes";
wenzelm@4780
   109
wenzelm@4780
   110
exception Attributes of
wenzelm@4780
   111
  {space: NameSpace.T,
wenzelm@4780
   112
   attrs:
wenzelm@4780
   113
    ((string list -> theory attribute) *
wenzelm@4790
   114
     (string list -> local_theory attribute)) Symtab.table};
wenzelm@4780
   115
wenzelm@4780
   116
fun print_attributes thy = Display.print_data thy attributesK;
wenzelm@4780
   117
wenzelm@4780
   118
wenzelm@4780
   119
(* setup *)
wenzelm@4780
   120
wenzelm@4780
   121
local
wenzelm@4780
   122
  val empty = Attributes {space = NameSpace.empty, attrs = Symtab.empty};
wenzelm@4780
   123
wenzelm@4780
   124
  fun prep_ext (x as Attributes _) = x;
wenzelm@4780
   125
wenzelm@4780
   126
  fun merge (Attributes {space = space1, attrs = attrs1},
wenzelm@4780
   127
      Attributes {space = space2, attrs = attrs2}) =
wenzelm@4780
   128
    Attributes {
wenzelm@4780
   129
      space = NameSpace.merge (space1, space2),
wenzelm@4780
   130
      attrs = Symtab.merge (K true) (attrs1, attrs2)};
wenzelm@4780
   131
wenzelm@4780
   132
  fun print _ (Attributes {space, attrs}) =
wenzelm@4780
   133
   (Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
wenzelm@4780
   134
    Pretty.writeln (Pretty.strs ("attributes:" :: map fst (Symtab.dest attrs))));
wenzelm@4780
   135
in
wenzelm@4780
   136
  val setup = Theory.init_data [(attributesK, (empty, prep_ext, merge, print))];
wenzelm@4780
   137
end;
wenzelm@4780
   138
wenzelm@4780
   139
wenzelm@4780
   140
(* get data record *)
wenzelm@4780
   141
wenzelm@4780
   142
fun get_attributes_sg sg =
wenzelm@4780
   143
  (case Sign.get_data sg attributesK of
wenzelm@4780
   144
    Attributes x => x
wenzelm@4792
   145
  | _ => type_error attributesK);
wenzelm@4780
   146
wenzelm@4780
   147
val get_attributes = get_attributes_sg o Theory.sign_of;
wenzelm@4780
   148
wenzelm@4780
   149
wenzelm@4780
   150
(* get global / local attributes *)
wenzelm@4780
   151
wenzelm@4850
   152
fun gen_attr which thy (raw_name, args) =
wenzelm@4780
   153
  let
wenzelm@4780
   154
    val {space, attrs} = get_attributes thy;
wenzelm@4780
   155
    val name = NameSpace.intern space raw_name;
wenzelm@4780
   156
  in
wenzelm@4780
   157
    (case Symtab.lookup (attrs, name) of
wenzelm@4797
   158
      None => raise FAIL (name, "unknown attribute")
wenzelm@4780
   159
    | Some p => which p args)
wenzelm@4780
   160
  end;
wenzelm@4780
   161
wenzelm@4850
   162
val global_attr = gen_attr fst;
wenzelm@4850
   163
val local_attr = gen_attr snd;
wenzelm@4780
   164
wenzelm@4780
   165
wenzelm@4780
   166
(* add_attrs *)
wenzelm@4780
   167
wenzelm@4780
   168
fun add_attrs raw_attrs thy =
wenzelm@4780
   169
  let
wenzelm@4780
   170
    val full = Sign.full_name (Theory.sign_of thy);
wenzelm@4780
   171
    val new_attrs = map (apfst full) raw_attrs;
wenzelm@4780
   172
wenzelm@4780
   173
    val {space, attrs} = get_attributes thy;
wenzelm@4780
   174
    val space' = NameSpace.extend (space, map fst new_attrs);
wenzelm@4780
   175
    val attrs' = Symtab.extend (attrs, new_attrs)
wenzelm@4780
   176
      handle Symtab.DUPS dups =>
wenzelm@4780
   177
        error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
wenzelm@4780
   178
  in
wenzelm@4780
   179
    Theory.put_data (attributesK, Attributes {space = space', attrs = attrs'}) thy
wenzelm@4780
   180
  end;
wenzelm@4780
   181
wenzelm@4780
   182
wenzelm@4780
   183
end;
wenzelm@4780
   184
wenzelm@4780
   185
wenzelm@4780
   186
structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
wenzelm@4780
   187
open BasicAttribute;