src/HOL/Tools/res_atpset.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 19170 a55a3464a1de
child 20547 796ae7fa1049
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
mengj@19159
     1
(*  ID:         $Id$
mengj@19159
     2
    Author:     Jia Meng, NICTA 
mengj@19159
     3
mengj@19159
     4
Set of rules used for ATPs
mengj@19159
     5
*)
mengj@19159
     6
mengj@19170
     7
signature RES_ATPSET =
mengj@19170
     8
sig
mengj@19170
     9
    type atpset
mengj@19170
    10
    val local_AtpSet_of: Proof.context -> atpset
mengj@19170
    11
    val add_atp_rules: atpset * Thm.thm list -> atpset
mengj@19170
    12
    val del_atp_rules: atpset * Thm.thm list -> atpset
mengj@19170
    13
    val get_AtpSet: theory -> atpset
mengj@19170
    14
    val print_local_AtpSet: Proof.context -> unit
mengj@19170
    15
    val AtpSet_of: theory -> atpset
mengj@19170
    16
    val add_atp_rule: Thm.thm * atpset -> atpset
mengj@19170
    17
    val del_atp_rule: Thm.thm * atpset -> atpset
mengj@19170
    18
    val print_atpset: atpset -> unit
mengj@19170
    19
    val setup: theory -> theory
mengj@19170
    20
    val get_local_AtpSet: Proof.context -> atpset
mengj@19170
    21
    val rep_as: atpset -> Thm.thm list
mengj@19170
    22
    val merge_atpset: atpset * atpset -> atpset
mengj@19170
    23
    val add_atp_rule': Thm.thm -> atpset -> atpset
mengj@19170
    24
    val del_atp_rule': Thm.thm -> atpset -> atpset
mengj@19170
    25
    val Add_AtpRs: Thm.thm list -> unit
mengj@19170
    26
    val Del_AtpRs: Thm.thm list -> unit
mengj@19170
    27
    val empty_atpset: atpset
mengj@19170
    28
    val put_local_AtpSet: atpset -> Proof.context -> Proof.context
mengj@19170
    29
    val print_AtpSet: theory -> unit
mengj@19170
    30
    val atp_rules_of_thy: theory -> Thm.thm list
mengj@19170
    31
    val atp_rules_of_ctxt: Proof.context -> Thm.thm list
mengj@19170
    32
end;
mengj@19170
    33
mengj@19170
    34
mengj@19170
    35
mengj@19170
    36
structure ResAtpSet : RES_ATPSET =
mengj@19159
    37
mengj@19159
    38
struct
mengj@19159
    39
mengj@19159
    40
datatype atpset = AtpSet of thm list
mengj@19159
    41
mengj@19159
    42
mengj@19159
    43
val mem_thm = member Drule.eq_thm_prop;
mengj@19159
    44
val rem_thm = remove Drule.eq_thm_prop;
mengj@19159
    45
mengj@19159
    46
val empty_atpset = AtpSet [];
mengj@19159
    47
mengj@19159
    48
fun add_atp_rule (thm,AtpSet thms) = 
mengj@19159
    49
    if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms)
mengj@19159
    50
    else
mengj@19159
    51
	AtpSet (thm::thms);
mengj@19159
    52
mengj@19159
    53
fun add_atp_rule' thm ars = add_atp_rule (thm,ars);
mengj@19159
    54
fun add_atp_rules (ars,thms) =  foldl add_atp_rule ars thms;
mengj@19159
    55
mengj@19159
    56
fun del_atp_rule (thm,AtpSet thms) = 
mengj@19159
    57
    if mem_thm thms thm then AtpSet (rem_thm thm thms)
mengj@19159
    58
    else
mengj@19159
    59
	(warning "Undeclared rule for ATPs"; AtpSet thms);
mengj@19159
    60
mengj@19159
    61
fun del_atp_rule' thm ars = del_atp_rule (thm,ars);
mengj@19159
    62
mengj@19159
    63
fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms;
mengj@19159
    64
mengj@19159
    65
fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2);
mengj@19159
    66
mengj@19159
    67
fun print_atpset (AtpSet thms) =
mengj@19159
    68
    let val pretty_thms = map Display.pretty_thm in
mengj@19159
    69
	[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)]
mengj@19159
    70
	    |> Pretty.chunks |> Pretty.writeln
mengj@19159
    71
    end;
mengj@19159
    72
mengj@19170
    73
fun rep_as (AtpSet thms) = thms;
mengj@19159
    74
mengj@19159
    75
(* global AtpSet *)
mengj@19159
    76
mengj@19159
    77
structure GlobalAtpSet = TheoryDataFun
mengj@19159
    78
(struct
mengj@19159
    79
  val name = "AtpSet";
mengj@19159
    80
  type T = atpset ref;
mengj@19159
    81
  
mengj@19159
    82
  val empty = ref empty_atpset;
mengj@19159
    83
  fun copy (ref atpst) = ref atpst : T;
mengj@19159
    84
  val extend = copy;
mengj@19159
    85
  fun merge _ (ref atpst1, ref atpst2) =
mengj@19159
    86
      ref (merge_atpset (atpst1, atpst2));
mengj@19159
    87
  fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
mengj@19159
    88
end);
mengj@19159
    89
mengj@19159
    90
val print_AtpSet = GlobalAtpSet.print; 
mengj@19159
    91
val get_AtpSet = ! o GlobalAtpSet.get;
mengj@19159
    92
mengj@19159
    93
val change_AtpSet_of = change o GlobalAtpSet.get;
mengj@19159
    94
fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f;
mengj@19159
    95
mengj@19159
    96
mengj@19159
    97
fun AtpSet_of thy = get_AtpSet thy;
mengj@19159
    98
mengj@19159
    99
fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args));
mengj@19159
   100
mengj@19159
   101
fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));
mengj@19159
   102
mengj@19170
   103
fun atp_rules_of_thy thy = rep_as (AtpSet_of thy);
mengj@19159
   104
mengj@19159
   105
(* local AtpSet *)
mengj@19159
   106
mengj@19159
   107
structure LocalAtpSet = ProofDataFun
mengj@19159
   108
(struct
mengj@19159
   109
  val name = "AtpSet";
mengj@19159
   110
  type T = atpset;
mengj@19159
   111
  val init = get_AtpSet;
mengj@19159
   112
  fun print _ atpst = print_atpset atpst;
mengj@19159
   113
end);
mengj@19159
   114
mengj@19159
   115
val print_local_AtpSet = LocalAtpSet.print;
mengj@19159
   116
mengj@19159
   117
val get_local_AtpSet = LocalAtpSet.get;
mengj@19159
   118
mengj@19159
   119
val put_local_AtpSet = LocalAtpSet.put;
mengj@19159
   120
mengj@19170
   121
fun local_AtpSet_of ctxt = get_local_AtpSet ctxt;
mengj@19159
   122
mengj@19170
   123
fun atp_rules_of_ctxt ctxt = rep_as (local_AtpSet_of ctxt);
mengj@19159
   124
mengj@19159
   125
(* attributes *)
mengj@19159
   126
fun attrib f = Thm.declaration_attribute (fn th =>
mengj@19159
   127
   fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy)
mengj@19159
   128
    | Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt));
mengj@19159
   129
mengj@19159
   130
mengj@19159
   131
val add_rule = attrib add_atp_rule';
mengj@19159
   132
val del_rule = attrib del_atp_rule';
mengj@19159
   133
mengj@19159
   134
val atpN = "atp";
mengj@19159
   135
mengj@19159
   136
val setup_attrs = Attrib.add_attributes
mengj@19159
   137
[(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")];
mengj@19159
   138
mengj@19159
   139
val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
mengj@19159
   140
mengj@19159
   141
end;