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