# HG changeset patch # User bulwahn # Date 1269262095 -3600 # Node ID 5ed2e9a545ac47046e9e45d084b791271806623d # Parent 3122bdd9527576e8ec4f5268d2c8aa237a2c03e4# Parent 9b579860d59b07312f16a7ebaf99f7f2688e75ee merged diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 13:48:15 2010 +0100 @@ -63,9 +63,8 @@ THEN' Boogie_Tactics.drop_assert_at_tac THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context)) in -fun boogie_vc (vc_name, vc_opts) lthy = +fun boogie_vc (vc_name, vc_opts) thy = let - val thy = ProofContext.theory_of lthy val vc = get_vc thy vc_name fun extract vc l = @@ -92,16 +91,16 @@ | _ => (pair ts, K I)) val discharge = fold (Boogie_VCs.discharge o pair vc_name) - fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms)) + fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms)) | after_qed _ = I in - lthy + ProofContext.init thy |> fold Variable.auto_fixes ts - |> (fn lthy1 => lthy1 + |> (fn ctxt1 => ctxt1 |> prepare - |-> (fn us => fn lthy2 => lthy2 + |-> (fn us => fn ctxt2 => ctxt2 |> Proof.theorem_i NONE (fn thmss => fn ctxt => - let val export = map (finish lthy1) o ProofContext.export ctxt lthy2 + let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2 in after_qed (map export thmss) ctxt end) [map (rpair []) us])) end end @@ -300,7 +299,7 @@ "Enter into proof mode for a specific verification condition." OuterKeyword.thy_goal (vc_name -- vc_opts >> (fn args => - (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args)))) + (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args)))) val quick_timeout = 5 diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 13:48:15 2010 +0100 @@ -238,10 +238,14 @@ |> split_list_kind thy o Termtab.dest in fun add_axioms verbose axs thy = - let val (used, new) = mark_axioms thy (name_axioms axs) + let + val (used, new) = mark_axioms thy (name_axioms axs) + fun add (n, t) = + Specification.axiomatization [] [((Binding.name n, []), [t])] #>> + hd o hd o snd in thy - |> fold_map (Drule.add_axiom o apfst Binding.name) new + |> fold_map add new |-> Context.theory_map o fold Boogie_Axioms.add_thm |> log verbose "The following axioms were added:" (map fst new) |> (fn thy' => log verbose "The following axioms already existed:" diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Boogie/Tools/boogie_vcs.ML --- a/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 13:48:15 2010 +0100 @@ -27,6 +27,9 @@ val state_of_vc: theory -> string -> string list * string list val close: theory -> theory val is_closed: theory -> bool + + val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) -> + theory -> theory end structure Boogie_VCs: BOOGIE_VCS = @@ -252,30 +255,35 @@ (* the VC store *) -fun err_vcs () = error "undischarged Boogie verification conditions found" +fun err_unfinished () = error "An unfinished Boogie environment is still open." + +fun err_vcs names = error (Pretty.string_of + (Pretty.big_list "Undischarged Boogie verification conditions found:" + (map Pretty.str names))) structure VCs = Theory_Data ( - type T = (vc * thm) Symtab.table option + type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option val empty = NONE val extend = I fun merge (NONE, NONE) = NONE - | merge _ = err_vcs () + | merge _ = err_unfinished () ) -fun prep thy t = vc_of_term t |> (fn vc => (vc, thm_of thy vc)) +fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc))) fun set vcs thy = VCs.map (fn - NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs)) - | SOME _ => err_vcs ()) thy + NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I) + | SOME _ => err_unfinished ()) thy fun lookup thy name = (case VCs.get thy of - SOME vcs => Option.map fst (Symtab.lookup vcs name) + SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name) | NONE => NONE) fun discharge (name, prf) = - VCs.map (Option.map (Symtab.map_entry name (join prf))) + let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t) + in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end datatype state = Proved | NotProved | PartiallyProved @@ -284,21 +292,35 @@ SOME vc => names_of vc | NONE => ([], [])) +fun state_of_vc' (vc, _) = + (case names_of vc of + ([], _) => Proved + | (_, []) => NotProved + | (_, _) => PartiallyProved) + fun state_of thy = (case VCs.get thy of - SOME vcs => Symtab.dest vcs |> map (apsnd (fst #> names_of #> (fn - ([], _) => Proved - | (_, []) => NotProved - | (_, _) => PartiallyProved))) + SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs) | NONE => []) +fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t + fun close thy = thy |> VCs.map (fn - SOME _ => - if forall (fn (_, Proved) => true | _ => false) (state_of thy) - then NONE - else err_vcs () + SOME (vcs, g) => + let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc + in + Symtab.dest vcs + |> map_filter (fn (n, vc) => if check vc then NONE else SOME n) + |> (fn names => if null names then NONE else err_vcs names) + end | NONE => NONE) val is_closed = is_none o VCs.get +fun rewrite_vcs f g thy = + let + fun rewr (_, (t, _)) = vc_of_term (f thy t) + |> (fn vc => (vc, (t, thm_of thy vc))) + in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end + end diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/IsaMakefile Mon Mar 22 13:48:15 2010 +0100 @@ -313,11 +313,13 @@ 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 \ Tools/Sledgehammer/sledgehammer_fol_clause.ML \ Tools/Sledgehammer/sledgehammer_hol_clause.ML \ + Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ Tools/string_code.ML \ Tools/string_syntax.ML \ diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 13:48:15 2010 +0100 @@ -42,8 +42,7 @@ datatype min_data = MinData of { succs: int, - ab_ratios: int, - it_ratios: int + ab_ratios: int } fun make_sh_data @@ -51,23 +50,22 @@ ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} -fun make_min_data (succs, ab_ratios, it_ratios) = - MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios} +fun make_min_data (succs, ab_ratios) = + MinData{succs=succs, ab_ratios=ab_ratios} fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) = MeData{calls=calls, success=success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0) -val empty_min_data = make_min_data(0, 0, 0) -val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), []) +val empty_min_data = make_min_data (0, 0) +val empty_me_data = make_me_data (0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) = - (succs, ab_ratios, it_ratios) +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas, posns}) = (calls, success, proofs, time, timeout, lemmas, posns) @@ -147,13 +145,10 @@ => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t)) val inc_min_succs = map_min_data - (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios)) + (fn (succs,ab_ratios) => (succs+1, ab_ratios)) fun inc_min_ab_ratios r = map_min_data - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios)) - -fun inc_min_it_ratios r = map_min_data - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) + (fn (succs, ab_ratios) => (succs, ab_ratios+r)) val inc_metis_calls = map_me_data (fn (calls,success,proofs,time,timeout,lemmas,posns) @@ -234,10 +229,9 @@ else () ) -fun log_min_data log (succs, ab_ratios, it_ratios) = +fun log_min_data log (succs, ab_ratios) = (log ("Number of successful minimizations: " ^ string_of_int succs); - log ("After/before ratios: " ^ string_of_int ab_ratios); - log ("Iterations ratios: " ^ string_of_int it_ratios) + log ("After/before ratios: " ^ string_of_int ab_ratios) ) in @@ -313,19 +307,19 @@ ctxt |> change_dir dir |> Config.put ATP_Wrapper.measure_runtime true - val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); + val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result, + val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout in if success then (message, SH_OK (time_isa, time_atp, theorem_names)) else (message, SH_FAIL(time_isa, time_atp)) end - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, [])) + handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, [])) | ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) @@ -380,9 +374,10 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let + open ATP_Minimal val n0 = length (these (!named_thms)) val (prover_name, prover) = get_atp (Proof.theory_of st) args - val minimize = ATP_Minimal.minimalize prover prover_name + val minimize = minimize_theorems linear_minimize prover prover_name val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) @@ -390,10 +385,9 @@ val _ = log separator in case minimize timeout st (these (!named_thms)) of - (SOME (named_thms',its), msg) => + (SOME named_thms', msg) => (change_data id inc_min_succs; change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); - change_data id (inc_min_it_ratios ((100*its) div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") else (named_thms := SOME named_thms'; diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Mar 22 13:48:15 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,71 +20,72 @@ ("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/sledgehammer_isar.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) @@ -91,35 +94,24 @@ 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" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" setup Sledgehammer_Proof_Reconstruct.setup use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" - +use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup -use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_minimal.ML" +use "Tools/Sledgehammer/sledgehammer_isar.ML" -text {* basic provers *} -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *} -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *} -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *} -text {* provers with stuctured output *} -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *} -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *} +subsection {* The MESON prover *} -text {* on some problems better results *} -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *} - -text {* remote provers via SystemOnTPTP *} -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 *} - +use "Tools/Sledgehammer/meson_tactic.ML" +setup Meson_Tactic.setup subsection {* The Metis prover *} diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 13:48:15 2010 +0100 @@ -7,6 +7,23 @@ signature ATP_MANAGER = sig + type problem = + {with_full_types: bool, + subgoal: int, + goal: Proof.context * (thm list * thm), + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option} + val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem + type prover_result = + {success: bool, + message: string, + theorem_names: string list, + runtime: int, + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list} + type prover = int -> problem -> prover_result + val atps: string Unsynchronized.ref val get_atps: unit -> string list val timeout: int Unsynchronized.ref @@ -14,15 +31,43 @@ val kill: unit -> unit val info: unit -> unit val messages: int option -> unit - val add_prover: string * ATP_Wrapper.prover -> theory -> theory - val get_prover: theory -> string -> ATP_Wrapper.prover option + val add_prover: string * prover -> theory -> theory + val get_prover: theory -> string -> prover option val print_provers: theory -> unit val sledgehammer: string list -> Proof.state -> unit end; -structure ATP_Manager: ATP_MANAGER = +structure ATP_Manager : ATP_MANAGER = struct +(** problems, results, and provers **) + +type problem = + {with_full_types: bool, + subgoal: int, + goal: Proof.context * (thm list * thm), + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option}; + +fun problem_of_goal with_full_types subgoal goal : problem = + {with_full_types = with_full_types, + subgoal = subgoal, + goal = goal, + axiom_clauses = NONE, + filtered_clauses = NONE}; + +type prover_result = + {success: bool, + message: string, + theorem_names: string list, (*relevant theorems*) + runtime: int, (*user time of the ATP, in milliseconds*) + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list}; + +type prover = int -> problem -> prover_result; + + (** preferences **) val message_store_limit = 20; @@ -228,7 +273,7 @@ structure Provers = Theory_Data ( - type T = (ATP_Wrapper.prover * stamp) Symtab.table; + type T = (prover * stamp) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (eq_snd op =) data @@ -261,9 +306,9 @@ val _ = Toplevel.thread true (fn () => let val _ = register birth_time death_time (Thread.self (), desc); - val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal)); + val problem = 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 ()); @@ -282,36 +327,4 @@ val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers; in () end; - - -(** Isar command syntax **) - -local structure K = OuterKeyword and P = OuterParse in - -val _ = - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); - -val _ = - OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)); - -val _ = - OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> - (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit))); - -val _ = - OuterSyntax.improper_command "print_atps" "print external provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o - Toplevel.keep (print_provers o Toplevel.theory_of))); - -val _ = - OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag - (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (sledgehammer names o Toplevel.proof_of))); - end; - -end; - diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 13:48:15 2010 +0100 @@ -1,32 +1,40 @@ (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML Author: Philipp Meyer, TU Muenchen -Minimization of theorem list for metis by using an external automated theorem prover +Minimization of theorem list for Metis using automatic theorem provers. *) signature ATP_MINIMAL = sig - val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state -> - (string * thm list) list -> ((string * thm list) list * int) option * string - (* To be removed once TN has finished his measurements; - the int component of the result should then be removed: *) - val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> - (string * thm list) list -> ((string * thm list) list * int) option * string -end + type prover = ATP_Manager.prover + type prover_result = ATP_Manager.prover_result + type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list -structure ATP_Minimal: ATP_MINIMAL = + val linear_minimize : 'a minimize_fun + val binary_minimize : 'a minimize_fun + val minimize_theorems : + (string * thm list) minimize_fun -> prover -> string -> int + -> Proof.state -> (string * thm list) list + -> (string * thm list) list option * string +end; + +structure ATP_Minimal : ATP_MINIMAL = struct -(* Linear minimization *) +open Sledgehammer_Fact_Preprocessor +open ATP_Manager + +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list + +(* Linear minimization algorithm *) -fun lin_gen_minimize p s = -let - fun min [] needed = needed - | min (x::xs) needed = - if p(xs @ needed) then min xs needed else min xs (x::needed) -in (min s [], length s) end; +fun linear_minimize p s = + let + fun aux [] needed = needed + | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x) + in aux s [] end; -(* Clever minimalization algorithm *) +(* Binary minimalization *) local fun isplit (l, r) [] = (l, r) @@ -37,24 +45,21 @@ end local - fun min p sup [] = raise Empty - | min p sup [s0] = [s0] + fun min _ _ [] = raise Empty + | min _ _ [s0] = [s0] | min p sup s = let val (l0, r0) = split s in - if p (sup @ l0) - then min p sup l0 + if p (sup @ l0) then + min p sup l0 + else if p (sup @ r0) then + min p sup r0 else - if p (sup @ r0) - then min p sup r0 - else - let - val l = min p (sup @ r0) l0 - val r = min p (sup @ l) r0 - in - l @ r - end + let + val l = min p (sup @ r0) l0 + val r = min p (sup @ l) r0 + in l @ r end end in (* return a minimal subset v of s that satisfies p @@ -62,15 +67,10 @@ @post v subset s & p(v) & forall e in v. ~p(v \ e) *) - fun minimal p s = - let - val count = Unsynchronized.ref 0 - fun p_count xs = (Unsynchronized.inc count; p xs) - val v = - (case min p_count [] s of - [x] => if p_count [] then [] else [x] - | m => m); - in (v, ! count) end + fun binary_minimize p s = + case min p [] s of + [x] => if p [] then [] else [x] + | m => m end @@ -91,32 +91,31 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer (result: ATP_Wrapper.prover_result) = - let - val {success, proof = result_string, internal_thm_names = thm_name_vec, - filtered_clauses = filtered, ...} = result - in - if success then - (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string) - else - let - val failure = failure_strings |> get_first (fn (s, t) => - if String.isSubstring s result_string then SOME (t, result_string) else NONE) - in - (case failure of - SOME res => res - | NONE => (Failure, result_string)) - end - end +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...} + : prover_result) = + if success then + (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses), + proof) + else + let + val failure = failure_strings |> get_first (fn (s, t) => + if String.isSubstring s proof then SOME (t, proof) else NONE) + in + (case failure of + SOME res => res + | NONE => (Failure, proof)) + end (* wrapper for calling external prover *) -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered + name_thms_pairs = let - val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") + val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ + " theorems... ") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {with_full_types = ! ATP_Manager.full_types, @@ -126,20 +125,19 @@ filtered_clauses = filtered} val (result, proof) = produce_answer (prover time_limit problem) val _ = priority (string_of_result result) - in - (result, proof) - end + in (result, proof) end (* minimalization of thms *) -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs = +fun minimize_theorems gen_min prover prover_name time_limit state + name_thms_pairs = let val _ = priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ " theorems, prover: " ^ prover_name ^ ", time limit: " ^ string_of_int time_limit ^ " seconds") - val test_thms_fun = sh_test_thms prover time_limit 1 state + val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false in @@ -152,15 +150,14 @@ if length ordered_used < length name_thms_pairs then filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val (min_thms, n) = - if null to_use then ([], 0) + val min_thms = + if null to_use then [] else gen_min (test_thms (SOME filtered)) to_use val min_names = sort_distinct string_ord (map fst min_thms) val _ = priority (cat_lines - ["Iterations: " ^ string_of_int n (* FIXME TN remove later *), - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) + ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in - (SOME (min_thms, n), "Try this command: " ^ + (SOME min_thms, "Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) end | (Timeout, _) => @@ -170,68 +167,9 @@ (NONE, "Error in prover: " ^ msg) | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => - (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + handle Sledgehammer_HOL_Clause.TRIVIAL => + (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => (NONE, "Error: " ^ msg) end - -(* Isar command and parsing input *) - -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in - -fun get_thms context = - map (fn (name, interval) => - let - val thmref = Facts.Named ((name, Position.none), interval) - val ths = ProofContext.get_fact context thmref - val name' = Facts.string_of_ref thmref - in - (name', ths) - end) - -val default_prover = "remote_vampire" -val default_time_limit = 5 - -fun get_time_limit_arg time_string = - (case Int.fromString time_string of - SOME t => t - | NONE => error ("Invalid time limit: " ^ quote time_string)) - -fun get_opt (name, a) (p, t) = - (case name of - "time" => (p, get_time_limit_arg a) - | "atp" => (a, t) - | n => error ("Invalid argument: " ^ n)) - -fun get_options args = fold get_opt args (default_prover, default_time_limit) - -val minimize = gen_minimalize lin_gen_minimize - -val minimalize = gen_minimalize minimal - -fun sh_min_command args thm_names state = - let - val (prover_name, time_limit) = get_options args - val prover = - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of - SOME prover => prover - | NONE => error ("Unknown prover: " ^ quote prover_name)) - val name_thms_pairs = get_thms (Proof.context_of state) thm_names - in - writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs)) - end - -val parse_args = - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) - -val _ = - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag - (parse_args -- parse_thm_names >> (fn (args, thm_names) => - Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of))) - -end - -end +end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 13:48:15 2010 +0100 @@ -6,54 +6,24 @@ signature ATP_WRAPPER = sig - (*hooks for problem files*) - val destdir: string Config.T - val problem_prefix: string Config.T - val measure_runtime: bool Config.T - val setup: theory -> theory + type prover = ATP_Manager.prover - (*prover configuration, problem format, and prover result*) - type prover_config = - {command: Path.T, - arguments: int -> string, - max_new_clauses: int, - insert_theory_const: bool, - emit_structured_proof: bool} - type problem = - {with_full_types: bool, - subgoal: int, - goal: Proof.context * (thm list * thm), - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option} - val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem - type prover_result = - {success: bool, - message: string, - theorem_names: string list, - runtime: int, - proof: string, - internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list} - type prover = int -> problem -> prover_result + (* hooks for problem files *) + val destdir : string Config.T + val problem_prefix : string Config.T + val measure_runtime : bool Config.T - (*common provers*) - val vampire: string * prover - val vampire_full: string * prover - val eprover: string * prover - val eprover_full: string * prover - val spass: string * prover - val spass_no_tc: string * prover - val remote_vampire: string * prover - val remote_eprover: string * prover - val remote_spass: string * prover - val refresh_systems: unit -> unit + val refresh_systems_on_tptp : unit -> unit + val setup : theory -> theory 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 +open ATP_Manager (** generic ATP wrapper **) @@ -68,43 +38,17 @@ val (measure_runtime, measure_runtime_setup) = Attrib.config_bool "atp_measure_runtime" false; -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup; - -(* prover configuration, problem format, and prover result *) +(* prover configuration *) 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}; -type problem = - {with_full_types: bool, - subgoal: int, - goal: Proof.context * (thm list * thm), - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option}; - -fun problem_of_goal with_full_types subgoal goal : problem = - {with_full_types = with_full_types, - subgoal = subgoal, - goal = goal, - axiom_clauses = NONE, - filtered_clauses = NONE}; - -type prover_result = - {success: bool, - message: string, - theorem_names: string list, (*relevant theorems*) - runtime: int, (*user time of the ATP, in milliseconds*) - proof: string, - internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list}; - -type prover = int -> problem -> prover_result; - (* basic template *) @@ -114,13 +58,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 +135,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 +151,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,40 +169,51 @@ (*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; -fun vampire_prover_config full : prover_config = +fun vampire_prover_config isar : prover_config = {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}; + emit_structured_proof = isar}; val vampire = tptp_prover ("vampire", vampire_prover_config false); -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true); +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true); (* 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; -fun eprover_config full : prover_config = +fun eprover_config isar : prover_config = {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}; + emit_structured_proof = isar}; val eprover = tptp_prover ("e", eprover_config false); -val eprover_full = tptp_prover ("e_full", eprover_config true); +val eprover_isar = tptp_prover ("e_isar", eprover_config true); (* 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 +221,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); @@ -305,7 +257,8 @@ else split_lines answer end; -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ()); +fun refresh_systems_on_tptp () = + Synchronized.change systems (fn _ => get_systems ()); fun get_system prefix = Synchronized.change_result systems (fn systems => (if null systems then get_systems () else systems) @@ -316,10 +269,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}; @@ -333,4 +289,15 @@ val remote_spass = tptp_prover ("remote_spass", remote_prover_config "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); +val provers = + [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc, + remote_vampire, remote_spass, remote_eprover] +val prover_setup = fold add_prover provers + +val setup = + destdir_setup + #> problem_prefix_setup + #> measure_runtime_setup + #> prover_setup; + end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 13:48:15 2010 +0100 @@ -13,7 +13,7 @@ val auto: bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params val setup : theory -> theory -end +end; structure Nitpick_Isar : NITPICK_ISAR = struct diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 13:48:15 2010 +0100 @@ -12,7 +12,7 @@ hol_context -> (typ option * bool option) list -> (typ option * bool option) list -> term -> term list * term list * bool * bool * bool -end +end; structure Nitpick_Preproc : NITPICK_PREPROC = struct diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 13:48:15 2010 +0100 @@ -8,7 +8,7 @@ signature NITPICK_TESTS = sig val run_all_tests : unit -> unit -end +end; structure Nitpick_Tests = struct diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 13:48:15 2010 +0100 @@ -62,7 +62,7 @@ val pstrs : string -> Pretty.T list val unyxml : string -> string val maybe_quote : string -> string -end +end; structure Nitpick_Util : NITPICK_UTIL = struct diff -r 3122bdd95275 -r 5ed2e9a545ac 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 Mon Mar 22 13:48:15 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 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Mar 22 13:48:15 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 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 13:48:15 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 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 13:48:15 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,49 +458,13 @@ 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 = EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]; -val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf; +val neg_clausify = + Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf; fun neg_conjecture_clauses ctxt st0 n = let @@ -534,11 +501,9 @@ "conversion of theorem to clauses"; - (** setup **) val setup = - meson_method_setup #> neg_clausify_setup #> clausify_setup #> perhaps saturate_skolem_cache #> diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 22 13:48:15 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 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 13:48:15 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 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 22 13:48:15 2010 +0100 @@ -0,0 +1,87 @@ +(* Title: HOL/Sledgehammer/sledgehammer_isar.ML + Author: Jasmin Blanchette, TU Muenchen + +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. +*) + +structure Sledgehammer_Isar : sig end = +struct + +open ATP_Manager +open ATP_Minimal + +structure K = OuterKeyword and P = OuterParse + +val _ = + OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); + +val _ = + OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)); + +val _ = + OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag + (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> + (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit))); + +val _ = + OuterSyntax.improper_command "print_atps" "print external provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (print_provers o Toplevel.theory_of))); + +val _ = + OuterSyntax.command "sledgehammer" + "search for first-order proof using automatic theorem provers" K.diag + (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o + Toplevel.keep (sledgehammer names o Toplevel.proof_of))); + +val default_minimize_prover = "remote_vampire" +val default_minimize_time_limit = 5 + +fun atp_minimize_command args thm_names state = + let + fun theorems_from_names ctxt = + map (fn (name, interval) => + let + val thmref = Facts.Named ((name, Position.none), interval) + val ths = ProofContext.get_fact ctxt thmref + val name' = Facts.string_of_ref thmref + in (name', ths) end) + fun get_time_limit_arg time_string = + (case Int.fromString time_string of + SOME t => t + | NONE => error ("Invalid time limit: " ^ quote time_string)) + fun get_opt (name, a) (p, t) = + (case name of + "time" => (p, get_time_limit_arg a) + | "atp" => (a, t) + | n => error ("Invalid argument: " ^ n)) + fun get_options args = + fold get_opt args (default_minimize_prover, default_minimize_time_limit) + val (prover_name, time_limit) = get_options args + val prover = + (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of + SOME prover => prover + | NONE => error ("Unknown prover: " ^ quote prover_name)) + val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names + in + writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit + state name_thms_pairs)) + end + +local structure K = OuterKeyword and P = OuterParse in + +val parse_args = + Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) + +val _ = + OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag + (parse_args -- parse_thm_names >> (fn (args, thm_names) => + Toplevel.no_timing o Toplevel.unknown_proof o + Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of))) + +end + +end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 13:48:15 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 - -val trace_path = Path.basic "atp_trace"; +open Sledgehammer_FOL_Clause +open Sledgehammer_Fact_Preprocessor -fun trace s = - if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s - else (); +val trace_proof_path = Path.basic "atp_trace"; + +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; @@ -340,26 +333,30 @@ then SOME ctm else perm ctms in perm end; -fun have_or_show "show " _ = "show \"" - | have_or_show have lname = have ^ lname ^ ": \"" - (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the 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") - 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" - | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*) - | doline have (lname, t, deps) = - have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^ - "\"\n by (metis " ^ space_implode " " deps ^ ")\n" - fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)] - | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines - in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end; +fun isar_proof_body ctxt ctms = + let + val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") + val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt) + fun have_or_show "show" _ = "show \"" + | have_or_show have lname = have ^ " " ^ lname ^ ": \"" + fun do_line _ (lname, t, []) = + (* No deps: it's a conjecture clause, with no proof. *) + (case permuted_clause t ctms of + SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" + | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", + [t])) + | do_line have (lname, t, deps) = + have_or_show have lname ^ + string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^ + "\"\n by (metis " ^ space_implode " " deps ^ ")\n" + fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] + | do_lines ((lname, t, deps) :: lines) = + do_line "have" (lname, t, deps) :: do_lines lines + in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end; -fun notequal t (_,t',_) = not (t aconv t'); +fun unequal t (_, t', _) = not (t aconv t'); (*No "real" literals means only type information*) fun eq_types t = t aconv HOLogic.true_const; @@ -375,7 +372,7 @@ if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*) then map (replace_deps (lno, [])) lines else - (case take_prefix (notequal t) lines of + (case take_prefix (unequal t) lines of (_,[]) => lines (*no repetition of proof line*) | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) pre @ map (replace_deps (lno', [lno])) post) @@ -385,7 +382,7 @@ if eq_types t then (lno, t, deps) :: lines (*Type information will be deleted later; skip repetition test.*) else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) - case take_prefix (notequal t) lines of + case take_prefix (unequal t) lines of (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) | (pre, (lno', t', _) :: post) => (lno, t', deps) :: (*repetition: replace later line by earlier one*) @@ -399,7 +396,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. @@ -435,39 +432,42 @@ fun isar_header [] = proofstart | 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" - val tuples = map (dest_tstp o tstp_line o explode) cnfs - val _ = trace (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 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 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 ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) - val _ = trace "\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?)"; +fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names = + let + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") + val tuples = map (dest_tstp o tstp_line o explode) cnfs + 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_proof_msg (fn () => + Int.toString (length raw_lines) ^ " raw_lines extracted\n") + val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines + 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 _ = app (fn th => trace_proof_msg + (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls + val body = isar_proof_body ctxt (map prop_of ccls) + (stringify_deps thm_names [] lines) + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") + in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end + handle STREE _ => error "Could not extract proof (ATP output malformed?)"; (*=== 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 +475,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 +484,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 +515,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 ^ ")" @@ -555,34 +541,37 @@ (* atp_minimize [atp=] *) 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)) - -fun sendback_metis_nochained lemmas = - (Markup.markup Markup.sendback o metis_line) (nochained lemmas) + Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ + space_implode " " (kill_chained lemmas)) -fun 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) +fun metis_lemma_list dfg name result = + let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in + (Markup.markup Markup.sendback (metis_line (kill_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 tokens = String.tokens (fn c => c = #" ") one_line_proof + val isar_proof = + if member (op =) tokens chained_hint then "" + else isar_proof_from_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 isar_proof, + lemma_names) + end end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Mar 22 13:48:15 2010 +0100 @@ -22,7 +22,6 @@ val global_setup: theory -> theory val split_limit: int Config.T val neq_limit: int Config.T - val warning_count: int Unsynchronized.ref val trace: bool Unsynchronized.ref end; @@ -797,7 +796,6 @@ fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; val lin_arith_tac = Fast_Arith.lin_arith_tac; val trace = Fast_Arith.trace; -val warning_count = Fast_Arith.warning_count; (* reduce contradictory <= to False. Most of the work is done by the cancel tactics. *) diff -r 3122bdd95275 -r 5ed2e9a545ac src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/meson.ML Mon Mar 22 13:48:15 2010 +0100 @@ -18,6 +18,7 @@ val make_nnf: Proof.context -> thm -> thm val skolemize: Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool + val make_clauses_unsorted: thm list -> thm list val make_clauses: thm list -> thm list val make_horns: thm list -> thm list val best_prolog_tac: (thm -> int) -> thm list -> tactic @@ -560,7 +561,8 @@ (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) -fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []); +fun make_clauses_unsorted ths = fold_rev add_clauses ths []; +val make_clauses = sort_clauses o make_clauses_unsorted; (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) fun make_horns ths = diff -r 3122bdd95275 -r 5ed2e9a545ac src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 13:48:15 2010 +0100 @@ -96,7 +96,6 @@ number_of : serial * (theory -> typ -> int -> cterm)}) -> Context.generic -> Context.generic val trace: bool Unsynchronized.ref - val warning_count: int Unsynchronized.ref; end; functor Fast_Lin_Arith @@ -426,9 +425,6 @@ fun trace_msg msg = if !trace then tracing msg else (); -val warning_count = Unsynchronized.ref 0; -val warning_count_max = 10; - val union_term = union Pattern.aeconv; val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')); @@ -532,17 +528,11 @@ val _ = if LA_Logic.is_False fls then () else - let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in - if count > warning_count_max then () - else - (tracing (cat_lines - (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @ - ["Proved:", Display.string_of_thm ctxt fls, ""] @ - (if count <> warning_count_max then [] - else ["\n(Reached maximal message count -- disabling future warnings)"]))); - warning "Linear arithmetic should have refuted the assumptions.\n\ - \Please inform Tobias Nipkow (nipkow@in.tum.de).") - end; + (tracing (cat_lines + (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @ + ["Proved:", Display.string_of_thm ctxt fls, ""])); + warning "Linear arithmetic should have refuted the assumptions.\n\ + \Please inform Tobias Nipkow.") in fls end handle FalseE thm => trace_thm ctxt "False reached early:" thm end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/Pure/Isar/class_target.ML Mon Mar 22 13:48:15 2010 +0100 @@ -16,12 +16,13 @@ val rules: theory -> class -> thm option * thm val these_params: theory -> sort -> (string * (class * (string * typ))) list val these_defs: theory -> sort -> thm list - val these_operations: theory -> sort -> (string * (class * (typ * term))) list + val these_operations: theory -> sort + -> (string * (class * (typ * term))) list val print_classes: theory -> unit val begin: class list -> sort -> Proof.context -> Proof.context val init: class -> theory -> Proof.context - val declare: class -> (binding * mixfix) * term -> theory -> theory + val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory val class_prefix: string -> string val refresh_syntax: class -> Proof.context -> Proof.context @@ -253,8 +254,8 @@ (* class context syntax *) -fun these_unchecks thy = - map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy; +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) + o these_operations thy; fun redeclare_const thy c = let val b = Long_Name.base_name c @@ -317,15 +318,15 @@ val class_prefix = Logic.const_of_class o Long_Name.base_name; -fun declare class ((c, mx), dict) thy = +fun declare class ((c, mx), (type_params, dict)) thy = let val morph = morphism thy class; val b = Morphism.binding morph c; val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); val c' = Sign.full_name thy b; val dict' = Morphism.term morph dict; - val ty' = Term.fastype_of dict'; - val def_eq = Logic.mk_equals (Const (c', ty'), dict') + val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; + val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') |> map_types Type.strip_sorts; in thy @@ -335,7 +336,7 @@ |>> Thm.varifyT_global |-> (fn def_thm => PureThy.store_thm (b_def, def_thm) #> snd - #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) + #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) |> Sign.add_const_constraint (c', SOME ty') end; diff -r 3122bdd95275 -r 5ed2e9a545ac src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/Pure/Isar/overloading.ML Mon Mar 22 13:48:15 2010 +0100 @@ -13,7 +13,7 @@ val define: bool -> binding -> string * term -> theory -> thm * theory val operation: Proof.context -> binding -> (string * bool) option val pretty: Proof.context -> Pretty.T - + type improvable_syntax val add_improvable_syntax: Proof.context -> Proof.context val map_improvable_syntax: (improvable_syntax -> improvable_syntax) diff -r 3122bdd95275 -r 5ed2e9a545ac src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/Pure/Isar/theory_target.ML Mon Mar 22 13:48:15 2010 +0100 @@ -277,7 +277,7 @@ in lthy' |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) - |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t)) + |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t))) |> Local_Defs.add_def ((b, NoSyn), t) end;