src/HOL/ex/reflection_data.ML
author chaieb
Tue Jul 03 17:49:53 2007 +0200 (2007-07-03)
changeset 23545 2fddae6056ab
child 23606 60950b22dcbf
permissions -rw-r--r--
Context Data for the reflection and reification methods
chaieb@23545
     1
(*  Title:      HOL/ex/reflection_data.ML
chaieb@23545
     2
    ID:         $Id$
chaieb@23545
     3
    Author:     Amine Chaieb, TU Muenchen
chaieb@23545
     4
chaieb@23545
     5
Data for the reification and  reflection Methods
chaieb@23545
     6
*)
chaieb@23545
     7
chaieb@23545
     8
signature REIFY_DATA =
chaieb@23545
     9
sig
chaieb@23545
    10
  type entry
chaieb@23545
    11
  val get: Proof.context -> entry
chaieb@23545
    12
  val del: thm list -> attribute
chaieb@23545
    13
  val add: thm list -> attribute 
chaieb@23545
    14
  val setup: theory -> theory
chaieb@23545
    15
end;
chaieb@23545
    16
chaieb@23545
    17
structure Reify_Data : REIFY_DATA =
chaieb@23545
    18
struct
chaieb@23545
    19
chaieb@23545
    20
type entry = thm list;
chaieb@23545
    21
chaieb@23545
    22
structure Data = GenericDataFun
chaieb@23545
    23
( val name = "Reify-Data";
chaieb@23545
    24
  type T = thm list
chaieb@23545
    25
  val empty = [];
chaieb@23545
    26
  val extend = I
chaieb@23545
    27
  fun merge _ = Library.merge Thm.eq_thm);
chaieb@23545
    28
chaieb@23545
    29
val get = Data.get o Context.Proof;
chaieb@23545
    30
chaieb@23545
    31
fun add ths = Thm.declaration_attribute (fn th => fn context => 
chaieb@23545
    32
  context |> Data.map (fn x => merge Thm.eq_thm (x,ths)))
chaieb@23545
    33
chaieb@23545
    34
fun del ths = Thm.declaration_attribute (fn th => fn context => 
chaieb@23545
    35
  context |> Data.map (fn x => subtract Thm.eq_thm x ths))
chaieb@23545
    36
chaieb@23545
    37
(* concrete syntax *)
chaieb@23545
    38
local
chaieb@23545
    39
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
chaieb@23545
    40
chaieb@23545
    41
val constsN = "consts";
chaieb@23545
    42
val addN = "add";
chaieb@23545
    43
val delN = "del";
chaieb@23545
    44
val any_keyword = keyword constsN || keyword addN || keyword delN;
chaieb@23545
    45
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
chaieb@23545
    46
val terms = thms >> map (term_of o Drule.dest_term);
chaieb@23545
    47
chaieb@23545
    48
fun optional scan = Scan.optional scan [];
chaieb@23545
    49
chaieb@23545
    50
in
chaieb@23545
    51
fun att_syntax src = src |> Attrib.syntax
chaieb@23545
    52
 ((Scan.lift (Args.$$$ "del") |-- thms) >> del ||
chaieb@23545
    53
  optional (keyword addN |-- thms) >> add)
chaieb@23545
    54
end;
chaieb@23545
    55
chaieb@23545
    56
chaieb@23545
    57
(* theory setup *)
chaieb@23545
    58
 val setup =
chaieb@23545
    59
  Attrib.add_attributes [("reify", att_syntax, "Reify data")];
chaieb@23545
    60
end;