src/Pure/Isar/attrib.ML
author wenzelm
Mon Nov 09 15:32:20 1998 +0100 (1998-11-09)
changeset 5823 ee7c198a2154
child 5879 18b8f048d93a
permissions -rw-r--r--
Symbolic theorem attributes.
     1 (*  Title:      Pure/Isar/attrib.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Symbolic theorem attributes.
     6 *)
     7 
     8 signature BASIC_ATTRIB =
     9 sig
    10   val print_attributes: theory -> unit
    11 end;
    12 
    13 signature ATTRIB =
    14 sig
    15   include BASIC_ATTRIB
    16   val global_attribute: theory -> Args.src -> theory attribute
    17   val local_attribute: theory -> Args.src -> Proof.context attribute
    18   val add_attributes: (bstring * ((Args.src -> theory attribute) *
    19       (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
    20   val syntax: (Args.T list -> 'a * Args.T list) -> ('a -> 'b) -> Args.src -> 'b
    21   val no_args: 'a attribute -> Args.src -> 'a attribute
    22   val thm_args: ('a -> string list -> tthm list)
    23     -> (tthm list -> 'a attribute) -> Args.src -> 'a attribute
    24   val global_thm_args: (tthm list -> theory attribute) -> Args.src -> theory attribute
    25   val local_thm_args: (tthm list -> Proof.context attribute)
    26     -> Args.src -> Proof.context attribute
    27   val setup: (theory -> theory) list
    28 end;
    29 
    30 structure Attrib: ATTRIB =
    31 struct
    32 
    33 
    34 (** attributes theory data **)
    35 
    36 (* data kind 'Isar/attributes' *)
    37 
    38 structure AttributesDataArgs =
    39 struct
    40   val name = "Isar/attributes";
    41   type T =
    42     {space: NameSpace.T,
    43      attrs:
    44        ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute))
    45          * string) * stamp) Symtab.table};
    46 
    47   val empty = {space = NameSpace.empty, attrs = Symtab.empty};
    48   val prep_ext = I;
    49 
    50   fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
    51     {space = NameSpace.merge (space1, space2),
    52       attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
    53         error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
    54 
    55   fun print _ ({space, attrs}) =
    56     let
    57       fun prt_attr (name, ((_, comment), _)) = Pretty.block
    58         [Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];
    59     in
    60       Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
    61       Pretty.writeln (Pretty.big_list "attributes:" (map prt_attr (Symtab.dest attrs)))
    62     end;
    63 end;
    64 
    65 structure AttributesData = TheoryDataFun(AttributesDataArgs);
    66 val print_attributes = AttributesData.print;
    67 
    68 
    69 (* get global / local attributes *)
    70 
    71 fun gen_attribute which thy =
    72   let
    73     val {space, attrs} = AttributesData.get thy;
    74 
    75     fun attr ((raw_name, args), pos) =
    76       let val name = NameSpace.intern space raw_name in
    77         (case Symtab.lookup (attrs, name) of
    78           None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    79         | Some ((p, _), _) => which p ((name, args), pos))
    80       end;
    81   in attr end;
    82 
    83 val global_attribute = gen_attribute fst;
    84 val local_attribute = gen_attribute snd;
    85 
    86 
    87 (* add_attributes *)
    88 
    89 fun add_attributes raw_attrs thy =
    90   let
    91     val full = Sign.full_name (Theory.sign_of thy);
    92     val new_attrs =
    93       map (fn (name, (f, g), comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs;
    94 
    95     val {space, attrs} = AttributesData.get thy;
    96     val space' = NameSpace.extend (space, map fst new_attrs);
    97     val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups =>
    98       error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
    99   in thy |> AttributesData.put {space = space', attrs = attrs'} end;
   100 
   101 
   102 (* attribute syntax *)
   103 
   104 val attributeN = "attribute";
   105 fun syntax scan = Args.syntax attributeN scan;
   106 
   107 fun no_args x = syntax (Scan.succeed x) I;
   108 
   109 fun thm_args get f = syntax (Scan.repeat Args.name)
   110   (fn names => fn (x, ths) => f (get x names) (x, ths));
   111 
   112 fun global_thm_args f = thm_args PureThy.get_tthmss f;
   113 fun local_thm_args f = thm_args ProofContext.get_tthmss f;
   114 
   115 
   116 
   117 (** Pure attributes **)
   118 
   119 (* tags *)
   120 
   121 fun gen_tag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.tag x;
   122 fun gen_untag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.untag x;
   123 fun gen_lemma x = no_args Attribute.tag_lemma x;
   124 fun gen_assumption x = no_args Attribute.tag_assumption x;
   125 
   126 
   127 (* resolution *)
   128 
   129 fun gen_RS get = syntax Args.name
   130   (fn name => fn (x, (thm, tags)) => (x, (thm RS (Attribute.thm_of (get x name)), tags)));
   131 
   132 fun RS_global x = gen_RS PureThy.get_tthm x;
   133 fun RS_local x = gen_RS ProofContext.get_tthm x;
   134 
   135 
   136 (* pure_attributes *)
   137 
   138 val pure_attributes =
   139  [("tag", (gen_tag, gen_tag), "tag theorem"),
   140   ("untag", (gen_untag, gen_untag), "untag theorem"),
   141   ("lemma", (gen_lemma, gen_lemma), "tag as lemma"),
   142   ("assumption", (gen_assumption, gen_assumption), "tag as assumption"),
   143   ("RS", (RS_global, RS_local), "resolve with rule")];
   144 
   145 
   146 
   147 (** theory setup **)
   148 
   149 val setup = [AttributesData.init, add_attributes pure_attributes];
   150 
   151 
   152 end;
   153 
   154 
   155 structure BasicAttrib: BASIC_ATTRIB = Attrib;
   156 open BasicAttrib;