# HG changeset patch # User paulson # Date 1126178659 -7200 # Node ID 159783c74f75e362db925041c8d74b4b92ce7ed7 # Parent 5b1d47d920ce02d4bba3387518ae2ac2135c8f78 yet more tidying of Isabelle-ATP link diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Thu Sep 08 13:24:19 2005 +0200 @@ -33,7 +33,7 @@ [rtac ccontr, ResLib.atomize_tac, skolemize_tac, METAHYPS(fn negs => (Recon_Transfer.vampString_to_lemmaString proofextract thmstring - goalstring toParent ppid negs clause_arr num_of_clauses ))]) sg_num + goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Sep 08 13:24:19 2005 +0200 @@ -23,8 +23,6 @@ fun numlist 0 = [] | numlist n = (numlist (n - 1))@[n] - -fun last(x::xs) = if xs=[] then x else last xs fun butlast []= [] | butlast(x::xs) = if xs=[] then [] else (x::(butlast xs)) @@ -44,7 +42,7 @@ fun contains_eq str = "=" mem str fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str []) - in (last uptoeq) <> "~" end + in (List.last uptoeq) <> "~" end fun get_eq_strs str = if eq_not_neq str (*not an inequality *) then diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Sep 08 13:24:19 2005 +0200 @@ -25,8 +25,6 @@ (* Parser combinators *) exception Noparse; -exception VampError of string; - fun (parser1 ++ parser2) input = let @@ -158,53 +156,18 @@ fun lex s = alltokens (explode s) -(*********************************************************) -(* Temporary code to "parse" Vampire proofs *) -(*********************************************************) -fun num_int (Number n) = n -| num_int _ = raise VampError "Not a number" - - fun takeUntil ch [] res = (res, []) - | takeUntil ch (x::xs) res = if x = ch - then - (res, xs) - else - takeUntil ch xs (res@[x]) - -fun linenums [] nums = nums -| linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) [] - in - if rest = [] - then - nums - else - let val first = hd rest - - in - if (first = (Other "*") ) - then - - linenums rest ((num_int (hd (tl rest)))::nums) - else - linenums rest ((num_int first)::nums) - end - end +(*String contains multiple lines, terminated with newline characters. + A list consisting of the first number in each line is returned. *) +fun get_linenums proofstr = + let val numerics = String.tokens (not o Char.isDigit) + fun firstno [] = NONE + | firstno (x::xs) = Int.fromString x + val lines = String.tokens (fn c => c = #"\n") proofstr + in List.mapPartial (firstno o numerics) lines end -(* This relies on a Vampire proof line starting "% Number" or "% * Number"*) -(* Check this is right *) - -fun get_linenums proofstr = let (*val s = extract_proof proofstr*) - val tokens = #1(lex proofstr) - - in - rev (linenums tokens []) - end - (************************************************************) -(************************************************************) - (**************************************************) (* Code to parse SPASS proofs *) diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 08 13:24:19 2005 +0200 @@ -3,10 +3,6 @@ Copyright 2004 University of Cambridge *) -(******************) -(* complete later *) -(******************) - structure Recon_Transfer = struct @@ -104,10 +100,8 @@ extraAxs_to_string xs (str^newstr) end; -fun is_axiom ( num:int,Axiom, str) = true -| is_axiom (num, _,_) = false - -fun get_init_axioms xs = List.filter (is_axiom) ( xs) +fun is_axiom (_,Axiom,str) = true +| is_axiom (_,_,_) = false fun get_step_nums [] nums = nums | get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num]) @@ -159,23 +153,22 @@ (* retrieve the axioms that were obtained from the clasimpset *) -fun get_clasimp_cls clause_arr clasimp_num step_nums = +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = let val realnums = map subone step_nums val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums (* val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums"))) val _ = TextIO.output(axnums,(numstr clasimp_nums)) val _ = TextIO.closeOut(axnums)*) in - retrieve_axioms clause_arr clasimp_nums + retrieve_axioms clause_arr clasimp_nums end - (*****************************************************) (* get names of clasimp axioms used *) (*****************************************************) - fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses = + fun get_axiom_names step_nums thms clause_arr num_of_clauses = let (* not sure why this is necessary again, but seems to be *) val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) @@ -184,7 +177,7 @@ (* here need to add the clauses from clause_arr*) (***********************************************) - val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums + val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls val _ = File.write (File.tmp_path (Path.basic "clasimp_names")) @@ -195,7 +188,7 @@ end fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses = - get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) + get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) thms clause_arr num_of_clauses; fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses = @@ -217,7 +210,7 @@ fun get_axioms_used proof_steps thms clause_arr num_of_clauses = let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val axioms = get_init_axioms proof_steps + val axioms = (List.filter is_axiom) proof_steps val step_nums = get_step_nums axioms [] val clauses =(*(clasimp_cls)@*)( make_clauses thms) @@ -322,9 +315,7 @@ let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" in TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" ); - TextIO.flushOut toParent; TextIO.output (toParent, (remove_linebreaks thmstring)^"\n"); - TextIO.flushOut toParent; TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n")); TextIO.flushOut toParent; Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); @@ -343,11 +334,12 @@ (* get vampire axiom names *) (***********************************) - val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses + val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^ rules_to_string axiom_names in - File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring); + File.append(File.tmp_path (Path.basic "reconstrfile")) + ("reconstring is: "^ax_str^" "^goalstring); TextIO.output (toParent, ax_str^"\n"); TextIO.output (toParent, "goalstring: "^goalstring^"\n"); TextIO.output (toParent, "thmstring: "^thmstring^"\n"); @@ -383,9 +375,10 @@ val ax_str = "Rules from clasimpset used in proof found by E: " ^ rules_to_string axiom_names in - File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring); + File.append(File.tmp_path (Path.basic "reconstrfile")) + ("reconstring is: "^ax_str^" "^goalstring); TextIO.output (toParent, ax_str^"\n"); - TextIO.flushOut toParent; + TextIO.output (toParent, "goalstring: "^goalstring^"\n"); TextIO.output (toParent, "thmstring: "^thmstring^"\n"); TextIO.flushOut toParent; @@ -771,7 +764,7 @@ val steps = Library.drop (origax_num, axioms_and_steps) val firststeps = ReconOrderClauses.butlast steps - val laststep = ReconOrderClauses.last steps + val laststep = List.last steps val goalstring = implode(ReconOrderClauses.butlast(explode goalstring)) val isar_proof = diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Sep 08 13:24:19 2005 +0200 @@ -259,25 +259,6 @@ end handle Option => reconstruction_failed "follow_standard_para" -(* -fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= - let - val th1 = valOf (assoc (thml,clause1)) - val th2 = valOf (assoc (thml,clause2)) - val eq_lit_th = select_literal (lit1+1) th1 - val mod_lit_th = select_literal (lit2+1) th2 - val eqsubst = eq_lit_th RSN (2,rev_subst) - val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) - val newth' =negate_nead newth - val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars) - val thmvars = thm_vars res - in - (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) - end - handle Option => reconstruction_failed "follow_standard_para" - -*) - (********************************) (* Reconstruct a rewriting step *) @@ -401,22 +382,6 @@ (* follow through the res. proof, creating an Isabelle theorem *) (***************************************************************) - - -(*fun is_proof_char ch = (case ch of - - "(" => true - | ")" => true - | ":" => true - | "'" => true - | "&" => true - | "|" => true - | "~" => true - | "." => true - |(is_alpha ) => true - |(is_digit) => true - | _ => false)*) - fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ") fun proofstring x = let val exp = explode x @@ -424,35 +389,6 @@ List.filter (is_proof_char ) exp end - -(* - -fun follow clauses [] allvars thml recons = - let (* val _ = reset show_sorts*) - val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml)) - val thmproofstring = proofstring ( thmstring) - val no_returns = no_lines thmproofstring - val thmstr = implode no_returns - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file"))) - val _ = TextIO.output(outfile, "thmstr is "^thmstr) - val _ = TextIO.flushOut outfile; - val _ = TextIO.closeOut outfile - (*val _ = set show_sorts*) - in - ((snd( hd thml)), recons) - end - | follow clauses (h::t) allvars thml recons - = let - val (thml', recons') = follow_line clauses allvars thml h recons - val (thm, recons_list) = follow clauses t allvars thml' recons' - - - in - (thm,recons_list) - end - -*) - fun replace_clause_strs [] recons newrecons = (newrecons) | replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = @@ -477,17 +413,11 @@ (thm,recons_list) end - - (* Assume we have the cnf clauses as a list of (clauseno, clause) *) (* and the proof as a list of the proper datatype *) (* take the cnf clauses of the goal and the proof from the res. prover *) (* as a list of type Proofstep and return the thm goal ==> False *) -fun first_pair (a,b,c) = (a,b); - -fun second_pair (a,b,c) = (b,c); - (* takes original axioms, proof_steps parsed from spass, variables *) fun translate_proof clauses proof allvars @@ -496,10 +426,4 @@ (thm, (recons)) end - - -fun remove_tinfo [] = [] - | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = - (clausenum, step , newstrs)::(remove_tinfo xs) - end; diff -r 5b1d47d920ce -r 159783c74f75 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Sep 07 21:07:09 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Thu Sep 08 13:24:19 2005 +0200 @@ -448,20 +448,9 @@ (sorts_on_typs ((FOLTFree x), ss)); -(*FIXME: duplicate code that needs removal??*) - -fun takeUntil ch [] res = (res, []) - | takeUntil ch (x::xs) res = if x = ch - then - (res, xs) - else - takeUntil ch xs (res@[x]) - -fun remove_type str = let val exp = explode str - val (first,rest) = (takeUntil "(" exp []) - in - implode first - end +(*UGLY: seems to be parsing the "show sorts" output, removing anything that + starts with a left parenthesis.*) +fun remove_type str = hd (String.fields (fn c => c = #"(") str); fun pred_of_sort (LTVar x) = ((remove_type x),1) | pred_of_sort (LTFree x) = ((remove_type x),1) @@ -487,22 +476,6 @@ (vss, ResLib.no_rep_app fs fss,preds'') end; - -(*fun add_typs_aux [] = ([],[]) - | add_typs_aux ((FOLTVar indx,s)::tss) = - let val vs = sorts_on_typs (FOLTVar indx, s) - val (vss,fss) = add_typs_aux tss - in - (ResLib.no_rep_app vs vss, fss) - end - | add_typs_aux ((FOLTFree x,s)::tss) = - let val fs = sorts_on_typs (FOLTFree x, s) - val (vss,fss) = add_typs_aux tss - in - (vss, ResLib.no_rep_app fs fss) - end;*) - - fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds