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;
     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 end;
    14 
    15 signature ATTRIBUTE =
    16 sig
    17   include BASIC_ATTRIBUTE
    18   val thm_of: tthm -> thm
    19   val tthm_of: thm -> tthm
    20   val lift_modifier: ('a * thm list -> 'b) -> 'a * tthm list -> 'b
    21   val rule: ('b -> 'a) -> ('a -> thm -> thm) -> 'b attribute
    22   val none: 'a -> 'a * 'b attribute list
    23   val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
    24   val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
    25   val fail: string -> string -> 'a
    26   val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
    27   val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
    28   val pretty_tthm: tthm -> Pretty.T
    29   val tag: tag -> 'a attribute
    30   val untag: tag -> 'a attribute
    31   val lemma: tag
    32   val assumption: tag
    33   val internal: tag
    34   val tag_lemma: 'a attribute
    35   val tag_assumption: 'a attribute
    36   val tag_internal: 'a attribute
    37 end;
    38 
    39 structure Attribute: ATTRIBUTE =
    40 struct
    41 
    42 
    43 (** tags and attributes **)
    44 
    45 type tag = string * string list;
    46 type tthm = thm * tag list;
    47 type 'a attribute = 'a * tthm -> 'a * tthm;
    48 
    49 fun thm_of (thm, _) = thm;
    50 fun tthm_of thm = (thm, []);
    51 
    52 fun lift_modifier f (x, tthms) = f (x, map thm_of tthms);
    53 
    54 fun rule get_data f (x, (thm, tags)) = (x, (f (get_data x) thm, tags));
    55 
    56 fun none x = (x, []);
    57 fun no_attrs (x, y) = ((x, (y, [])), []);
    58 fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
    59 
    60 
    61 (* apply attributes *)
    62 
    63 exception FAIL of string * string;
    64 
    65 fun fail name msg = raise FAIL (name, msg);
    66 
    67 (* FIXME error (!!?), push up the warning (??) *)
    68 fun warn_failed (name, msg) =
    69   warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);
    70 
    71 fun apply (x_th, []) = x_th
    72   | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);
    73 
    74 fun applys ((x, []), _) = (x, [])
    75   | applys ((x, th :: ths), atts) =
    76       let
    77         val (x', th') = apply ((x, th), atts);
    78         val (x'', ths') = applys ((x', ths), atts);
    79       in (x'', th' :: ths') end;
    80 
    81 
    82 (* display tagged theorems *)
    83 
    84 fun pretty_tag (name, args) = Pretty.strs (name :: args);
    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, if tg mem tags then tags else tags @ [tg]));
    95 fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
    96 
    97 val lemma = ("lemma", []);
    98 val assumption = ("assumption", []);
    99 val internal = ("internal", []);
   100 fun tag_lemma x = tag lemma x;
   101 fun tag_assumption x = tag assumption x;
   102 fun tag_internal x = tag internal x;
   103 
   104 
   105 end;
   106 
   107 
   108 structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
   109 open BasicAttribute;