src/HOL/Tools/res_atpset.ML
author mengj
Wed Mar 01 05:56:53 2006 +0100 (2006-03-01)
changeset 19159 f737ecbad1c4
child 19170 a55a3464a1de
permissions -rw-r--r--
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
     1 (*  ID:         $Id$
     2     Author:     Jia Meng, NICTA 
     3 
     4 Set of rules used for ATPs
     5 *)
     6 
     7 structure ResAtpSet =
     8 
     9 struct
    10 
    11 datatype atpset = AtpSet of thm list
    12 
    13 
    14 val mem_thm = member Drule.eq_thm_prop;
    15 val rem_thm = remove Drule.eq_thm_prop;
    16 
    17 val empty_atpset = AtpSet [];
    18 
    19 fun add_atp_rule (thm,AtpSet thms) = 
    20     if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms)
    21     else
    22 	AtpSet (thm::thms);
    23 
    24 fun add_atp_rule' thm ars = add_atp_rule (thm,ars);
    25 fun add_atp_rules (ars,thms) =  foldl add_atp_rule ars thms;
    26 
    27 fun del_atp_rule (thm,AtpSet thms) = 
    28     if mem_thm thms thm then AtpSet (rem_thm thm thms)
    29     else
    30 	(warning "Undeclared rule for ATPs"; AtpSet thms);
    31 
    32 fun del_atp_rule' thm ars = del_atp_rule (thm,ars);
    33 
    34 fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms;
    35 
    36 fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2);
    37 
    38 fun print_atpset (AtpSet thms) =
    39     let val pretty_thms = map Display.pretty_thm in
    40 	[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)]
    41 	    |> Pretty.chunks |> Pretty.writeln
    42     end;
    43 
    44 
    45 (* global AtpSet *)
    46 
    47 structure GlobalAtpSet = TheoryDataFun
    48 (struct
    49   val name = "AtpSet";
    50   type T = atpset ref;
    51   
    52   val empty = ref empty_atpset;
    53   fun copy (ref atpst) = ref atpst : T;
    54   val extend = copy;
    55   fun merge _ (ref atpst1, ref atpst2) =
    56       ref (merge_atpset (atpst1, atpst2));
    57   fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
    58 end);
    59 
    60 val print_AtpSet = GlobalAtpSet.print; 
    61 val get_AtpSet = ! o GlobalAtpSet.get;
    62 
    63 val change_AtpSet_of = change o GlobalAtpSet.get;
    64 fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f;
    65 
    66 
    67 fun AtpSet_of thy = get_AtpSet thy;
    68 
    69 fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args));
    70 
    71 fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));
    72 
    73 
    74 (* local AtpSet *)
    75 
    76 structure LocalAtpSet = ProofDataFun
    77 (struct
    78   val name = "AtpSet";
    79   type T = atpset;
    80   val init = get_AtpSet;
    81   fun print _ atpst = print_atpset atpst;
    82 end);
    83 
    84 val print_local_AtpSet = LocalAtpSet.print;
    85 
    86 val get_local_AtpSet = LocalAtpSet.get;
    87 
    88 val put_local_AtpSet = LocalAtpSet.put;
    89 
    90 fun local_AtpSet_of ctxt = get_local_AtpSet;
    91 
    92 
    93 (* attributes *)
    94 fun attrib f = Thm.declaration_attribute (fn th =>
    95    fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy)
    96     | Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt));
    97 
    98 
    99 val add_rule = attrib add_atp_rule';
   100 val del_rule = attrib del_atp_rule';
   101 
   102 val atpN = "atp";
   103 
   104 val setup_attrs = Attrib.add_attributes
   105 [(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")];
   106 
   107 val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
   108 
   109 end;