src/Pure/Isar/attrib.ML
changeset 5823 ee7c198a2154
child 5879 18b8f048d93a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 09 15:32:20 1998 +0100
     1.3 @@ -0,0 +1,156 @@
     1.4 +(*  Title:      Pure/Isar/attrib.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Symbolic theorem attributes.
     1.9 +*)
    1.10 +
    1.11 +signature BASIC_ATTRIB =
    1.12 +sig
    1.13 +  val print_attributes: theory -> unit
    1.14 +end;
    1.15 +
    1.16 +signature ATTRIB =
    1.17 +sig
    1.18 +  include BASIC_ATTRIB
    1.19 +  val global_attribute: theory -> Args.src -> theory attribute
    1.20 +  val local_attribute: theory -> Args.src -> Proof.context attribute
    1.21 +  val add_attributes: (bstring * ((Args.src -> theory attribute) *
    1.22 +      (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
    1.23 +  val syntax: (Args.T list -> 'a * Args.T list) -> ('a -> 'b) -> Args.src -> 'b
    1.24 +  val no_args: 'a attribute -> Args.src -> 'a attribute
    1.25 +  val thm_args: ('a -> string list -> tthm list)
    1.26 +    -> (tthm list -> 'a attribute) -> Args.src -> 'a attribute
    1.27 +  val global_thm_args: (tthm list -> theory attribute) -> Args.src -> theory attribute
    1.28 +  val local_thm_args: (tthm list -> Proof.context attribute)
    1.29 +    -> Args.src -> Proof.context attribute
    1.30 +  val setup: (theory -> theory) list
    1.31 +end;
    1.32 +
    1.33 +structure Attrib: ATTRIB =
    1.34 +struct
    1.35 +
    1.36 +
    1.37 +(** attributes theory data **)
    1.38 +
    1.39 +(* data kind 'Isar/attributes' *)
    1.40 +
    1.41 +structure AttributesDataArgs =
    1.42 +struct
    1.43 +  val name = "Isar/attributes";
    1.44 +  type T =
    1.45 +    {space: NameSpace.T,
    1.46 +     attrs:
    1.47 +       ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute))
    1.48 +         * string) * stamp) Symtab.table};
    1.49 +
    1.50 +  val empty = {space = NameSpace.empty, attrs = Symtab.empty};
    1.51 +  val prep_ext = I;
    1.52 +
    1.53 +  fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
    1.54 +    {space = NameSpace.merge (space1, space2),
    1.55 +      attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
    1.56 +        error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
    1.57 +
    1.58 +  fun print _ ({space, attrs}) =
    1.59 +    let
    1.60 +      fun prt_attr (name, ((_, comment), _)) = Pretty.block
    1.61 +        [Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.62 +    in
    1.63 +      Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
    1.64 +      Pretty.writeln (Pretty.big_list "attributes:" (map prt_attr (Symtab.dest attrs)))
    1.65 +    end;
    1.66 +end;
    1.67 +
    1.68 +structure AttributesData = TheoryDataFun(AttributesDataArgs);
    1.69 +val print_attributes = AttributesData.print;
    1.70 +
    1.71 +
    1.72 +(* get global / local attributes *)
    1.73 +
    1.74 +fun gen_attribute which thy =
    1.75 +  let
    1.76 +    val {space, attrs} = AttributesData.get thy;
    1.77 +
    1.78 +    fun attr ((raw_name, args), pos) =
    1.79 +      let val name = NameSpace.intern space raw_name in
    1.80 +        (case Symtab.lookup (attrs, name) of
    1.81 +          None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    1.82 +        | Some ((p, _), _) => which p ((name, args), pos))
    1.83 +      end;
    1.84 +  in attr end;
    1.85 +
    1.86 +val global_attribute = gen_attribute fst;
    1.87 +val local_attribute = gen_attribute snd;
    1.88 +
    1.89 +
    1.90 +(* add_attributes *)
    1.91 +
    1.92 +fun add_attributes raw_attrs thy =
    1.93 +  let
    1.94 +    val full = Sign.full_name (Theory.sign_of thy);
    1.95 +    val new_attrs =
    1.96 +      map (fn (name, (f, g), comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs;
    1.97 +
    1.98 +    val {space, attrs} = AttributesData.get thy;
    1.99 +    val space' = NameSpace.extend (space, map fst new_attrs);
   1.100 +    val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups =>
   1.101 +      error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   1.102 +  in thy |> AttributesData.put {space = space', attrs = attrs'} end;
   1.103 +
   1.104 +
   1.105 +(* attribute syntax *)
   1.106 +
   1.107 +val attributeN = "attribute";
   1.108 +fun syntax scan = Args.syntax attributeN scan;
   1.109 +
   1.110 +fun no_args x = syntax (Scan.succeed x) I;
   1.111 +
   1.112 +fun thm_args get f = syntax (Scan.repeat Args.name)
   1.113 +  (fn names => fn (x, ths) => f (get x names) (x, ths));
   1.114 +
   1.115 +fun global_thm_args f = thm_args PureThy.get_tthmss f;
   1.116 +fun local_thm_args f = thm_args ProofContext.get_tthmss f;
   1.117 +
   1.118 +
   1.119 +
   1.120 +(** Pure attributes **)
   1.121 +
   1.122 +(* tags *)
   1.123 +
   1.124 +fun gen_tag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.tag x;
   1.125 +fun gen_untag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.untag x;
   1.126 +fun gen_lemma x = no_args Attribute.tag_lemma x;
   1.127 +fun gen_assumption x = no_args Attribute.tag_assumption x;
   1.128 +
   1.129 +
   1.130 +(* resolution *)
   1.131 +
   1.132 +fun gen_RS get = syntax Args.name
   1.133 +  (fn name => fn (x, (thm, tags)) => (x, (thm RS (Attribute.thm_of (get x name)), tags)));
   1.134 +
   1.135 +fun RS_global x = gen_RS PureThy.get_tthm x;
   1.136 +fun RS_local x = gen_RS ProofContext.get_tthm x;
   1.137 +
   1.138 +
   1.139 +(* pure_attributes *)
   1.140 +
   1.141 +val pure_attributes =
   1.142 + [("tag", (gen_tag, gen_tag), "tag theorem"),
   1.143 +  ("untag", (gen_untag, gen_untag), "untag theorem"),
   1.144 +  ("lemma", (gen_lemma, gen_lemma), "tag as lemma"),
   1.145 +  ("assumption", (gen_assumption, gen_assumption), "tag as assumption"),
   1.146 +  ("RS", (RS_global, RS_local), "resolve with rule")];
   1.147 +
   1.148 +
   1.149 +
   1.150 +(** theory setup **)
   1.151 +
   1.152 +val setup = [AttributesData.init, add_attributes pure_attributes];
   1.153 +
   1.154 +
   1.155 +end;
   1.156 +
   1.157 +
   1.158 +structure BasicAttrib: BASIC_ATTRIB = Attrib;
   1.159 +open BasicAttrib;