src/Pure/attribute.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 6000 aa84c30c1f61
permissions -rw-r--r--
tidying
     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 show_tags: bool ref
    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 thms_of: tthm list -> thm list
    22   val tthms_of: thm list -> tthm list
    23   val rule: ('a -> thm -> thm) -> 'a attribute
    24   val none: 'a -> 'a * 'b attribute list
    25   val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
    26   val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
    27   val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
    28   val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
    29   val pretty_tthm: tthm -> Pretty.T
    30   val pretty_tthms: tthm list -> Pretty.T
    31   val print_tthm: tthm -> unit
    32   val print_tthms: tthm list -> unit
    33   val tag: tag -> 'a attribute
    34   val untag: tag -> 'a attribute
    35   val lemma: tag
    36   val assumption: tag
    37   val internal: tag
    38   val tag_lemma: 'a attribute
    39   val tag_assumption: 'a attribute
    40   val tag_internal: 'a attribute
    41 end;
    42 
    43 structure Attribute: ATTRIBUTE =
    44 struct
    45 
    46 
    47 (** tags and attributes **)
    48 
    49 type tag = string * string list;
    50 type tthm = thm * tag list;
    51 type 'a attribute = 'a * tthm -> 'a * tthm;
    52 
    53 fun thm_of (thm, _) = thm;
    54 fun tthm_of thm = (thm, []);
    55 
    56 fun thms_of ths = map thm_of ths;
    57 fun tthms_of ths = map tthm_of ths;
    58 
    59 fun rule f (x, (thm, _)) = (x, (f x thm, []));
    60 
    61 fun none x = (x, []);
    62 fun no_attrs (x, y) = ((x, (y, [])), []);
    63 fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);
    64 
    65 
    66 (* apply attributes *)
    67 
    68 fun apply (x_th, atts) = Library.apply atts x_th;
    69 fun applys (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
    70 
    71 
    72 (* display tagged theorems *)
    73 
    74 val show_tags = ref false;
    75 
    76 fun pretty_tag (name, args) = Pretty.strs (name :: args);
    77 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    78 
    79 fun pretty_tthm (thm, tags) =
    80   if null tags orelse not (! show_tags) then Pretty.quote (Display.pretty_thm thm)
    81   else Pretty.block [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
    82 
    83 fun pretty_tthms [th] = pretty_tthm th
    84   | pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));
    85 
    86 val print_tthm = Pretty.writeln o pretty_tthm;
    87 val print_tthms = Pretty.writeln o pretty_tthms;
    88 
    89 
    90 (* basic attributes *)
    91 
    92 fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
    93 fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
    94 
    95 val lemma = ("lemma", []);
    96 val assumption = ("assumption", []);
    97 val internal = ("internal", []);
    98 fun tag_lemma x = tag lemma x;
    99 fun tag_assumption x = tag assumption x;
   100 fun tag_internal x = tag internal x;
   101 
   102 
   103 end;
   104 
   105 
   106 structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
   107 open BasicAttribute;