--- 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,
--- 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
--- 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 *)
--- 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 =
--- 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;
--- 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