src/Pure/attribute.ML

added lift_modifier, rule;

(*  Title:      Pure/attribute.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Theorem tags and attributes.
*)

signature BASIC_ATTRIBUTE =
sig
  type tag
  type tthm
  type 'a attribute
end;

signature ATTRIBUTE =
sig
  include BASIC_ATTRIBUTE
  val thm_of: tthm -> thm
  val tthm_of: thm -> tthm
  val lift_modifier: ('a * thm list -> 'b) -> 'a * tthm list -> 'b
  val rule: ('b -> 'a) -> ('a -> thm -> thm) -> 'b attribute
  val none: 'a -> 'a * 'b attribute list
  val no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list
  val no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list
  val fail: string -> string -> 'a
  val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
  val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
  val pretty_tthm: tthm -> Pretty.T
  val tag: tag -> 'a attribute
  val untag: tag -> 'a attribute
  val lemma: tag
  val assumption: tag
  val internal: tag
  val tag_lemma: 'a attribute
  val tag_assumption: 'a attribute
  val tag_internal: 'a attribute
end;

structure Attribute: ATTRIBUTE =
struct


(** tags and attributes **)

type tag = string * string list;
type tthm = thm * tag list;
type 'a attribute = 'a * tthm -> 'a * tthm;

fun thm_of (thm, _) = thm;
fun tthm_of thm = (thm, []);

fun lift_modifier f (x, tthms) = f (x, map thm_of tthms);

fun rule get_data f (x, (thm, tags)) = (x, (f (get_data x) thm, tags));

fun none x = (x, []);
fun no_attrs (x, y) = ((x, (y, [])), []);
fun no_attrss (x, ys) = ((x, map (rpair []) ys), []);


(* apply attributes *)

exception FAIL of string * string;

fun fail name msg = raise FAIL (name, msg);

(* FIXME error (!!?), push up the warning (??) *)
fun warn_failed (name, msg) =
  warning ("Failed invocation of " ^ quote name ^ " attribute: " ^ msg);

fun apply (x_th, []) = x_th
  | apply (x_th, f :: fs) = apply (f x_th handle FAIL info => (warn_failed info; x_th), fs);

fun applys ((x, []), _) = (x, [])
  | applys ((x, th :: ths), atts) =
      let
        val (x', th') = apply ((x, th), atts);
        val (x'', ths') = applys ((x', ths), atts);
      in (x'', th' :: ths') end;


(* display tagged theorems *)

fun pretty_tag (name, args) = Pretty.strs (name :: args);
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;

fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
  | pretty_tthm (thm, tags) = Pretty.block
      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];


(* basic attributes *)

fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));

val lemma = ("lemma", []);
val assumption = ("assumption", []);
val internal = ("internal", []);
fun tag_lemma x = tag lemma x;
fun tag_assumption x = tag assumption x;
fun tag_internal x = tag internal x;


end;


structure BasicAttribute: BASIC_ATTRIBUTE = Attribute;
open BasicAttribute;