# HG changeset patch # User paulson # Date 1187957804 -7200 # Node ID ca97c6f3d9cdf97e6e1b7d4dbee101f4d1c2e752 # Parent 90500d3b5b5dcf6eea708515e006e5cdb2fbfdfd Returning both a "one-line" proof and a structured proof diff -r 90500d3b5b5d -r ca97c6f3d9cd src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Aug 24 14:15:58 2007 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Aug 24 14:16:44 2007 +0200 @@ -7,7 +7,7 @@ signature RES_ATP = sig - val prover: string ref + val prover: ResReconstruct.atp ref val destdir: string ref val helper_path: string -> string -> string val problem_name: string ref @@ -45,6 +45,8 @@ structure ResAtp: RES_ATP = struct +structure Recon = ResReconstruct; + fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s)); (********************************************************************) @@ -55,7 +57,7 @@ (*** background linkup ***) val run_blacklist_filter = ref true; val time_limit = ref 60; -val prover = ref ""; +val prover = ref Recon.E; (*** relevance filter parameters ***) val run_relevance_filter = ref true; @@ -70,15 +72,15 @@ "e" => (max_new := 100; theory_const := false; - prover := "E") + prover := Recon.E) | "spass" => (max_new := 40; theory_const := true; - prover := "spass") + prover := Recon.SPASS) | "vampire" => (max_new := 60; theory_const := false; - prover := "vampire") + prover := Recon.Vampire) | _ => error ("No such prover: " ^ atp); val _ = set_prover "E"; (* use E as the default prover *) @@ -822,30 +824,26 @@ in Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile); (*options are separated by Watcher.setting_sep, currently #"%"*) - if !prover = "spass" - then - let val spass = helper_path "SPASS_HOME" "SPASS" - val sopts = - "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time - in - ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1) - end - else if !prover = "vampire" - then - let val vampire = helper_path "VAMPIRE_HOME" "vampire" - val vopts = "--mode casc%-t " ^ time (*what about -m 100000?*) - in - ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1) - end - else if !prover = "E" - then - let val Eprover = helper_path "E_HOME" "eproof" - in - ("E", Eprover, - "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: - make_atp_list xs (n+1) - end - else error ("Invalid prover name: " ^ !prover) + case !prover of + Recon.SPASS => + let val spass = helper_path "SPASS_HOME" "SPASS" + val sopts = + "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time + in + ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1) + end + | Recon.Vampire => + let val vampire = helper_path "VAMPIRE_HOME" "vampire" + val vopts = "--mode casc%-t " ^ time (*what about -m 100000?*) + in + ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1) + end + | Recon.E => + let val eproof = helper_path "E_HOME" "eproof" + val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time + in + ("E", eproof, eopts, probfile) :: make_atp_list xs (n+1) + end end val atp_list = make_atp_list sg_terms 1 @@ -885,7 +883,7 @@ val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) axcls_list - val writer = if !prover = "spass" then dfg_writer else tptp_writer + val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer fun write_all [] [] _ = [] | write_all (ccls::ccls_list) (axcls::axcls_list) k = let val fname = probfile k diff -r 90500d3b5b5d -r ca97c6f3d9cd src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri Aug 24 14:15:58 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Fri Aug 24 14:16:44 2007 +0200 @@ -7,22 +7,30 @@ (* Code to deal with the transfer of proofs from a prover process *) (***************************************************************************) signature RES_RECONSTRUCT = - sig - val checkEProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * Proof.context * thm * int * string Vector.vector -> bool - val checkVampProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * Proof.context * thm * int * string Vector.vector -> bool - val checkSpassProofFound: - TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * Proof.context * thm * int * string Vector.vector -> bool - val signal_parent: - TextIO.outstream * Posix.Process.pid * string * string -> unit +sig + datatype atp = E | SPASS | Vampire + val modulus: int ref + val recon_sorts: bool ref + val checkEProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * Proof.context * thm * int * string Vector.vector -> bool + val checkVampProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * Proof.context * thm * int * string Vector.vector -> bool + val checkSpassProofFound: + TextIO.instream * TextIO.outstream * Posix.Process.pid * + string * Proof.context * thm * int * string Vector.vector -> bool + val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit + val txt_path: string -> Path.T + val fix_sorts: sort Vartab.table -> term -> term + val invert_const: string -> string + val invert_type_const: string -> string + val num_typargs: Context.theory -> string -> int + val make_tvar: string -> typ + val strip_prefix: string -> string -> string option +end; - end; - -structure ResReconstruct = +structure ResReconstruct : RES_RECONSTRUCT = struct val trace_path = Path.basic "atp_trace"; @@ -30,8 +38,7 @@ fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s else (); -(*Full proof reconstruction wanted*) -val full = ref true; +datatype atp = E | SPASS | Vampire; val recon_sorts = ref true; @@ -467,13 +474,6 @@ OS.Process.sleep (Time.fromMilliseconds 600) end; -fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names = - let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - in - signal_success probfile toParent ppid - (decode_tstp_file cnfs ctxt th sgno thm_names) - end; - (**** retrieve the axioms that were used in the proof ****) @@ -491,15 +491,15 @@ (*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. *) -fun get_spass_linenums proofstr = +fun get_spass_linenums proofextract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok | inputno _ = NONE - val lines = String.tokens (fn c => c = #"\n") proofstr + val lines = String.tokens (fn c => c = #"\n") proofextract in List.mapPartial (inputno o toks) lines end -fun get_axiom_names_spass proofstr thm_names = - get_axiom_names thm_names (get_spass_linenums proofstr); +fun get_axiom_names_spass proofextract thm_names = + get_axiom_names thm_names (get_spass_linenums proofextract); fun not_comma c = c <> #","; @@ -516,47 +516,43 @@ in Int.fromString ints end handle Fail _ => NONE; -fun get_axiom_names_tstp proofstr thm_names = - get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr)); +fun get_axiom_names_tstp proofextract thm_names = + get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract)); (*String contains multiple lines. We want those of the form "*********** [448, input] ***********". A list consisting of the first number in each line is returned. *) -fun get_vamp_linenums proofstr = +fun get_vamp_linenums proofextract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno [ntok,"input"] = Int.fromString ntok | inputno _ = NONE - val lines = String.tokens (fn c => c = #"\n") proofstr + val lines = String.tokens (fn c => c = #"\n") proofextract in List.mapPartial (inputno o toks) lines end -fun get_axiom_names_vamp proofstr thm_names = - get_axiom_names thm_names (get_vamp_linenums proofstr); +fun get_axiom_names_vamp proofextract thm_names = + get_axiom_names thm_names (get_vamp_linenums proofextract); + +fun get_axiom_names E = get_axiom_names_tstp + | get_axiom_names SPASS = get_axiom_names_spass + | get_axiom_names Vampire = get_axiom_names_vamp; fun rules_to_metis [] = "metis" | rules_to_metis xs = "(metis " ^ space_implode " " xs ^ ")" +fun metis_line atp proofextract thm_names = + "apply " ^ rules_to_metis (get_axiom_names atp proofextract thm_names); (*The signal handler in watcher.ML must be able to read the output of this.*) -fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = - (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^ - " num of clauses is " ^ string_of_int (Vector.length thm_names)); - signal_success probfile toParent ppid - ("apply " ^ rules_to_metis (getax proofstr thm_names)) - ) - handle e => (*FIXME: exn handler is too general!*) - (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e); - TextIO.output (toParent, "Translation failed for the proof: " ^ - String.toString proofstr ^ "\n"); - TextIO.output (toParent, probfile); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); +fun lemma_list atp proofextract thm_names probfile toParent ppid = + signal_success probfile toParent ppid (metis_line atp proofextract thm_names); -val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp; - -val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp; - -val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass; - +fun tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno = + let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) + val line1 = metis_line atp proofextract thm_names + in + signal_success probfile toParent ppid + (line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names) + end; (**** Extracting proofs from an ATP's output ****) @@ -592,16 +588,22 @@ | SOME thisLine => if String.isPrefix endS thisLine then let val proofextract = currentString ^ cut_before endS thisLine - val lemma_list = if endS = end_V8 then vamp_lemma_list - else if endS = end_SPASS then spass_lemma_list - else e_lemma_list + val atp = if endS = end_V8 then Vampire + else if endS = end_SPASS then SPASS + else E in trace ("\nExtracted proof:\n" ^ proofextract); - if !full andalso String.isPrefix "cnf(" proofextract - then tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names - else lemma_list proofextract probfile toParent ppid thm_names; + if String.isPrefix "cnf(" proofextract + then tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno + else lemma_list atp proofextract thm_names probfile toParent ppid; true end + handle e => (*FIXME: exn handler is too general!*) + (trace ("\nstartTransfer: In exception handler: " ^ Toplevel.exn_message e); + TextIO.output (toParent, "Translation failed\n" ^ probfile); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + true) else transferInput (currentString^thisLine)) in transferInput "" diff -r 90500d3b5b5d -r ca97c6f3d9cd src/HOL/Tools/watcher.ML --- a/src/HOL/Tools/watcher.ML Fri Aug 24 14:15:58 2007 +0200 +++ b/src/HOL/Tools/watcher.ML Fri Aug 24 14:16:44 2007 +0200 @@ -360,12 +360,14 @@ (*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*) fun report_success i s sgtx = - let val lines = String.tokens (fn c => c = #"\n") s - in if length lines > 1 then report i (s ^ sgtx) (*multiple commands: do the old way*) - else priority (cat_lines ["Subgoal " ^ string_of_int i ^ ":", sgtx, - " Try this command:", Markup.enclose Markup.sendback s]) - end; - + let val sgline = "Subgoal " ^ string_of_int i ^ ":" + val outlines = + case split_lines s of + [] => ["Received bad string: " ^ s] + | line::lines => [" Try this command:", (*Markup.enclose Markup.sendback*) line, ""] + @ lines + in priority (cat_lines (sgline::sgtx::outlines)) end; + fun createWatcher (ctxt, th, thm_names_list) = let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list) fun decr_watched() =