--- a/src/HOL/Tools/res_atp.ML Fri Aug 10 14:49:01 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Aug 10 15:13:18 2007 +0200
@@ -8,7 +8,6 @@
signature RES_ATP =
sig
val prover: string ref
- val custom_spass: string list ref
val destdir: string ref
val helper_path: string -> string -> string
val problem_name: string ref
@@ -18,22 +17,12 @@
datatype mode = Auto | Fol | Hol
val linkup_logic_mode : mode ref
val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
- val vampire_time: int ref
- val eprover_time: int ref
- val spass_time: int ref
- val run_vampire: int -> unit
- val run_eprover: int -> unit
- val run_spass: int -> unit
- val vampireLimit: unit -> int
- val eproverLimit: unit -> int
- val spassLimit: unit -> int
val atp_method: (Proof.context -> thm list -> int -> tactic) ->
Method.src -> Proof.context -> Proof.method
val cond_rm_tmp: string -> unit
val include_all: bool ref
val run_relevance_filter: bool ref
val run_blacklist_filter: bool ref
- val blacklist: string list ref
val add_all : unit -> unit
val add_claset : unit -> unit
val add_simpset : unit -> unit
@@ -61,8 +50,6 @@
(********************************************************************)
(*** background linkup ***)
-val call_atp = ref false;
-val hook_count = ref 0;
val time_limit = ref 60;
val prover = ref "";
@@ -84,8 +71,6 @@
val _ = set_prover "E"; (* use E as the default prover *)
-val custom_spass = (*specialized options for SPASS*)
- ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
val destdir = ref ""; (*Empty means write files to /tmp*)
val problem_name = ref "prob";
@@ -108,29 +93,6 @@
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
-
-(*** ATP methods ***)
-val vampire_time = ref 60;
-val eprover_time = ref 60;
-val spass_time = ref 60;
-
-fun run_vampire time =
- if (time >0) then vampire_time:= time
- else vampire_time:=60;
-
-fun run_eprover time =
- if (time > 0) then eprover_time:= time
- else eprover_time:=60;
-
-fun run_spass time =
- if (time > 0) then spass_time:=time
- else spass_time:=60;
-
-
-fun vampireLimit () = !vampire_time;
-fun eproverLimit () = !eprover_time;
-fun spassLimit () = !spass_time;
-
fun atp_input_file () =
let val file = !problem_name
in
@@ -294,8 +256,9 @@
(*** white list and black list of lemmas ***)
-(*The rule subsetI is frequently omitted by the relevance filter.*)
-val whitelist = ref [subsetI];
+(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
+ or identified with ATPset (which however is too big currently)*)
+val whitelist = [subsetI];
(*Names of theorems and theorem lists to be blacklisted.
@@ -303,7 +266,7 @@
membership literals) and relate to seldom-used facts. Some duplicate other rules.
FIXME: this blacklist needs to be maintained using theory data and added to using
an attribute.*)
-val blacklist = ref
+val blacklist =
["Datatype.prod.size",
"Divides.dvd_0_left_iff",
"Finite_Set.card_0_eq",
@@ -510,7 +473,7 @@
fun all_valid_thms ctxt =
let
- val banned_tab = foldl setinsert Symtab.empty (!blacklist)
+ val banned_tab = foldl setinsert Symtab.empty blacklist
fun blacklisted s = !run_blacklist_filter andalso
(isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
@@ -582,7 +545,7 @@
in claset_thms @ simpset_thms @ atpset_thms end
val user_rules = filter check_named
(map ResAxioms.pairname
- (if null user_thms then !whitelist else user_thms))
+ (if null user_thms then whitelist else user_thms))
in
(filter check_named included_thms, user_rules)
end;
@@ -681,10 +644,10 @@
they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
The resulting clause will have no type constraint, yielding false proofs. Even "bool"
leads to many unsound proofs, though (obviously) only for higher-order problems.*)
-val unwanted_types = ref ["Product_Type.unit","bool"];
+val unwanted_types = ["Product_Type.unit","bool"];
fun unwanted t =
- is_taut t orelse has_typed_var (!unwanted_types) t orelse
+ is_taut t orelse has_typed_var unwanted_types t orelse
forall too_general_equality (dest_disj t);
(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
@@ -909,8 +872,6 @@
Pretty.string_of (ProofContext.pretty_term ctxt
(Logic.mk_conjunction_list (Thm.prems_of goal))));
Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
- inc hook_count;
- Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
ResClause.init thy;
ResHolClause.init thy;
if !time_limit > 0 then isar_atp (ctxt, goal)
--- a/src/HOL/Tools/res_atp_methods.ML Fri Aug 10 14:49:01 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML Fri Aug 10 15:13:18 2007 +0200
@@ -17,22 +17,22 @@
(* vampire, eprover and spass tactics *)
-fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
-fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
-fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_time) st;
+fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
+fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
+fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
-fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
+fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
-fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
+fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
-fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
+fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
-fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
+fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
-fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
+fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
-fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) st;
+fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
val ResAtps_setup =
Method.add_methods
--- a/src/HOL/Tools/res_axioms.ML Fri Aug 10 14:49:01 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Aug 10 15:13:18 2007 +0200
@@ -7,7 +7,6 @@
signature RES_AXIOMS =
sig
- val trace_abs: bool ref
val cnf_axiom : string * thm -> thm list
val cnf_name : string -> thm list
val meta_cnf_axiom : thm -> thm list
@@ -32,8 +31,6 @@
because it is not performed by inference!!*)
val abstract_lambdas = true;
-val trace_abs = ref false;
-
(* FIXME legacy *)
fun freeze_thm th = #1 (Drule.freeze_thaw th);
@@ -230,8 +227,8 @@
(*Does an existing abstraction definition have an RHS that matches the one we need now?
thy is the current theory, which must extend that of theorem th.*)
fun match_rhs thy t th =
- let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
- " against\n" ^ string_of_thm th) else ();
+ let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
+ " against\n" ^ string_of_thm th);
val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
val ct_pairs = if subthy (theory_of_thm th, thy) andalso
@@ -256,27 +253,27 @@
val _ = assert_eta_free ct;
val (cvs,cta) = dest_abs_list ct
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
- val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
+ val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
val (u'_th,defs) = abstract thy cta
- val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
+ val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
val cu' = Thm.rhs_of u'_th
val u' = term_of cu'
val abs_v_u = lambda_list (map term_of cvs) u'
(*get the formal parameters: ALL variables free in the term*)
val args = term_frees abs_v_u
- val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
+ val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
val rhs = list_abs_free (map dest_Free args, abs_v_u)
(*Forms a lambda-abstraction over the formal parameters*)
- val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
+ val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
val thy = theory_of_thm u'_th
val (ax,ax',thy) =
case List.mapPartial (match_rhs thy abs_v_u)
(Net.match_term (!abstraction_cache) u') of
(ax,ax')::_ =>
- (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
+ (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
(ax,ax',thy))
| [] =>
- let val _ = if !trace_abs then warning "Lookup was empty" else ();
+ let val _ = Output.debug (fn()=>"Lookup was empty");
val Ts = map type_of args
val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
val c = Const (Sign.full_name thy cname, cT)
@@ -286,33 +283,29 @@
val cdef = cname ^ "_def"
val thy = Theory.add_defs_i false false
[(cdef, equals cT $ c $ rhs)] thy
- val _ = if !trace_abs then (warning ("Definition is " ^
- string_of_thm (get_axiom thy cdef)))
- else ();
+ val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
val ax = get_axiom thy cdef |> freeze_thm
|> mk_object_eq |> strip_lambdas (length args)
|> mk_meta_eq |> Meson.generalize
val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
- val _ = if !trace_abs then
- (warning ("Declaring: " ^ string_of_thm ax);
- warning ("Instance: " ^ string_of_thm ax'))
- else ();
+ val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
+ "Instance: " ^ string_of_thm ax');
val _ = abstraction_cache := Net.insert_term eq_absdef
((Logic.varify u'), ax) (!abstraction_cache)
handle Net.INSERT =>
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
in (ax,ax',thy) end
- in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
+ in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
| (t1$t2) =>
let val (ct1,ct2) = Thm.dest_comb ct
val (th1,defs1) = abstract thy ct1
val (th2,defs2) = abstract (theory_of_thm th1) ct2
in (combination th1 th2, defs1@defs2) end
- val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
+ val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
- val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
+ val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end;
fun name_of def = try (#1 o dest_Free o lhs_of) def;
@@ -349,7 +342,7 @@
case List.mapPartial (match_rhs thy abs_v_u)
(Net.match_term (!abstraction_cache) u') of
(ax,ax')::_ =>
- (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
+ (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
(ax,ax'))
| [] =>
let val Ts = map type_of args
@@ -365,17 +358,17 @@
handle Net.INSERT =>
raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
in (ax,ax') end
- in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
+ in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
| (t1$t2) =>
let val (ct1,ct2) = Thm.dest_comb ct
val (t1',defs1) = abstract ct1
val (t2',defs2) = abstract ct2
in (combination t1' t2', defs1@defs2) end
- val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
+ val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
val (eqth,defs) = abstract (cprop_of th)
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
- val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
+ val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
in map Drule.eta_contraction_rule ths end;
@@ -603,6 +596,9 @@
is_Free t andalso not (member (op aconv) xs t)
| is_okdef _ _ = false
+(*This function tries to cope with open locales, which introduce hypotheses of the form
+ Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
+ of llabs_ and sko_ functions. *)
fun expand_defs_tac st0 st =
let val hyps0 = #hyps (rep_thm st0)
val hyps = #hyps (crep_thm st)
--- a/src/HOL/Tools/res_hol_clause.ML Fri Aug 10 14:49:01 2007 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Fri Aug 10 15:13:18 2007 +0200
@@ -37,10 +37,6 @@
fun partial_types () = (typ_level:=T_PARTIAL);
fun const_types_only () = (typ_level:=T_CONST);
-(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
- combinators appear to work best.*)
-val use_Turner = ref false;
-
(*If true, each function will be directly applied to as many arguments as possible, avoiding
use of the "apply" operator. Use of hBOOL is also minimized. It only works for the
constant-typed translation, though it could be tried for the partially-typed one.*)
@@ -70,34 +66,7 @@
| is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
| is_free _ _ = false;
-fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds =
- let val tp_p = Term.type_of1(bnds,p)
- val tp_q = Term.type_of1(bnds,q)
- val tp_r = Term.type_of1(bnds,r)
- val typ_B' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
- in
- Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
- end
- | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
- let val tp_p = Term.type_of1(bnds,p)
- val tp_q = Term.type_of1(bnds,q)
- val tp_r = Term.type_of1(bnds,r)
- val typ_C' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
- in
- Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
- end
- | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
- let val tp_p = Term.type_of1(bnds,p)
- val tp_q = Term.type_of1(bnds,q)
- val tp_r = Term.type_of1(bnds,r)
- val typ_S' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
- in
- Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
- end
- | mk_compact_comb tm _ = tm;
-
-fun compact_comb t bnds =
- if !use_Turner then mk_compact_comb t bnds else t;
+fun compact_comb t bnds = t;
fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp)
| lam2comb (Abs(x,tp,Bound n)) bnds =