removal of some refs
authorpaulson
Fri Aug 10 15:13:18 2007 +0200 (2007-08-10)
changeset 242155458fbf18276
parent 24214 0482ecc4ef11
child 24216 2e2d81b4f184
removal of some refs
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_atp_methods.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 10 14:49:01 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 10 15:13:18 2007 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  signature RES_ATP =
     1.5  sig
     1.6    val prover: string ref
     1.7 -  val custom_spass: string list ref
     1.8    val destdir: string ref
     1.9    val helper_path: string -> string -> string
    1.10    val problem_name: string ref
    1.11 @@ -18,22 +17,12 @@
    1.12    datatype mode = Auto | Fol | Hol
    1.13    val linkup_logic_mode : mode ref
    1.14    val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    1.15 -  val vampire_time: int ref
    1.16 -  val eprover_time: int ref
    1.17 -  val spass_time: int ref
    1.18 -  val run_vampire: int -> unit
    1.19 -  val run_eprover: int -> unit
    1.20 -  val run_spass: int -> unit
    1.21 -  val vampireLimit: unit -> int
    1.22 -  val eproverLimit: unit -> int
    1.23 -  val spassLimit: unit -> int
    1.24    val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    1.25      Method.src -> Proof.context -> Proof.method
    1.26    val cond_rm_tmp: string -> unit
    1.27    val include_all: bool ref
    1.28    val run_relevance_filter: bool ref
    1.29    val run_blacklist_filter: bool ref
    1.30 -  val blacklist: string list ref
    1.31    val add_all : unit -> unit
    1.32    val add_claset : unit -> unit
    1.33    val add_simpset : unit -> unit
    1.34 @@ -61,8 +50,6 @@
    1.35  (********************************************************************)
    1.36  
    1.37  (*** background linkup ***)
    1.38 -val call_atp = ref false;
    1.39 -val hook_count = ref 0;
    1.40  val time_limit = ref 60;
    1.41  val prover = ref "";
    1.42  
    1.43 @@ -84,8 +71,6 @@
    1.44  
    1.45  val _ = set_prover "E"; (* use E as the default prover *)
    1.46  
    1.47 -val custom_spass =   (*specialized options for SPASS*)
    1.48 -      ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    1.49  val destdir = ref "";   (*Empty means write files to /tmp*)
    1.50  val problem_name = ref "prob";
    1.51  
    1.52 @@ -108,29 +93,6 @@
    1.53  
    1.54  fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    1.55  
    1.56 -
    1.57 -(*** ATP methods ***)
    1.58 -val vampire_time = ref 60;
    1.59 -val eprover_time = ref 60;
    1.60 -val spass_time = ref 60;
    1.61 -
    1.62 -fun run_vampire time =
    1.63 -    if (time >0) then vampire_time:= time
    1.64 -    else vampire_time:=60;
    1.65 -
    1.66 -fun run_eprover time =
    1.67 -    if (time > 0) then eprover_time:= time
    1.68 -    else eprover_time:=60;
    1.69 -
    1.70 -fun run_spass time =
    1.71 -    if (time > 0) then spass_time:=time
    1.72 -    else spass_time:=60;
    1.73 -
    1.74 -
    1.75 -fun vampireLimit () = !vampire_time;
    1.76 -fun eproverLimit () = !eprover_time;
    1.77 -fun spassLimit () = !spass_time;
    1.78 -
    1.79  fun atp_input_file () =
    1.80      let val file = !problem_name
    1.81      in
    1.82 @@ -294,8 +256,9 @@
    1.83  
    1.84  (*** white list and black list of lemmas ***)
    1.85  
    1.86 -(*The rule subsetI is frequently omitted by the relevance filter.*)
    1.87 -val whitelist = ref [subsetI];
    1.88 +(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
    1.89 +  or identified with ATPset (which however is too big currently)*)
    1.90 +val whitelist = [subsetI];
    1.91  
    1.92  (*Names of theorems and theorem lists to be blacklisted.
    1.93  
    1.94 @@ -303,7 +266,7 @@
    1.95    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.96    FIXME: this blacklist needs to be maintained using theory data and added to using
    1.97    an attribute.*)
    1.98 -val blacklist = ref
    1.99 +val blacklist = 
   1.100    ["Datatype.prod.size",
   1.101     "Divides.dvd_0_left_iff",
   1.102     "Finite_Set.card_0_eq",
   1.103 @@ -510,7 +473,7 @@
   1.104  
   1.105  fun all_valid_thms ctxt =
   1.106    let
   1.107 -    val banned_tab = foldl setinsert Symtab.empty (!blacklist)
   1.108 +    val banned_tab = foldl setinsert Symtab.empty blacklist
   1.109      fun blacklisted s = !run_blacklist_filter andalso
   1.110                          (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
   1.111  
   1.112 @@ -582,7 +545,7 @@
   1.113          in  claset_thms @ simpset_thms @ atpset_thms  end
   1.114        val user_rules = filter check_named
   1.115                           (map ResAxioms.pairname
   1.116 -                           (if null user_thms then !whitelist else user_thms))
   1.117 +                           (if null user_thms then whitelist else user_thms))
   1.118    in
   1.119        (filter check_named included_thms, user_rules)
   1.120    end;
   1.121 @@ -681,10 +644,10 @@
   1.122    they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   1.123    The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   1.124    leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   1.125 -val unwanted_types = ref ["Product_Type.unit","bool"];
   1.126 +val unwanted_types = ["Product_Type.unit","bool"];
   1.127  
   1.128  fun unwanted t =
   1.129 -    is_taut t orelse has_typed_var (!unwanted_types) t orelse
   1.130 +    is_taut t orelse has_typed_var unwanted_types t orelse
   1.131      forall too_general_equality (dest_disj t);
   1.132  
   1.133  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   1.134 @@ -909,8 +872,6 @@
   1.135                    Pretty.string_of (ProofContext.pretty_term ctxt
   1.136                      (Logic.mk_conjunction_list (Thm.prems_of goal))));
   1.137      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   1.138 -    inc hook_count;
   1.139 -    Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
   1.140      ResClause.init thy;
   1.141      ResHolClause.init thy;
   1.142      if !time_limit > 0 then isar_atp (ctxt, goal)
     2.1 --- a/src/HOL/Tools/res_atp_methods.ML	Fri Aug 10 14:49:01 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Fri Aug 10 15:13:18 2007 +0200
     2.3 @@ -17,22 +17,22 @@
     2.4  
     2.5  (* vampire, eprover and spass tactics *)
     2.6  
     2.7 -fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
     2.8 -fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
     2.9 -fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_time) st;
    2.10 +fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    2.11 +fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    2.12 +fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    2.13  
    2.14  
    2.15 -fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
    2.16 +fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    2.17  
    2.18 -fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
    2.19 +fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    2.20  
    2.21 -fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
    2.22 +fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    2.23  
    2.24 -fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
    2.25 +fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    2.26  
    2.27 -fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
    2.28 +fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    2.29  
    2.30 -fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) st;
    2.31 +fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    2.32  
    2.33  val ResAtps_setup =
    2.34    Method.add_methods 
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Aug 10 14:49:01 2007 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Aug 10 15:13:18 2007 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  
     3.5  signature RES_AXIOMS =
     3.6  sig
     3.7 -  val trace_abs: bool ref
     3.8    val cnf_axiom : string * thm -> thm list
     3.9    val cnf_name : string -> thm list
    3.10    val meta_cnf_axiom : thm -> thm list
    3.11 @@ -32,8 +31,6 @@
    3.12    because it is not performed by inference!!*)
    3.13  val abstract_lambdas = true;
    3.14  
    3.15 -val trace_abs = ref false;
    3.16 -
    3.17  (* FIXME legacy *)
    3.18  fun freeze_thm th = #1 (Drule.freeze_thaw th);
    3.19  
    3.20 @@ -230,8 +227,8 @@
    3.21  (*Does an existing abstraction definition have an RHS that matches the one we need now?
    3.22    thy is the current theory, which must extend that of theorem th.*)
    3.23  fun match_rhs thy t th =
    3.24 -  let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
    3.25 -                                          " against\n" ^ string_of_thm th) else ();
    3.26 +  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
    3.27 +                                   " against\n" ^ string_of_thm th);
    3.28        val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
    3.29        val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
    3.30        val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
    3.31 @@ -256,27 +253,27 @@
    3.32                  val _ = assert_eta_free ct;
    3.33                  val (cvs,cta) = dest_abs_list ct
    3.34                  val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
    3.35 -                val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
    3.36 +                val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
    3.37                  val (u'_th,defs) = abstract thy cta
    3.38 -                val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
    3.39 +                val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
    3.40                  val cu' = Thm.rhs_of u'_th
    3.41                  val u' = term_of cu'
    3.42                  val abs_v_u = lambda_list (map term_of cvs) u'
    3.43                  (*get the formal parameters: ALL variables free in the term*)
    3.44                  val args = term_frees abs_v_u
    3.45 -                val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
    3.46 +                val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
    3.47                  val rhs = list_abs_free (map dest_Free args, abs_v_u)
    3.48                        (*Forms a lambda-abstraction over the formal parameters*)
    3.49 -                val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
    3.50 +                val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
    3.51                  val thy = theory_of_thm u'_th
    3.52                  val (ax,ax',thy) =
    3.53                   case List.mapPartial (match_rhs thy abs_v_u) 
    3.54                           (Net.match_term (!abstraction_cache) u') of
    3.55                       (ax,ax')::_ => 
    3.56 -                       (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
    3.57 +                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
    3.58                          (ax,ax',thy))
    3.59                     | [] =>
    3.60 -                      let val _ = if !trace_abs then warning "Lookup was empty" else ();
    3.61 +                      let val _ = Output.debug (fn()=>"Lookup was empty");
    3.62                            val Ts = map type_of args
    3.63                            val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
    3.64                            val c = Const (Sign.full_name thy cname, cT)
    3.65 @@ -286,33 +283,29 @@
    3.66                            val cdef = cname ^ "_def"
    3.67                            val thy = Theory.add_defs_i false false
    3.68                                         [(cdef, equals cT $ c $ rhs)] thy
    3.69 -                          val _ = if !trace_abs then (warning ("Definition is " ^ 
    3.70 -                                                      string_of_thm (get_axiom thy cdef))) 
    3.71 -                                  else ();
    3.72 +                          val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
    3.73                            val ax = get_axiom thy cdef |> freeze_thm
    3.74                                       |> mk_object_eq |> strip_lambdas (length args)
    3.75                                       |> mk_meta_eq |> Meson.generalize
    3.76                            val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
    3.77 -                          val _ = if !trace_abs then 
    3.78 -                                    (warning ("Declaring: " ^ string_of_thm ax);
    3.79 -                                     warning ("Instance: " ^ string_of_thm ax')) 
    3.80 -                                  else ();
    3.81 +                          val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
    3.82 +                                                       "Instance: " ^ string_of_thm ax');
    3.83                            val _ = abstraction_cache := Net.insert_term eq_absdef 
    3.84                                              ((Logic.varify u'), ax) (!abstraction_cache)
    3.85                              handle Net.INSERT =>
    3.86                                raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
    3.87                         in  (ax,ax',thy)  end
    3.88 -            in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
    3.89 +            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
    3.90                 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
    3.91          | (t1$t2) =>
    3.92              let val (ct1,ct2) = Thm.dest_comb ct
    3.93                  val (th1,defs1) = abstract thy ct1
    3.94                  val (th2,defs2) = abstract (theory_of_thm th1) ct2
    3.95              in  (combination th1 th2, defs1@defs2)  end
    3.96 -      val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
    3.97 +      val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
    3.98        val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
    3.99        val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   3.100 -      val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   3.101 +      val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
   3.102    in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
   3.103  
   3.104  fun name_of def = try (#1 o dest_Free o lhs_of) def;
   3.105 @@ -349,7 +342,7 @@
   3.106                   case List.mapPartial (match_rhs thy abs_v_u) 
   3.107                          (Net.match_term (!abstraction_cache) u') of
   3.108                       (ax,ax')::_ => 
   3.109 -                       (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
   3.110 +                       (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   3.111                          (ax,ax'))
   3.112                     | [] =>
   3.113                        let val Ts = map type_of args
   3.114 @@ -365,17 +358,17 @@
   3.115                              handle Net.INSERT =>
   3.116                                raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   3.117                        in (ax,ax') end
   3.118 -            in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
   3.119 +            in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   3.120                 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   3.121          | (t1$t2) =>
   3.122              let val (ct1,ct2) = Thm.dest_comb ct
   3.123                  val (t1',defs1) = abstract ct1
   3.124                  val (t2',defs2) = abstract ct2
   3.125              in  (combination t1' t2', defs1@defs2)  end
   3.126 -      val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
   3.127 +      val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
   3.128        val (eqth,defs) = abstract (cprop_of th)
   3.129        val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   3.130 -      val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   3.131 +      val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
   3.132    in  map Drule.eta_contraction_rule ths  end;
   3.133  
   3.134  
   3.135 @@ -603,6 +596,9 @@
   3.136        is_Free t andalso not (member (op aconv) xs t)
   3.137    | is_okdef _ _ = false
   3.138  
   3.139 +(*This function tries to cope with open locales, which introduce hypotheses of the form
   3.140 +  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   3.141 +  of llabs_ and sko_ functions. *)
   3.142  fun expand_defs_tac st0 st =
   3.143    let val hyps0 = #hyps (rep_thm st0)
   3.144        val hyps = #hyps (crep_thm st)
     4.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Aug 10 14:49:01 2007 +0200
     4.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Aug 10 15:13:18 2007 +0200
     4.3 @@ -37,10 +37,6 @@
     4.4  fun partial_types () = (typ_level:=T_PARTIAL);
     4.5  fun const_types_only () = (typ_level:=T_CONST);
     4.6  
     4.7 -(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
     4.8 -  combinators appear to work best.*)
     4.9 -val use_Turner = ref false;
    4.10 -
    4.11  (*If true, each function will be directly applied to as many arguments as possible, avoiding
    4.12    use of the "apply" operator. Use of hBOOL is also minimized. It only works for the 
    4.13    constant-typed translation, though it could be tried for the partially-typed one.*)
    4.14 @@ -70,34 +66,7 @@
    4.15    | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    4.16    | is_free _ _ = false;
    4.17  
    4.18 -fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds =
    4.19 -      let val tp_p = Term.type_of1(bnds,p)
    4.20 -	  val tp_q = Term.type_of1(bnds,q)
    4.21 -	  val tp_r = Term.type_of1(bnds,r)
    4.22 -	  val typ_B' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    4.23 -      in
    4.24 -	  Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
    4.25 -      end
    4.26 -  | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
    4.27 -      let val tp_p = Term.type_of1(bnds,p)
    4.28 -	  val tp_q = Term.type_of1(bnds,q)
    4.29 -	  val tp_r = Term.type_of1(bnds,r)
    4.30 -	  val typ_C' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    4.31 -      in
    4.32 -	  Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
    4.33 -      end
    4.34 -  | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
    4.35 -      let val tp_p = Term.type_of1(bnds,p)
    4.36 -	  val tp_q = Term.type_of1(bnds,q)
    4.37 -	  val tp_r = Term.type_of1(bnds,r)
    4.38 -	  val typ_S' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    4.39 -      in
    4.40 -	  Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
    4.41 -      end
    4.42 -  | mk_compact_comb tm _ = tm;
    4.43 -
    4.44 -fun compact_comb t bnds = 
    4.45 -  if !use_Turner then mk_compact_comb t bnds else t;
    4.46 +fun compact_comb t bnds = t;
    4.47  
    4.48  fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) 
    4.49    | lam2comb (Abs(x,tp,Bound n)) bnds =