# HG changeset patch # User paulson # Date 1186751598 -7200 # Node ID 5458fbf18276366fc2ec8648fab222453eacba7e # Parent 0482ecc4ef11cecb8906e4cdc7f49b8de5cca968 removal of some refs diff -r 0482ecc4ef11 -r 5458fbf18276 src/HOL/Tools/res_atp.ML --- 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) diff -r 0482ecc4ef11 -r 5458fbf18276 src/HOL/Tools/res_atp_methods.ML --- 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 diff -r 0482ecc4ef11 -r 5458fbf18276 src/HOL/Tools/res_axioms.ML --- 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) diff -r 0482ecc4ef11 -r 5458fbf18276 src/HOL/Tools/res_hol_clause.ML --- 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 =