# HG changeset patch # User blanchet # Date 1269000138 -3600 # Node ID 2f8fb5242799288365f4f576a0933a050d4e534d # Parent 23908b4dbc2fbd70f4cf1640a4a1dda83661a7ae more Sledgehammer refactoring diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Mar 19 13:02:18 2010 +0100 @@ -314,6 +314,7 @@ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ + Tools/Sledgehammer/meson_tactic.ML \ Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer_fact_filter.ML \ Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \ diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 13:02:18 2010 +0100 @@ -1,7 +1,8 @@ (* Title: HOL/Sledgehammer.thy Author: Lawrence C Paulson Author: Jia Meng, NICTA - Author: Fabian Immler, TUM + Author: Fabian Immler, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen *) header {* Sledgehammer: Isabelle--ATP Linkup *} @@ -10,7 +11,8 @@ imports Plain Hilbert_Choice uses "Tools/polyhash.ML" - "Tools/Sledgehammer/sledgehammer_fol_clause.ML" + "~~/src/Tools/Metis/metis.ML" + ("Tools/Sledgehammer/sledgehammer_fol_clause.ML") ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML") ("Tools/Sledgehammer/sledgehammer_hol_clause.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") @@ -18,79 +20,79 @@ ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_wrapper.ML") ("Tools/ATP_Manager/atp_minimal.ML") - "~~/src/Tools/Metis/metis.ML" + ("Tools/Sledgehammer/meson_tactic.ML") ("Tools/Sledgehammer/metis_tactics.ML") begin -definition COMBI :: "'a => 'a" - where "COMBI P == P" +definition COMBI :: "'a \ 'a" + where "COMBI P \ P" -definition COMBK :: "'a => 'b => 'a" - where "COMBK P Q == P" +definition COMBK :: "'a \ 'b \ 'a" + where "COMBK P Q \ P" -definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" - where "COMBB P Q R == P (Q R)" +definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" + where "COMBB P Q R \ P (Q R)" -definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" - where "COMBC P Q R == P R Q" +definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" + where "COMBC P Q R \ P R Q" -definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" - where "COMBS P Q R == P R (Q R)" +definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" + where "COMBS P Q R \ P R (Q R)" -definition fequal :: "'a => 'a => bool" - where "fequal X Y == (X=Y)" +definition fequal :: "'a \ 'a \ bool" + where "fequal X Y \ (X = Y)" -lemma fequal_imp_equal: "fequal X Y ==> X=Y" +lemma fequal_imp_equal: "fequal X Y \ X = Y" by (simp add: fequal_def) -lemma equal_imp_fequal: "X=Y ==> fequal X Y" +lemma equal_imp_fequal: "X = Y \ fequal X Y" by (simp add: fequal_def) text{*These two represent the equivalence between Boolean equality and iff. They can't be converted to clauses automatically, as the iff would be expanded...*} -lemma iff_positive: "P | Q | P=Q" +lemma iff_positive: "P \ Q \ P = Q" by blast -lemma iff_negative: "~P | ~Q | P=Q" +lemma iff_negative: "\ P \ \ Q \ P = Q" by blast text{*Theorems for translation to combinators*} -lemma abs_S: "(%x. (f x) (g x)) == COMBS f g" +lemma abs_S: "\x. (f x) (g x) \ COMBS f g" apply (rule eq_reflection) apply (rule ext) apply (simp add: COMBS_def) done -lemma abs_I: "(%x. x) == COMBI" +lemma abs_I: "\x. x \ COMBI" apply (rule eq_reflection) apply (rule ext) apply (simp add: COMBI_def) done -lemma abs_K: "(%x. y) == COMBK y" +lemma abs_K: "\x. y \ COMBK y" apply (rule eq_reflection) apply (rule ext) apply (simp add: COMBK_def) done -lemma abs_B: "(%x. a (g x)) == COMBB a g" +lemma abs_B: "\x. a (g x) \ COMBB a g" apply (rule eq_reflection) apply (rule ext) apply (simp add: COMBB_def) done -lemma abs_C: "(%x. (f x) b) == COMBC f b" +lemma abs_C: "\x. (f x) b \ COMBC f b" apply (rule eq_reflection) apply (rule ext) apply (simp add: COMBC_def) done - subsection {* Setup of external ATPs *} +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML" use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML" setup Sledgehammer_Fact_Preprocessor.setup use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" @@ -119,7 +121,12 @@ setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} - + + +subsection {* The MESON prover *} + +use "Tools/Sledgehammer/meson_tactic.ML" +setup Meson_Tactic.setup subsection {* The Metis prover *} diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 13:02:18 2010 +0100 @@ -20,7 +20,7 @@ val sledgehammer: string list -> Proof.state -> unit end; -structure ATP_Manager: ATP_MANAGER = +structure ATP_Manager : ATP_MANAGER = struct (** preferences **) @@ -263,7 +263,7 @@ val _ = register birth_time death_time (Thread.self (), desc); val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal)); val message = #message (prover (! timeout) problem) - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *) + handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *) "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis" | ERROR msg => ("Error: " ^ msg); val _ = unregister message (Thread.self ()); diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100 @@ -14,7 +14,7 @@ (string * thm list) list -> ((string * thm list) list * int) option * string end -structure ATP_Minimal: ATP_MINIMAL = +structure ATP_Minimal : ATP_MINIMAL = struct (* Linear minimization *) @@ -170,7 +170,7 @@ (NONE, "Error in prover: " ^ msg) | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => + handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => (NONE, "Error: " ^ msg) end diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 13:02:18 2010 +0100 @@ -16,6 +16,7 @@ type prover_config = {command: Path.T, arguments: int -> string, + failure_strs: string list, max_new_clauses: int, insert_theory_const: bool, emit_structured_proof: bool} @@ -49,11 +50,12 @@ val refresh_systems: unit -> unit end; -structure ATP_Wrapper: ATP_WRAPPER = +structure ATP_Wrapper : ATP_WRAPPER = struct -structure SFF = Sledgehammer_Fact_Filter -structure SPR = Sledgehammer_Proof_Reconstruct +open Sledgehammer_HOL_Clause +open Sledgehammer_Fact_Filter +open Sledgehammer_Proof_Reconstruct (** generic ATP wrapper **) @@ -76,6 +78,7 @@ type prover_config = {command: Path.T, arguments: int -> string, + failure_strs: string list, max_new_clauses: int, insert_theory_const: bool, emit_structured_proof: bool}; @@ -114,13 +117,20 @@ |> Exn.release |> tap (after path); -fun external_prover relevance_filter prepare write cmd args produce_answer name - ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) = +fun find_failure strs proof = + case filter (fn s => String.isSubstring s proof) strs of + [] => if is_proof_well_formed proof then NONE + else SOME "Ill-formed ATP output" + | (failure :: _) => SOME failure + +fun external_prover relevance_filter prepare write cmd args failure_strs + produce_answer name ({with_full_types, subgoal, goal, axiom_clauses, + filtered_clauses}: problem) = let (* get clauses and prepare them for writing *) val (ctxt, (chain_ths, th)) = goal; val thy = ProofContext.theory_of ctxt; - val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths; + val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal); val the_filtered_clauses = (case filtered_clauses of @@ -184,7 +194,7 @@ with_path cleanup export run_on (prob_pathname subgoal); (* check for success and print out some information on failure *) - val failure = SPR.find_failure proof; + val failure = find_failure failure_strs proof; val success = rc = 0 andalso is_none failure; val (message, real_thm_names) = if is_some failure then ("External prover failed.", []) @@ -200,25 +210,16 @@ (* generic TPTP-based provers *) -fun gen_tptp_prover (name, prover_config) timeout problem = - let - val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} = - prover_config; - in - external_prover - (SFF.get_relevant max_new_clauses insert_theory_const) - (SFF.prepare_clauses false) - Sledgehammer_HOL_Clause.tptp_write_file - command - (arguments timeout) - (if emit_structured_proof then SPR.structured_proof - else SPR.lemma_list false) - name - problem - end; +fun generic_tptp_prover + (name, {command, arguments, failure_strs, max_new_clauses, + insert_theory_const, emit_structured_proof}) timeout = + external_prover (get_relevant_facts max_new_clauses insert_theory_const) + (prepare_clauses false) write_tptp_file command (arguments timeout) + failure_strs + (if emit_structured_proof then structured_isar_proof + else metis_lemma_list false) name; -fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config)); - +fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p)); (** common provers **) @@ -227,6 +228,8 @@ (*NB: Vampire does not work without explicit timelimit*) +val vampire_failure_strs = + ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; val vampire_max_new_clauses = 60; val vampire_insert_theory_const = false; @@ -234,6 +237,7 @@ {command = Path.explode "$VAMPIRE_HOME/vampire", arguments = (fn timeout => "--output_syntax tptp --mode casc" ^ " -t " ^ string_of_int timeout), + failure_strs = vampire_failure_strs, max_new_clauses = vampire_max_new_clauses, insert_theory_const = vampire_insert_theory_const, emit_structured_proof = full}; @@ -244,6 +248,10 @@ (* E prover *) +val eprover_failure_strs = + ["SZS status: Satisfiable", "SZS status Satisfiable", + "SZS status: ResourceOut", "SZS status ResourceOut", + "# Cannot determine problem status"]; val eprover_max_new_clauses = 100; val eprover_insert_theory_const = false; @@ -251,6 +259,7 @@ {command = Path.explode "$E_HOME/eproof", arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^ " --silent --cpu-limit=" ^ string_of_int timeout), + failure_strs = eprover_failure_strs, max_new_clauses = eprover_max_new_clauses, insert_theory_const = eprover_insert_theory_const, emit_structured_proof = full}; @@ -261,6 +270,9 @@ (* SPASS *) +val spass_failure_strs = + ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", + "SPASS beiseite: Maximal number of loops exceeded."]; val spass_max_new_clauses = 40; val spass_insert_theory_const = true; @@ -268,26 +280,25 @@ {command = Path.explode "$SPASS_HOME/SPASS", arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout), + failure_strs = spass_failure_strs, max_new_clauses = spass_max_new_clauses, insert_theory_const = insert_theory_const, emit_structured_proof = false}; -fun gen_dfg_prover (name, prover_config: prover_config) timeout problem = - let - val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config; - in - external_prover - (SFF.get_relevant max_new_clauses insert_theory_const) - (SFF.prepare_clauses true) - Sledgehammer_HOL_Clause.dfg_write_file - command - (arguments timeout) - (SPR.lemma_list true) - name - problem - end; +fun generic_dfg_prover + (name, ({command, arguments, failure_strs, max_new_clauses, + insert_theory_const, ...} : prover_config)) timeout = + external_prover + (get_relevant_facts max_new_clauses insert_theory_const) + (prepare_clauses true) + write_dfg_file + command + (arguments timeout) + failure_strs + (metis_lemma_list true) + name; -fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config)); +fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); val spass = dfg_prover ("spass", spass_config spass_insert_theory_const); val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false); @@ -316,10 +327,13 @@ NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") | SOME sys => sys); +val remote_failure_strs = ["Remote-script could not extract proof"]; + fun remote_prover_config prover_prefix args max_new insert_tc: prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", - arguments = - (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix), + arguments = (fn timeout => + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix), + failure_strs = remote_failure_strs, max_new_clauses = max_new, insert_theory_const = insert_tc, emit_structured_proof = false}; diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/meson_tactic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Fri Mar 19 13:02:18 2010 +0100 @@ -0,0 +1,53 @@ +(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML + Author: Jia Meng, Cambridge University Computer Laboratory + +MESON general tactic and proof method. +*) + +signature MESON_TACTIC = +sig + val expand_defs_tac : thm -> tactic + val meson_general_tac : Proof.context -> thm list -> int -> tactic + val setup: theory -> theory +end; + +structure Meson_Tactic : MESON_TACTIC = +struct + +open Sledgehammer_Fact_Preprocessor + +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*) +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) = + String.isPrefix skolem_prefix a + | is_absko _ = false; + +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*) + 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 sko_ functions. *) +fun expand_defs_tac st0 st = + let val hyps0 = #hyps (rep_thm st0) + val hyps = #hyps (crep_thm st) + val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps + val defs = filter (is_absko o Thm.term_of) newhyps + val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) + (map Thm.term_of hyps) + val fixed = OldTerm.term_frees (concl_of st) @ + fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) [] + in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; + +fun meson_general_tac ctxt ths i st0 = + let + val thy = ProofContext.theory_of ctxt + val ctxt0 = Classical.put_claset HOL_cs ctxt + in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end; + +val setup = + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) + "MESON resolution proof procedure"; + +end; diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 13:02:18 2010 +0100 @@ -18,9 +18,11 @@ structure Metis_Tactics : METIS_TACTICS = struct -structure SFC = Sledgehammer_FOL_Clause -structure SHC = Sledgehammer_HOL_Clause -structure SPR = Sledgehammer_Proof_Reconstruct +open Sledgehammer_FOL_Clause +open Sledgehammer_Fact_Preprocessor +open Sledgehammer_HOL_Clause +open Sledgehammer_Proof_Reconstruct +open Sledgehammer_Fact_Filter val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); @@ -67,62 +69,62 @@ fun metis_lit b c args = (b, (c, args)); -fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x - | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[]) - | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); +fun hol_type_to_fol (AtomV x) = Metis.Term.Var x + | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, []) + | hol_type_to_fol (Comp (tc, tps)) = + Metis.Term.Fn (tc, map hol_type_to_fol tps); (*These two functions insert type literals before the real literals. That is the opposite order from TPTP linkup, but maybe OK.*) fun hol_term_to_fol_FO tm = - case SHC.strip_comb tm of - (SHC.CombConst(c,_,tys), tms) => + case strip_combterm_comb tm of + (CombConst(c,_,tys), tms) => let val tyargs = map hol_type_to_fol tys val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end - | (SHC.CombVar(v,_), []) => Metis.Term.Var v + | (CombVar(v,_), []) => Metis.Term.Var v | _ => error "hol_term_to_fol_FO"; -fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a - | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) = +fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a + | hol_term_to_fol_HO (CombConst (a, _, tylist)) = Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) - | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) = + | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); -fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) = - wrap_type (Metis.Term.Var a, ty) - | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) = +fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty) + | hol_term_to_fol_FT (CombConst(a, ty, _)) = wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) - | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) = + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - SHC.type_of_combterm tm); + type_of_combterm tm); -fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) = - let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm +fun hol_literal_to_fol FO (Literal (pol, tm)) = + let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm val tylits = if p = "equal" then [] else map hol_type_to_fol tys val lits = map hol_term_to_fol_FO tms in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end - | hol_literal_to_fol HO (SHC.Literal (pol, tm)) = - (case SHC.strip_comb tm of - (SHC.CombConst("equal",_,_), tms) => + | hol_literal_to_fol HO (Literal (pol, tm)) = + (case strip_combterm_comb tm of + (CombConst("equal",_,_), tms) => metis_lit pol "=" (map hol_term_to_fol_HO tms) | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) - | hol_literal_to_fol FT (SHC.Literal (pol, tm)) = - (case SHC.strip_comb tm of - (SHC.CombConst("equal",_,_), tms) => + | hol_literal_to_fol FT (Literal (pol, tm)) = + (case strip_combterm_comb tm of + (CombConst("equal",_,_), tms) => metis_lit pol "=" (map hol_term_to_fol_FT tms) | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); fun literals_of_hol_thm thy mode t = - let val (lits, types_sorts) = SHC.literals_of_term thy t + let val (lits, types_sorts) = literals_of_term thy t in (map (hol_literal_to_fol mode) lits, types_sorts) end; (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) -fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] - | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; +fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] + | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; fun default_sort _ (TVar _) = false | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); @@ -136,10 +138,9 @@ (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th in if is_conjecture then - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts) + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts) else - let val tylits = SFC.add_typs - (filter (not o default_sort ctxt) types_sorts) + let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts) val mtylits = if Config.get ctxt type_lits then map (metis_of_typeLit false) tylits else [] in @@ -149,13 +150,13 @@ (* ARITY CLAUSE *) -fun m_arity_cls (SFC.TConsLit (c,t,args)) = - metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] - | m_arity_cls (SFC.TVarLit (c,str)) = - metis_lit false (SFC.make_type_class c) [Metis.Term.Var str]; +fun m_arity_cls (TConsLit (c,t,args)) = + metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] + | m_arity_cls (TVarLit (c,str)) = + metis_lit false (make_type_class c) [Metis.Term.Var str]; (*TrueI is returned as the Isabelle counterpart because there isn't any.*) -fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) = +fun arity_cls (ArityClause {conclLit, premLits, ...}) = (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); @@ -164,7 +165,7 @@ fun m_classrel_cls subclass superclass = [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; -fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) = +fun classrel_cls (ClassrelClause {subclass, superclass, ...}) = (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); (* ------------------------------------------------------------------------- *) @@ -213,14 +214,14 @@ | strip_happ args x = (x, args); fun fol_type_to_isa _ (Metis.Term.Var v) = - (case SPR.strip_prefix SFC.tvar_prefix v of - SOME w => SPR.make_tvar w - | NONE => SPR.make_tvar v) + (case strip_prefix tvar_prefix v of + SOME w => make_tvar w + | NONE => make_tvar v) | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = - (case SPR.strip_prefix SFC.tconst_prefix x of - SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys) + (case strip_prefix tconst_prefix x of + SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys) | NONE => - case SPR.strip_prefix SFC.tfree_prefix x of + case strip_prefix tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => error ("fol_type_to_isa: " ^ x)); @@ -229,10 +230,10 @@ let val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case SPR.strip_prefix SFC.tvar_prefix v of - SOME w => Type (SPR.make_tvar w) + (case strip_prefix tvar_prefix v of + SOME w => Type (make_tvar w) | NONE => - case SPR.strip_prefix SFC.schematic_var_prefix v of + case strip_prefix schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -247,16 +248,16 @@ end | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) and applic_to_tt ("=",ts) = - Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) + Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case SPR.strip_prefix SFC.const_prefix a of + case strip_prefix const_prefix a of SOME b => - let val c = SPR.invert_const b - val ntypes = SPR.num_typargs thy c + let val c = invert_const b + val ntypes = num_typargs thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = SPR.num_typargs thy c + val ntyargs = num_typargs thy c in if length tys = ntyargs then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ @@ -267,14 +268,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case SPR.strip_prefix SFC.tconst_prefix a of + case strip_prefix tconst_prefix a of SOME b => - Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts))) + Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case SPR.strip_prefix SFC.tfree_prefix a of + case strip_prefix tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case SPR.strip_prefix SFC.fixed_var_prefix a of + case strip_prefix fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -285,16 +286,16 @@ fun fol_term_to_hol_FT ctxt fol_tm = let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case SPR.strip_prefix SFC.schematic_var_prefix v of + (case strip_prefix schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case SPR.strip_prefix SFC.const_prefix x of - SOME c => Const (SPR.invert_const c, dummyT) + (case strip_prefix const_prefix x of + SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case SPR.strip_prefix SFC.fixed_var_prefix x of + case strip_prefix fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -303,12 +304,12 @@ cvt tm1 $ cvt tm2 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = - list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case SPR.strip_prefix SFC.const_prefix x of - SOME c => Const (SPR.invert_const c, dummyT) + (case strip_prefix const_prefix x of + SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case SPR.strip_prefix SFC.fixed_var_prefix x of + case strip_prefix fixed_var_prefix x of SOME v => Free (v, dummyT) | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) @@ -331,7 +332,7 @@ ts' in ts' end; -fun mk_not (Const ("Not", _) $ b) = b +fun mk_not (Const (@{const_name Not}, _) $ b) = b | mk_not b = HOLogic.mk_not b; val metis_eq = Metis.Term.Fn ("=", []); @@ -387,9 +388,9 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case SPR.strip_prefix SFC.schematic_var_prefix a of + case strip_prefix schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case SPR.strip_prefix SFC.tvar_prefix a of + | NONE => case strip_prefix tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) @@ -455,8 +456,8 @@ val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end; -fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0) +fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*) + | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0) | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) @@ -469,7 +470,7 @@ | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls fun path_finder_FO tm [] = (tm, Term.Bound 0) | path_finder_FO tm (p::ps) = - let val (tm1,args) = Term.strip_comb tm + let val (tm1,args) = strip_comb tm val adjustment = get_ty_arg_size thy tm1 val p' = if adjustment > p then p else p-adjustment val tm_p = List.nth(args,p') @@ -496,13 +497,13 @@ " isa-term: " ^ Syntax.string_of_term ctxt tm ^ " fol-term: " ^ Metis.Term.toString t) fun path_finder FO tm ps _ = path_finder_FO tm ps - | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ = + | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = (*equality: not curried, as other predicates are*) if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) else path_finder_HO tm (p::ps) (*1 selects second operand*) | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) - | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) + | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps) (Metis.Term.Fn ("=", [t1,t2])) = (*equality: not curried, as other predicates are*) if p=0 then path_finder_FT tm (0::1::ps) @@ -514,7 +515,7 @@ | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 (*if not equality, ignore head to skip the hBOOL predicate*) | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm in (tm, nt $ tm_rslt) end | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm @@ -542,7 +543,7 @@ | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = equality_inf ctxt mode f_lit f_p f_r; -fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c); +fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); fun translate _ _ thpairs [] = thpairs | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = @@ -568,23 +569,14 @@ (* Translation of HO Clauses *) (* ------------------------------------------------------------------------- *) -fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th); - -val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; -val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal}; - -val comb_I = cnf_th @{theory} SHC.comb_I; -val comb_K = cnf_th @{theory} SHC.comb_K; -val comb_B = cnf_th @{theory} SHC.comb_B; -val comb_C = cnf_th @{theory} SHC.comb_C; -val comb_S = cnf_th @{theory} SHC.comb_S; +fun cnf_th thy th = hd (cnf_axiom thy th); fun type_ext thy tms = - let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms - val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms - and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms - val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers - val classrel_clauses = SFC.make_classrel_clauses thy subs supers' + let val subs = tfree_classes_of_terms tms + val supers = tvar_classes_of_terms tms + and tycons = type_consts_of_terms thy tms + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val classrel_clauses = make_classrel_clauses thy subs supers' in map classrel_cls classrel_clauses @ map arity_cls arity_clauses end; @@ -593,8 +585,8 @@ (* ------------------------------------------------------------------------- *) type logic_map = - {axioms : (Metis.Thm.thm * thm) list, - tfrees : SFC.type_literal list}; + {axioms: (Metis.Thm.thm * thm) list, + tfrees: type_literal list}; fun const_in_metis c (pred, tm_list) = let @@ -606,7 +598,7 @@ (*Extract TFree constraints from context to include as conjecture clauses*) fun init_tfrees ctxt = let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts - in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; + in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; (*transform isabelle type / arity clause to metis clause *) fun add_type_thm [] lmap = lmap @@ -643,12 +635,12 @@ val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists (*Now check for the existence of certain combinators*) - val thI = if used "c_COMBI" then [comb_I] else [] - val thK = if used "c_COMBK" then [comb_K] else [] - val thB = if used "c_COMBB" then [comb_B] else [] - val thC = if used "c_COMBC" then [comb_C] else [] - val thS = if used "c_COMBS" then [comb_S] else [] - val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] + val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else [] + val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else [] + val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else [] + val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else [] + val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else [] + val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else [] val lmap' = if mode=FO then lmap else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap in @@ -668,7 +660,7 @@ fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt val th_cls_pairs = - map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0 + map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0 val ths = maps #2 th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls @@ -677,7 +669,7 @@ val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); - app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees) + app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees) val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms @@ -719,12 +711,12 @@ let val _ = trace_msg (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in - if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0) + if exists_type type_has_topsort (prop_of st0) then raise METIS "Metis: Proof state contains the universal sort {}" else - (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify + (Meson.MESON neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i - THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0 + THEN Meson_Tactic.expand_defs_tac st0) st0 end handle METIS s => (warning ("Metis: " ^ s); Seq.empty); @@ -737,11 +729,11 @@ val setup = type_lits_setup #> - method @{binding metis} HO "METIS for FOL & HOL problems" #> + method @{binding metis} HO "METIS for FOL and HOL problems" #> method @{binding metisF} FO "METIS for FOL problems" #> method @{binding metisFT} FT "METIS with fully-typed translation" #> Method.setup @{binding finish_clausify} - (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl)))) + (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl)))) "cleanup after conversion to clauses"; end; diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 13:02:18 2010 +0100 @@ -4,47 +4,45 @@ signature SLEDGEHAMMER_FACT_FILTER = sig - type classrelClause = Sledgehammer_FOL_Clause.classrelClause - type arityClause = Sledgehammer_FOL_Clause.arityClause + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause + type arity_clause = Sledgehammer_FOL_Clause.arity_clause type axiom_name = Sledgehammer_HOL_Clause.axiom_name - type clause = Sledgehammer_HOL_Clause.clause - type clause_id = Sledgehammer_HOL_Clause.clause_id - datatype mode = Auto | Fol | Hol + type hol_clause = Sledgehammer_HOL_Clause.hol_clause + type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> + val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : bool -> thm list -> thm list -> - (thm * (axiom_name * clause_id)) list -> - (thm * (axiom_name * clause_id)) list -> theory -> + (thm * (axiom_name * hol_clause_id)) list -> + (thm * (axiom_name * hol_clause_id)) list -> theory -> axiom_name vector * - (clause list * clause list * clause list * - clause list * classrelClause list * arityClause list) + (hol_clause list * hol_clause list * hol_clause list * + hol_clause list * classrel_clause list * arity_clause list) end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = struct -structure SFC = Sledgehammer_FOL_Clause -structure SFP = Sledgehammer_Fact_Preprocessor -structure SHC = Sledgehammer_HOL_Clause +open Sledgehammer_FOL_Clause +open Sledgehammer_Fact_Preprocessor +open Sledgehammer_HOL_Clause -type classrelClause = SFC.classrelClause -type arityClause = SFC.arityClause -type axiom_name = SHC.axiom_name -type clause = SHC.clause -type clause_id = SHC.clause_id +type axiom_name = axiom_name +type hol_clause = hol_clause +type hol_clause_id = hol_clause_id (********************************************************************) (* some settings for both background automatic ATP calling procedure*) (* and also explicit ATP invocation methods *) (********************************************************************) -(*Translation mode can be auto-detected, or forced to be first-order or higher-order*) +(* Translation mode can be auto-detected, or forced to be first-order or + higher-order *) datatype mode = Auto | Fol | Hol; -val linkup_logic_mode = Auto; +val translation_mode = Auto; (*** background linkup ***) val run_blacklist_filter = true; @@ -59,7 +57,7 @@ (* Relevance Filtering *) (***************************************************************) -fun strip_Trueprop (Const("Trueprop",_) $ t) = t +fun strip_Trueprop (@{const Trueprop} $ t) = t | strip_Trueprop t = t; (*A surprising number of theorems contain only a few significant constants. @@ -79,7 +77,10 @@ being chosen, but for some reason filtering works better with them listed. The logical signs All, Ex, &, and --> are omitted because any remaining occurrrences must be within comprehensions.*) -val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="]; +val standard_consts = + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, + @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, + @{const_name "op ="}]; (*** constants with types ***) @@ -233,7 +234,7 @@ end handle ConstFree => false in - case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => + case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) => defs lhs rhs | _ => false end; @@ -252,10 +253,10 @@ let val cls = sort compare_pairs newpairs val accepted = List.take (cls, max_new) in - SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ + trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ ", exceeds the limit of " ^ Int.toString (max_new))); - SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); - SFP.trace_msg (fn () => "Actually passed: " ^ + trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); + trace_msg (fn () => "Actually passed: " ^ space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); (map #1 accepted, map #1 (List.drop (cls, max_new))) @@ -270,7 +271,7 @@ val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts val newp = p + (1.0-p) / convergence in - SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); + trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); (map #1 newrels) @ (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) end @@ -278,12 +279,12 @@ let val weight = clause_weight ctab rel_consts consts_typs in if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) - then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ + then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight)); relevant ((ax,weight)::newrels, rejects) axs) else relevant (newrels, ax::rejects) axs end - in SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); + in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); relevant ([],[]) end; @@ -292,12 +293,12 @@ then let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals - val _ = SFP.trace_msg (fn () => ("Initial constants: " ^ + val _ = trace_msg (fn () => ("Initial constants: " ^ space_implode ", " (Symtab.keys goal_const_tab))); val rels = relevant_clauses max_new thy const_tab (pass_mark) goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms) in - SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels))); + trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels))); rels end else axioms; @@ -332,7 +333,7 @@ | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) +fun hash_literal (@{const Not} $ P) = Word.notb(hashw_term(P,0w0)) | hash_literal P = hashw_term(P,0w0); fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t)))); @@ -351,7 +352,7 @@ fun make_unique xs = let val ht = mk_clause_table 7000 in - SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); + trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht end; @@ -383,7 +384,7 @@ val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; - val ths = filter_out SFP.bad_for_atp ths0; + val ths = filter_out bad_for_atp ths0; in if Facts.is_concealed facts name orelse null ths orelse run_blacklist_filter andalso is_package_def name then I @@ -403,7 +404,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names (a, ths) pairs = - if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs + if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs else add_single_names (a, ths) pairs; fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; @@ -412,12 +413,17 @@ fun name_thm_pairs ctxt = let val (mults, singles) = List.partition is_multi (all_valid_thms ctxt) - val blacklist = - if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else [] - fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th) + val ps = [] |> fold add_multi_names mults + |> fold add_single_names singles in - filter_out is_blacklisted - (fold add_single_names singles (fold add_multi_names mults [])) + if run_blacklist_filter then + let + val blacklist = No_ATPs.get ctxt + |> map (`Thm.full_prop_of) |> Termtab.make + val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd + in ps |> filter_out is_blacklisted end + else + ps end; fun check_named ("", th) = @@ -426,7 +432,7 @@ fun get_all_lemmas ctxt = let val included_thms = - tap (fn ths => SFP.trace_msg + tap (fn ths => trace_msg (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) (name_thm_pairs ctxt) in @@ -440,7 +446,7 @@ fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts); (*Remove this trivial type class*) -fun delete_type cset = Symtab.delete_safe "HOL.type" cset; +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; fun tvar_classes_of_terms ts = let val sorts_list = map (map #2 o OldTerm.term_tvars) ts @@ -499,14 +505,10 @@ fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T | too_general_eqterms _ = false; -fun too_general_equality (Const ("op =", _) $ x $ y) = +fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) = too_general_eqterms (x,y) orelse too_general_eqterms(y,x) | too_general_equality _ = false; -(* tautologous? *) -fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true - | is_taut _ = false; - fun has_typed_var tycons = exists_subterm (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false); @@ -514,28 +516,29 @@ 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 = ["Product_Type.unit","bool"]; +val unwanted_types = [@{type_name unit}, @{type_name bool}]; fun unwanted t = - is_taut t orelse has_typed_var unwanted_types t orelse + t = @{prop True} orelse has_typed_var unwanted_types t orelse forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)); (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and likely to lead to unsound proofs.*) fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; -fun isFO thy goal_cls = case linkup_logic_mode of - Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls) - | Fol => true - | Hol => false +fun is_first_order thy goal_cls = + case translation_mode of + Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls) + | Fol => true + | Hol => false -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls = +fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt - val isFO = isFO thy goal_cls + val is_FO = is_first_order thy goal_cls val included_cls = get_all_lemmas ctxt - |> SFP.cnf_rules_pairs thy |> make_unique - |> restrict_to_logic thy isFO + |> cnf_rules_pairs thy |> make_unique + |> restrict_to_logic thy is_FO |> remove_unwanted_clauses in relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) @@ -547,28 +550,27 @@ let (* add chain thms *) val chain_cls = - SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths)) + cnf_rules_pairs thy (filter check_named (map pairname chain_ths)) val axcls = chain_cls @ axcls val extra_cls = chain_cls @ extra_cls - val isFO = isFO thy goal_cls + val is_FO = is_first_order thy goal_cls val ccls = subtract_cls goal_cls extra_cls - val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls + val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls val ccltms = map prop_of ccls and axtms = map (prop_of o #1) extra_cls val subs = tfree_classes_of_terms ccltms and supers = tvar_classes_of_terms axtms - and tycons = type_consts_of_terms thy (ccltms@axtms) + and tycons = type_consts_of_terms thy (ccltms @ axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = SHC.make_conjecture_clauses dfg thy ccls - val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls) - val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls) - val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, []) - val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers - val classrel_clauses = SFC.make_classrel_clauses thy subs supers' + val conjectures = make_conjecture_clauses dfg thy ccls + val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) + val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) + val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, []) + val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers + val classrel_clauses = make_classrel_clauses thy subs supers' in (Vector.fromList clnames, (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) end end; - diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 13:02:18 2010 +0100 @@ -8,6 +8,7 @@ sig val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit + val skolem_prefix: string val cnf_axiom: theory -> thm -> thm list val pairname: thm -> string * thm val multi_base_blacklist: string list @@ -15,7 +16,6 @@ val type_has_topsort: typ -> bool val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list val neg_clausify: thm list -> thm list - val expand_defs_tac: thm -> tactic val combinators: thm -> thm val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list val suppress_endtheory: bool Unsynchronized.ref @@ -26,8 +26,12 @@ structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR = struct +open Sledgehammer_FOL_Clause + val trace = Unsynchronized.ref false; -fun trace_msg msg = if ! trace then tracing (msg ()) else (); +fun trace_msg msg = if !trace then tracing (msg ()) else (); + +val skolem_prefix = "sko_" fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th); @@ -75,7 +79,7 @@ fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = (*Existential: declare a Skolem function, then insert into body and continue*) let - val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) + val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) val Ts = map type_of args0 val extraTs = rhs_extra_types (Ts ---> T) xtp @@ -110,7 +114,7 @@ val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*) val Ts = map type_of args val cT = Ts ---> T - val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count) + val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count) val c = Free (id, cT) val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) @@ -386,15 +390,14 @@ | cnf_rules_pairs_aux thy pairs ((name,th)::ths) = let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs handle THM _ => pairs | - Sledgehammer_FOL_Clause.CLAUSE _ => pairs + CLAUSE _ => pairs in cnf_rules_pairs_aux thy pairs' ths end; (*The combination of rev and tail recursion preserves the original order*) fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); -(**** Convert all facts of the theory into clauses - (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****) +(**** Convert all facts of the theory into FOL or HOL clauses ****) local @@ -455,43 +458,6 @@ lambda_free, but then the individual theory caches become much bigger.*) -(*** meson proof methods ***) - -(*Expand all new definitions of abstraction or Skolem functions in a proof state.*) -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a - | is_absko _ = false; - -fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*) - 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 sko_ functions. *) -fun expand_defs_tac st0 st = - let val hyps0 = #hyps (rep_thm st0) - val hyps = #hyps (crep_thm st) - val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps - val defs = filter (is_absko o Thm.term_of) newhyps - val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) - (map Thm.term_of hyps) - val fixed = OldTerm.term_frees (concl_of st) @ - fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) [] - in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; - - -fun meson_general_tac ctxt ths i st0 = - let - val thy = ProofContext.theory_of ctxt - val ctxt0 = Classical.put_claset HOL_cs ctxt - in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end; - -val meson_method_setup = - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) - "MESON resolution proof procedure"; - - (*** Converting a subgoal into negated conjecture clauses. ***) fun neg_skolemize_tac ctxt = @@ -534,11 +500,9 @@ "conversion of theorem to clauses"; - (** setup **) val setup = - meson_method_setup #> neg_clausify_setup #> clausify_setup #> perhaps saturate_skolem_cache #> diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 13:02:18 2010 +0100 @@ -44,19 +44,19 @@ datatype arLit = TConsLit of class * string * string list | TVarLit of class * string - datatype arityClause = ArityClause of + datatype arity_clause = ArityClause of {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} - datatype classrelClause = ClassrelClause of + datatype classrel_clause = ClassrelClause of {axiom_name: axiom_name, subclass: class, superclass: class} - val make_classrel_clauses: theory -> class list -> class list -> classrelClause list - val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list - val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list + val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list + val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list + val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table - val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table + val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table val class_of_arityLit: arLit -> class - val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table + val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table - val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table + val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table val init_functab: int Symtab.table val dfg_sign: bool -> string -> string val dfg_of_typeLit: bool -> type_literal -> string @@ -67,14 +67,14 @@ val string_of_start: string -> string val string_of_descrip : string -> string val dfg_tfree_clause : string -> string - val dfg_classrelClause: classrelClause -> string - val dfg_arity_clause: arityClause -> string + val dfg_classrel_clause: classrel_clause -> string + val dfg_arity_clause: arity_clause -> string val tptp_sign: bool -> string -> string val tptp_of_typeLit : bool -> type_literal -> string val gen_tptp_cls : int * string * kind * string list * string list -> string val tptp_tfree_clause : string -> string - val tptp_arity_clause : arityClause -> string - val tptp_classrelClause : classrelClause -> string + val tptp_arity_clause : arity_clause -> string + val tptp_classrel_clause : classrel_clause -> string end structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE = @@ -96,28 +96,23 @@ fun union_all xss = List.foldl (uncurry (union (op =))) [] xss; -(*Provide readable names for the more common symbolic functions*) +(* Provide readable names for the more common symbolic functions *) val const_trans_table = - Symtab.make [(@{const_name "op ="}, "equal"), - (@{const_name Orderings.less_eq}, "lessequals"), - (@{const_name "op &"}, "and"), - (@{const_name "op |"}, "or"), - (@{const_name "op -->"}, "implies"), - (@{const_name "op :"}, "in"), - ("Sledgehammer.fequal", "fequal"), - ("Sledgehammer.COMBI", "COMBI"), - ("Sledgehammer.COMBK", "COMBK"), - ("Sledgehammer.COMBB", "COMBB"), - ("Sledgehammer.COMBC", "COMBC"), - ("Sledgehammer.COMBS", "COMBS"), - ("Sledgehammer.COMBB'", "COMBB_e"), - ("Sledgehammer.COMBC'", "COMBC_e"), - ("Sledgehammer.COMBS'", "COMBS_e")]; + Symtab.make [(@{const_name "op ="}, "equal"), + (@{const_name Orderings.less_eq}, "lessequals"), + (@{const_name "op &"}, "and"), + (@{const_name "op |"}, "or"), + (@{const_name "op -->"}, "implies"), + (@{const_name "op :"}, "in"), + (@{const_name fequal}, "fequal"), + (@{const_name COMBI}, "COMBI"), + (@{const_name COMBK}, "COMBK"), + (@{const_name COMBB}, "COMBB"), + (@{const_name COMBC}, "COMBC"), + (@{const_name COMBS}, "COMBS")]; val type_const_trans_table = - Symtab.make [("*", "prod"), - ("+", "sum"), - ("~=>", "map")]; + Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")]; (*Escaping of special characters. Alphanumeric characters are left unchanged. @@ -290,7 +285,7 @@ datatype arLit = TConsLit of class * string * string list | TVarLit of class * string; -datatype arityClause = +datatype arity_clause = ArityClause of {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}; @@ -316,7 +311,7 @@ (**** Isabelle class relations ****) -datatype classrelClause = +datatype classrel_clause = ClassrelClause of {axiom_name: axiom_name, subclass: class, superclass: class}; @@ -330,13 +325,13 @@ fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers in List.foldl add_supers [] subs end; -fun make_classrelClause (sub,super) = +fun make_classrel_clause (sub,super) = ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, subclass = make_type_class sub, superclass = make_type_class super}; fun make_classrel_clauses thy subs supers = - map make_classrelClause (class_pairs thy subs supers); + map make_classrel_clause (class_pairs thy subs supers); (** Isabelle arities **) @@ -391,13 +386,13 @@ fun add_type_sort_preds (T, preds) = update_many (preds, map pred_of_sort (sorts_on_typs T)); -fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) = +fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) = Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass | class_of_arityLit (TVarLit (tclass, _)) = tclass; -fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) = +fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) = let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits) fun upd (class,preds) = Symtab.update (class,1) preds in List.foldl upd preds classes end; @@ -414,7 +409,7 @@ | add_type_sort_funcs (TFree (a, _), funcs) = Symtab.update (make_fixed_type_var a, 0) funcs -fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = +fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) = let val TConsLit (_, tcons, tvars) = conclLit in Symtab.update (tcons, length tvars) funcs end; @@ -480,7 +475,7 @@ fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)"; -fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = +fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ axiom_name ^ ").\n\n"; @@ -528,7 +523,7 @@ let val tvar = "(T)" in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; -fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = +fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" end; diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 13:02:18 2010 +0100 @@ -6,67 +6,54 @@ signature SLEDGEHAMMER_HOL_CLAUSE = sig - val ext: thm - val comb_I: thm - val comb_K: thm - val comb_B: thm - val comb_C: thm - val comb_S: thm - val minimize_applies: bool + type kind = Sledgehammer_FOL_Clause.kind + type fol_type = Sledgehammer_FOL_Clause.fol_type + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause + type arity_clause = Sledgehammer_FOL_Clause.arity_clause type axiom_name = string type polarity = bool - type clause_id = int + type hol_clause_id = int + datatype combterm = - CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*) - | CombVar of string * Sledgehammer_FOL_Clause.fol_type - | CombApp of combterm * combterm + CombConst of string * fol_type * fol_type list (* Const and Free *) | + CombVar of string * fol_type | + CombApp of combterm * combterm datatype literal = Literal of polarity * combterm - datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, - kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list} - val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type - val strip_comb: combterm -> combterm * combterm list - val literals_of_term: theory -> term -> literal list * typ list - exception TOO_TRIVIAL - val make_conjecture_clauses: bool -> theory -> thm list -> clause list - val make_axiom_clauses: bool -> - theory -> - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list - val get_helper_clauses: bool -> - theory -> - bool -> - clause list * (thm * (axiom_name * clause_id)) list * string list -> - clause list - val tptp_write_file: bool -> Path.T -> - clause list * clause list * clause list * clause list * - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> + datatype hol_clause = + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, + kind: kind, literals: literal list, ctypes_sorts: typ list} + + val type_of_combterm : combterm -> fol_type + val strip_combterm_comb : combterm -> combterm * combterm list + val literals_of_term : theory -> term -> literal list * typ list + exception TRIVIAL + val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list + val make_axiom_clauses : bool -> theory -> + (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list + val get_helper_clauses : bool -> theory -> bool -> + hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> + hol_clause list + val write_tptp_file : bool -> Path.T -> + hol_clause list * hol_clause list * hol_clause list * hol_clause list * + classrel_clause list * arity_clause list -> int * int - val dfg_write_file: bool -> Path.T -> - clause list * clause list * clause list * clause list * - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> - int * int + val write_dfg_file : bool -> Path.T -> + hol_clause list * hol_clause list * hol_clause list * hol_clause list * + classrel_clause list * arity_clause list -> int * int end structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = struct -structure SFC = Sledgehammer_FOL_Clause; - -(* theorems for combinators and function extensionality *) -val ext = thm "HOL.ext"; -val comb_I = thm "Sledgehammer.COMBI_def"; -val comb_K = thm "Sledgehammer.COMBK_def"; -val comb_B = thm "Sledgehammer.COMBB_def"; -val comb_C = thm "Sledgehammer.COMBC_def"; -val comb_S = thm "Sledgehammer.COMBS_def"; -val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal"; -val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal"; - +open Sledgehammer_FOL_Clause +open Sledgehammer_Fact_Preprocessor (* Parameter t_full below indicates that full type information is to be exported *) -(*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.*) +(* 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. *) val minimize_applies = true; fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); @@ -84,21 +71,18 @@ type axiom_name = string; type polarity = bool; -type clause_id = int; +type hol_clause_id = int; -datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*) - | CombVar of string * SFC.fol_type - | CombApp of combterm * combterm +datatype combterm = + CombConst of string * fol_type * fol_type list (* Const and Free *) | + CombVar of string * fol_type | + CombApp of combterm * combterm datatype literal = Literal of polarity * combterm; -datatype clause = - Clause of {clause_id: clause_id, - axiom_name: axiom_name, - th: thm, - kind: SFC.kind, - literals: literal list, - ctypes_sorts: typ list}; +datatype hol_clause = + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, + kind: kind, literals: literal list, ctypes_sorts: typ list}; (*********************************************************************) @@ -106,8 +90,7 @@ (*********************************************************************) fun isFalse (Literal(pol, CombConst(c,_,_))) = - (pol andalso c = "c_False") orelse - (not pol andalso c = "c_True") + (pol andalso c = "c_False") orelse (not pol andalso c = "c_True") | isFalse _ = false; fun isTrue (Literal (pol, CombConst(c,_,_))) = @@ -115,24 +98,22 @@ (not pol andalso c = "c_False") | isTrue _ = false; -fun isTaut (Clause {literals,...}) = exists isTrue literals; +fun isTaut (HOLClause {literals,...}) = exists isTrue literals; fun type_of dfg (Type (a, Ts)) = let val (folTypes,ts) = types_of dfg Ts - in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end - | type_of _ (tp as TFree (a, _)) = - (SFC.AtomF (SFC.make_fixed_type_var a), [tp]) - | type_of _ (tp as TVar (v, _)) = - (SFC.AtomV (SFC.make_schematic_type_var v), [tp]) + in (Comp(make_fixed_type_const dfg a, folTypes), ts) end + | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp]) + | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp]) and types_of dfg Ts = let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) - in (folTyps, SFC.union_all ts) end; + in (folTyps, union_all ts) end; (* same as above, but no gathering of sort information *) fun simp_type_of dfg (Type (a, Ts)) = - SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) - | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a) - | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v); + Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) + | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a) + | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v); fun const_type_of dfg thy (c,t) = @@ -142,27 +123,27 @@ (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) fun combterm_of dfg thy (Const(c,t)) = let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) - val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list) + val c' = CombConst(make_fixed_const dfg c, tp, tvar_list) in (c',ts) end | combterm_of dfg _ (Free(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombConst(SFC.make_fixed_var v, tp, []) + val v' = CombConst(make_fixed_var v, tp, []) in (v',ts) end | combterm_of dfg _ (Var(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombVar(SFC.make_schematic_var v,tp) + val v' = CombVar(make_schematic_var v,tp) in (v',ts) end | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q in (CombApp(P',Q'), union (op =) tsP tsQ) end - | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t); + | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t); -fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) +fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity) | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); -fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P - | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) = +fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P + | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) = literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q | literals_of_term1 dfg thy (lits,ts) P = let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) @@ -173,23 +154,23 @@ fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; val literals_of_term = literals_of_term_dfg false; -(* Problem too trivial for resolution (empty clause) *) -exception TOO_TRIVIAL; +(* Trivial problem, which resolution cannot handle (empty clause) *) +exception TRIVIAL; (* making axiom and conjecture clauses *) -fun make_clause dfg thy (clause_id,axiom_name,kind,th) = +fun make_clause dfg thy (clause_id, axiom_name, kind, th) = let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th) in - if forall isFalse lits - then raise TOO_TRIVIAL + if forall isFalse lits then + raise TRIVIAL else - Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, - literals = lits, ctypes_sorts = ctypes_sorts} + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts} end; fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = - let val cls = make_clause dfg thy (id, name, SFC.Axiom, th) + let val cls = make_clause dfg thy (id, name, Axiom, th) in if isTaut cls then pairs else (name,cls)::pairs end; @@ -198,7 +179,7 @@ fun make_conjecture_clauses_aux _ _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = - make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) :: + make_clause dfg thy (n,"conjecture", Conjecture, th) :: make_conjecture_clauses_aux dfg thy (n+1) ths; fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0; @@ -211,7 +192,7 @@ (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) -fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2 +fun result_type (Comp ("tc_fun", [_, tp2])) = tp2 | result_type _ = error "result_type" fun type_of_combterm (CombConst (_, tp, _)) = tp @@ -219,7 +200,7 @@ | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1); (*gets the head of a combinator application, along with the list of arguments*) -fun strip_comb u = +fun strip_combterm_comb u = let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) | stripc x = x in stripc(u,[]) end; @@ -231,10 +212,10 @@ fun wrap_type t_full (s, tp) = if t_full then - type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp] + type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s; -fun apply ss = "hAPP" ^ SFC.paren_pack ss; +fun apply ss = "hAPP" ^ paren_pack ss; fun rev_apply (v, []) = v | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; @@ -251,10 +232,9 @@ Int.toString nargs ^ " but is applied to " ^ space_implode ", " args) val args2 = List.drop(args, nargs) - val targs = if not t_full then map SFC.string_of_fol_type tvars - else [] + val targs = if not t_full then map string_of_fol_type tvars else [] in - string_apply (c ^ SFC.paren_pack (args1@targs), args2) + string_apply (c ^ paren_pack (args1@targs), args2) end | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) | string_of_applic _ _ _ = error "string_of_applic"; @@ -263,7 +243,7 @@ if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s; fun string_of_combterm (params as (t_full, cma, cnh)) t = - let val (head, args) = strip_comb t + let val (head, args) = strip_combterm_comb t in wrap_type_if t_full cnh (head, string_of_applic t_full cma (head, map (string_of_combterm (params)) args), type_of_combterm t) @@ -271,15 +251,15 @@ (*Boolean-valued terms are here converted to literals.*) fun boolify params t = - "hBOOL" ^ SFC.paren_pack [string_of_combterm params t]; + "hBOOL" ^ paren_pack [string_of_combterm params t]; fun string_of_predicate (params as (_,_,cnh)) t = case t of (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => (*DFG only: new TPTP prefers infix equality*) - ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2]) + ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2]) | _ => - case #1 (strip_comb t) of + case #1 (strip_combterm_comb t) of CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t | _ => boolify params t; @@ -290,31 +270,31 @@ let val eqop = if pol then " = " else " != " in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end; -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) = tptp_of_equality params pol (t1,t2) | tptp_literal params (Literal(pol,pred)) = - SFC.tptp_sign pol (string_of_predicate params pred); + tptp_sign pol (string_of_predicate params pred); (*Given a clause, returns its literals paired with a list of literals concerning TFrees; the latter should only occur in conjecture clauses.*) -fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = +fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = (map (tptp_literal params) literals, - map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts)); + map (tptp_of_typeLit pos) (add_typs ctypes_sorts)); -fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) = - let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls +fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) = + let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls in - (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) + (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits) end; (*** dfg format ***) -fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred); +fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred); -fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = +fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = (map (dfg_literal params) literals, - map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts)); + map (dfg_of_typeLit pos) (add_typs ctypes_sorts)); fun get_uvars (CombConst _) vars = vars | get_uvars (CombVar(v,_)) vars = (v::vars) @@ -322,20 +302,21 @@ fun get_uvars_l (Literal(_,c)) = get_uvars c []; -fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals); +fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals); -fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = - let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls +fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind, + ctypes_sorts, ...}) = + let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls val vars = dfg_vars cls - val tvars = SFC.get_tvar_strs ctypes_sorts + val tvars = get_tvar_strs ctypes_sorts in - (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) + (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) end; (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars; +fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = if c = "equal" then (addtypes tvars funcs, preds) @@ -348,33 +329,33 @@ else (addtypes tvars funcs, addit preds) end | add_decls _ (CombVar(_,ctp), (funcs,preds)) = - (SFC.add_foltype_funcs (ctp,funcs), preds) + (add_foltype_funcs (ctp,funcs), preds) | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); -fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls); +fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls); -fun add_clause_decls params (Clause {literals, ...}, decls) = +fun add_clause_decls params (HOLClause {literals, ...}, decls) = List.foldl (add_literal_decls params) decls literals handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") fun decls_of_clauses params clauses arity_clauses = - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab) + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab) val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) in - (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses), + (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses), Symtab.dest predtab) end; -fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = - List.foldl SFC.add_type_sort_preds preds ctypes_sorts +fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) = + List.foldl add_type_sort_preds preds ctypes_sorts handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = Symtab.dest - (List.foldl SFC.add_classrelClause_preds - (List.foldl SFC.add_arityClause_preds + (List.foldl add_classrel_clause_preds + (List.foldl add_arity_clause_preds (List.foldl add_clause_preds Symtab.empty clauses) arity_clauses) clsrel_clauses) @@ -385,9 +366,8 @@ (**********************************************************************) val init_counters = - Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), - ("c_COMBB", 0), ("c_COMBC", 0), - ("c_COMBS", 0)]; + Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), + ("c_COMBS", 0)]; fun count_combterm (CombConst (c, _, _), ct) = (case Symtab.lookup ct c of NONE => ct (*no counter*) @@ -397,18 +377,18 @@ fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); -fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals; +fun count_clause (HOLClause {literals, ...}, ct) = + List.foldl count_literal ct literals; -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) = if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals else ct; -fun cnf_helper_thms thy = - Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy - o map Sledgehammer_Fact_Preprocessor.pairname +fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = - if isFO then [] (*first-order*) + if isFO then + [] else let val axclauses = map #2 (make_axiom_clauses dfg thy axcls) @@ -416,15 +396,15 @@ val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses fun needed c = the (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" - then cnf_helper_thms thy [comb_I,comb_K] + then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] else [] val BC = if needed "c_COMBB" orelse needed "c_COMBC" - then cnf_helper_thms thy [comb_B,comb_C] + then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}] else [] - val S = if needed "c_COMBS" - then cnf_helper_thms thy [comb_S] + val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}] else [] - val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal] + val other = cnf_helper_thms thy [@{thm fequal_imp_equal}, + @{thm equal_imp_fequal}] in map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end; @@ -432,7 +412,7 @@ (*Find the minimal arity of each function mentioned in the term. Also, note which uses are not at top level, to see if hBOOL is needed.*) fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = - let val (head, args) = strip_comb t + let val (head, args) = strip_combterm_comb t val n = length args val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL) in @@ -451,11 +431,12 @@ fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) = count_constants_term true t (const_min_arity, const_needs_hBOOL); -fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) = +fun count_constants_clause (HOLClause {literals, ...}) + (const_min_arity, const_needs_hBOOL) = fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); fun display_arity const_needs_hBOOL (c,n) = - Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^ + trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else "")); @@ -469,31 +450,31 @@ in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); -(* tptp format *) +(* TPTP format *) -fun tptp_write_file t_full file clauses = +fun write_tptp_file t_full file clauses = let val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) - val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) + val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) val _ = File.write_list file ( map (#1 o (clause2tptp params)) axclauses @ tfree_clss @ tptp_clss @ - map SFC.tptp_classrelClause classrel_clauses @ - map SFC.tptp_arity_clause arity_clauses @ + map tptp_classrel_clause classrel_clauses @ + map tptp_arity_clause arity_clauses @ map (#1 o (clause2tptp params)) helper_clauses) in (length axclauses + 1, length tfree_clss + length tptp_clss) end; -(* dfg format *) +(* DFG format *) -fun dfg_write_file t_full file clauses = +fun write_dfg_file t_full file clauses = let val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses @@ -502,20 +483,20 @@ val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) and probname = Path.implode (Path.base file) val axstrs = map (#1 o (clause2dfg params)) axclauses - val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss) + val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses val _ = File.write_list file ( - SFC.string_of_start probname :: - SFC.string_of_descrip probname :: - SFC.string_of_symbols (SFC.string_of_funcs funcs) - (SFC.string_of_preds (cl_preds @ ty_preds)) :: + string_of_start probname :: + string_of_descrip probname :: + string_of_symbols (string_of_funcs funcs) + (string_of_preds (cl_preds @ ty_preds)) :: "list_of_clauses(axioms,cnf).\n" :: axstrs @ - map SFC.dfg_classrelClause classrel_clauses @ - map SFC.dfg_arity_clause arity_clauses @ + map dfg_classrel_clause classrel_clauses @ + map dfg_arity_clause arity_clauses @ helper_clauses_strs @ ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ tfree_clss @ @@ -530,4 +511,3 @@ end; end; - diff -r 23908b4dbc2f -r 2f8fb5242799 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 06:14:37 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 13:02:18 2010 +0100 @@ -7,33 +7,29 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig val chained_hint: string - - val fix_sorts: sort Vartab.table -> term -> term val invert_const: string -> string val invert_type_const: string -> string val num_typargs: theory -> string -> int val make_tvar: string -> typ val strip_prefix: string -> string -> string option val setup: theory -> theory - (* extracting lemma list*) - val find_failure: string -> string option - val lemma_list: bool -> string -> + val is_proof_well_formed: string -> bool + val metis_lemma_list: bool -> string -> string * string vector * (int * int) * Proof.context * thm * int -> string * string list - (* structured proofs *) - val structured_proof: string -> + val structured_isar_proof: string -> string * string vector * (int * int) * Proof.context * thm * int -> string * string list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = struct -structure SFC = Sledgehammer_FOL_Clause +open Sledgehammer_FOL_Clause +open Sledgehammer_Fact_Preprocessor -val trace_path = Path.basic "atp_trace"; +val trace_proof_path = Path.basic "atp_trace"; -fun trace s = - if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s - else (); +fun trace_proof_msg f = + if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else (); fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); @@ -43,9 +39,6 @@ (*Indicates whether to include sort information in generated proofs*) val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true; -(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*) -(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *) - val setup = modulus_setup #> recon_sorts_setup; (**** PARSING OF TSTP FORMAT ****) @@ -109,12 +102,12 @@ (*If string s has the prefix s1, return the result of deleting it.*) fun strip_prefix s1 s = if String.isPrefix s1 s - then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE))) + then SOME (undo_ascii_of (String.extract (s, size s1, NONE))) else NONE; (*Invert the table of translations between Isabelle and ATPs*) val type_const_trans_table_inv = - Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table)); + Symtab.make (map swap (Symtab.dest type_const_trans_table)); fun invert_type_const c = case Symtab.lookup type_const_trans_table_inv c of @@ -132,15 +125,15 @@ | Br (a,ts) => let val Ts = map type_of_stree ts in - case strip_prefix SFC.tconst_prefix a of + case strip_prefix tconst_prefix a of SOME b => Type(invert_type_const b, Ts) | NONE => if not (null ts) then raise STREE t (*only tconsts have type arguments*) else - case strip_prefix SFC.tfree_prefix a of + case strip_prefix tfree_prefix a of SOME b => TFree("'" ^ b, HOLogic.typeS) | NONE => - case strip_prefix SFC.tvar_prefix a of + case strip_prefix tvar_prefix a of SOME b => make_tvar b | NONE => make_tvar a (*Variable from the ATP, say X1*) end; @@ -148,7 +141,7 @@ (*Invert the table of translations between Isabelle and ATPs*) val const_trans_table_inv = Symtab.update ("fequal", "op =") - (Symtab.make (map swap (Symtab.dest SFC.const_trans_table))); + (Symtab.make (map swap (Symtab.dest const_trans_table))); fun invert_const c = case Symtab.lookup const_trans_table_inv c of @@ -169,9 +162,9 @@ | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*) | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t | Br (a,ts) => - case strip_prefix SFC.const_prefix a of + case strip_prefix const_prefix a of SOME "equal" => - list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts) + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts) | SOME b => let val c = invert_const b val nterms = length ts - num_typargs thy c @@ -183,10 +176,10 @@ | NONE => (*a variable, not a constant*) let val T = HOLogic.typeT val opr = (*a Free variable is typically a Skolem function*) - case strip_prefix SFC.fixed_var_prefix a of + case strip_prefix fixed_var_prefix a of SOME b => Free(b,T) | NONE => - case strip_prefix SFC.schematic_var_prefix a of + case strip_prefix schematic_var_prefix a of SOME b => make_var (b,T) | NONE => make_var (a,T) (*Variable from the ATP, say X1*) in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; @@ -196,7 +189,7 @@ | constraint_of_stree pol t = case t of Int _ => raise STREE t | Br (a,ts) => - (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of + (case (strip_prefix class_prefix a, map type_of_stree ts) of (SOME b, [T]) => (pol, b, T) | _ => raise STREE t); @@ -286,7 +279,7 @@ may disagree. We have to try all combinations of literals (quadratic!) and match up the variable names consistently. **) -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) = +fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) = strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) | strip_alls_aux _ t = t; @@ -347,7 +340,7 @@ ATP may have their literals reordered.*) fun isar_lines ctxt ctms = let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term) - val _ = trace ("\n\nisar_lines: start\n") + val _ = trace_proof_msg (K "\n\nisar_lines: start\n") fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*) (case permuted_clause t ctms of SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n" @@ -399,7 +392,7 @@ | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); -fun bad_free (Free (a,_)) = String.isPrefix "sko_" a +fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a | bad_free _ = false; (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies. @@ -436,26 +429,22 @@ | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; fun decode_tstp_file cnfs ctxt th sgno thm_names = - let val _ = trace "\ndecode_tstp_file: start\n" + let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n") val tuples = map (dest_tstp o tstp_line o explode) cnfs - val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n") + val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n") val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) - val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n") + val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n") val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines - val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") - val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines - val _ = trace (Int.toString (length lines) ^ " lines extracted\n") - val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno - val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n") + val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") + val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines + val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n") + val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno + val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n") val ccls = map forall_intr_vars ccls - val _ = - if ! Sledgehammer_Fact_Preprocessor.trace then - app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls - else - () + val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) - val _ = trace "\ndecode_tstp_file: finishing\n" + val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n") in isar_header (map #1 fixes) ^ implode ilines ^ "qed\n" end handle STREE _ => error "Could not extract proof (ATP output malformed?)"; @@ -463,11 +452,11 @@ (*=== EXTRACTING PROOF-TEXT === *) -val begin_proof_strings = ["# SZS output start CNFRefutation.", +val begin_proof_strs = ["# SZS output start CNFRefutation.", "=========== Refutation ==========", "Here is a proof"]; -val end_proof_strings = ["# SZS output end CNFRefutation", +val end_proof_strs = ["# SZS output end CNFRefutation", "======= End of refutation =======", "Formulae used in the proof"]; @@ -475,8 +464,8 @@ let (*splits to_split by the first possible of a list of splitters*) val (begin_string, end_string) = - (find_first (fn s => String.isSubstring s proof) begin_proof_strings, - find_first (fn s => String.isSubstring s proof) end_proof_strings) + (find_first (fn s => String.isSubstring s proof) begin_proof_strs, + find_first (fn s => String.isSubstring s proof) end_proof_strs) in if is_none begin_string orelse is_none end_string then error "Could not extract proof (no substring indicating a proof)" @@ -484,36 +473,24 @@ |> first_field (the end_string) |> the |> fst end; -(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *) +(* ==== CHECK IF PROOF WAS SUCCESSFUL === *) -val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable", - "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"]; -val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; -val failure_strings_SPASS = ["SPASS beiseite: Completion found.", - "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."]; -val failure_strings_remote = ["Remote-script could not extract proof"]; -fun find_failure proof = - let val failures = - map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote) - val correct = null failures andalso - exists (fn s => String.isSubstring s proof) begin_proof_strings andalso - exists (fn s => String.isSubstring s proof) end_proof_strings - in - if correct then NONE - else if null failures then SOME "Output of ATP not in proper format" - else SOME (hd failures) end; +fun is_proof_well_formed proof = + exists (fn s => String.isSubstring s proof) begin_proof_strs andalso + exists (fn s => String.isSubstring s proof) end_proof_strs (* === EXTRACTING LEMMAS === *) (* lines have the form "cnf(108, axiom, ...", the number (108) has to be extracted)*) -fun get_step_nums false proofextract = - let val toks = String.tokens (not o Char.isAlphaNum) - fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok - | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok - | inputno _ = NONE - val lines = split_lines proofextract - in map_filter (inputno o toks) lines end +fun get_step_nums false extract = + let + val toks = String.tokens (not o Char.isAlphaNum) + fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok + | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) = + Int.fromString ntok + | inputno _ = NONE + val lines = split_lines extract + in map_filter (inputno o toks) lines end (*String contains multiple lines. We want those of the form "253[0:Inp] et cetera..." A list consisting of the first number in each line is returned. *) @@ -527,27 +504,25 @@ (*extracting lemmas from tstp-output between the lines from above*) fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = let - (* get the names of axioms from their numbers*) - fun get_axiom_names thm_names step_nums = - let - val last_axiom = Vector.length thm_names - fun is_axiom n = n <= last_axiom - fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count - fun getname i = Vector.sub(thm_names, i-1) - in - (sort_distinct string_ord (filter (fn x => x <> "??.unknown") - (map getname (filter is_axiom step_nums))), - exists is_conj step_nums) - end - val proofextract = get_proof_extract proof - in - get_axiom_names thm_names (get_step_nums proofextract) - end; + (* get the names of axioms from their numbers*) + fun get_axiom_names thm_names step_nums = + let + val last_axiom = Vector.length thm_names + fun is_axiom n = n <= last_axiom + fun is_conj n = n >= fst conj_count andalso + n < fst conj_count + snd conj_count + fun getname i = Vector.sub(thm_names, i-1) + in + (sort_distinct string_ord (filter (fn x => x <> "??.unknown") + (map getname (filter is_axiom step_nums))), + exists is_conj step_nums) + end + in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end; (*Used to label theorems chained into the sledgehammer call*) val chained_hint = "CHAINED"; -val nochained = filter_out (fn y => y = chained_hint) - +val kill_chained = filter_out (curry (op =) chained_hint) + (* metis-command *) fun metis_line [] = "apply metis" | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" @@ -556,33 +531,36 @@ fun minimize_line _ [] = "" | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ - space_implode " " (nochained lemmas)) + space_implode " " (kill_chained lemmas)) -fun sendback_metis_nochained lemmas = - (Markup.markup Markup.sendback o metis_line) (nochained lemmas) +val sendback_metis_no_chained = + Markup.markup Markup.sendback o metis_line o kill_chained -fun lemma_list dfg name result = +fun metis_lemma_list dfg name result = let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result - in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^ - (if used_conj then "" - else "\nWarning: Goal is provable because context is inconsistent."), - nochained lemmas) + in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^ + (if used_conj then + "" + else + "\nWarning: The goal is provable because the context is inconsistent."), + kill_chained lemmas) end; -(* === Extracting structured Isar-proof === *) -fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) = +fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt, + goal, subgoalno)) = let - (*Could use split_lines, but it can return blank lines...*) - val lines = String.tokens (equal #"\n"); - val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c) - val proofextract = get_proof_extract proof - val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - val (one_line_proof, lemma_names) = lemma_list false name result - val structured = - if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" - else decode_tstp_file cnfs ctxt goal subgoalno thm_names + (* Could use "split_lines", but it can return blank lines *) + val lines = String.tokens (equal #"\n"); + val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c) + val extract = get_proof_extract proof + val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) + val (one_line_proof, lemma_names) = metis_lemma_list false name result + val structured = + if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" + else decode_tstp_file cnfs ctxt goal subgoalno thm_names in - (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names) -end + (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, + lemma_names) + end end;