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