src/HOL/Tools/res_atpset.ML
changeset 19159 f737ecbad1c4
child 19170 a55a3464a1de
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/res_atpset.ML	Wed Mar 01 05:56:53 2006 +0100
     1.3 @@ -0,0 +1,109 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Jia Meng, NICTA 
     1.6 +
     1.7 +Set of rules used for ATPs
     1.8 +*)
     1.9 +
    1.10 +structure ResAtpSet =
    1.11 +
    1.12 +struct
    1.13 +
    1.14 +datatype atpset = AtpSet of thm list
    1.15 +
    1.16 +
    1.17 +val mem_thm = member Drule.eq_thm_prop;
    1.18 +val rem_thm = remove Drule.eq_thm_prop;
    1.19 +
    1.20 +val empty_atpset = AtpSet [];
    1.21 +
    1.22 +fun add_atp_rule (thm,AtpSet thms) = 
    1.23 +    if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms)
    1.24 +    else
    1.25 +	AtpSet (thm::thms);
    1.26 +
    1.27 +fun add_atp_rule' thm ars = add_atp_rule (thm,ars);
    1.28 +fun add_atp_rules (ars,thms) =  foldl add_atp_rule ars thms;
    1.29 +
    1.30 +fun del_atp_rule (thm,AtpSet thms) = 
    1.31 +    if mem_thm thms thm then AtpSet (rem_thm thm thms)
    1.32 +    else
    1.33 +	(warning "Undeclared rule for ATPs"; AtpSet thms);
    1.34 +
    1.35 +fun del_atp_rule' thm ars = del_atp_rule (thm,ars);
    1.36 +
    1.37 +fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms;
    1.38 +
    1.39 +fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2);
    1.40 +
    1.41 +fun print_atpset (AtpSet thms) =
    1.42 +    let val pretty_thms = map Display.pretty_thm in
    1.43 +	[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)]
    1.44 +	    |> Pretty.chunks |> Pretty.writeln
    1.45 +    end;
    1.46 +
    1.47 +
    1.48 +(* global AtpSet *)
    1.49 +
    1.50 +structure GlobalAtpSet = TheoryDataFun
    1.51 +(struct
    1.52 +  val name = "AtpSet";
    1.53 +  type T = atpset ref;
    1.54 +  
    1.55 +  val empty = ref empty_atpset;
    1.56 +  fun copy (ref atpst) = ref atpst : T;
    1.57 +  val extend = copy;
    1.58 +  fun merge _ (ref atpst1, ref atpst2) =
    1.59 +      ref (merge_atpset (atpst1, atpst2));
    1.60 +  fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
    1.61 +end);
    1.62 +
    1.63 +val print_AtpSet = GlobalAtpSet.print; 
    1.64 +val get_AtpSet = ! o GlobalAtpSet.get;
    1.65 +
    1.66 +val change_AtpSet_of = change o GlobalAtpSet.get;
    1.67 +fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f;
    1.68 +
    1.69 +
    1.70 +fun AtpSet_of thy = get_AtpSet thy;
    1.71 +
    1.72 +fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args));
    1.73 +
    1.74 +fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));
    1.75 +
    1.76 +
    1.77 +(* local AtpSet *)
    1.78 +
    1.79 +structure LocalAtpSet = ProofDataFun
    1.80 +(struct
    1.81 +  val name = "AtpSet";
    1.82 +  type T = atpset;
    1.83 +  val init = get_AtpSet;
    1.84 +  fun print _ atpst = print_atpset atpst;
    1.85 +end);
    1.86 +
    1.87 +val print_local_AtpSet = LocalAtpSet.print;
    1.88 +
    1.89 +val get_local_AtpSet = LocalAtpSet.get;
    1.90 +
    1.91 +val put_local_AtpSet = LocalAtpSet.put;
    1.92 +
    1.93 +fun local_AtpSet_of ctxt = get_local_AtpSet;
    1.94 +
    1.95 +
    1.96 +(* attributes *)
    1.97 +fun attrib f = Thm.declaration_attribute (fn th =>
    1.98 +   fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy)
    1.99 +    | Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt));
   1.100 +
   1.101 +
   1.102 +val add_rule = attrib add_atp_rule';
   1.103 +val del_rule = attrib del_atp_rule';
   1.104 +
   1.105 +val atpN = "atp";
   1.106 +
   1.107 +val setup_attrs = Attrib.add_attributes
   1.108 +[(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")];
   1.109 +
   1.110 +val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
   1.111 +
   1.112 +end;
   1.113 \ No newline at end of file