--- a/src/HOL/IsaMakefile Thu Sep 28 16:01:34 2006 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 28 16:01:48 2006 +0200
@@ -100,11 +100,7 @@
ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \
Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML \
Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \
- Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
- Tools/ATP/recon_transfer_proof.ML \
- Tools/ATP/reduce_axiomsN.ML \
- Tools/ATP/recon_translate_proof.ML \
- Tools/ATP/watcher.ML \
+ Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
Tools/cnf_funcs.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
Tools/datatype_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.ML \
--- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 28 16:01:34 2006 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 28 16:01:48 2006 +0200
@@ -9,7 +9,6 @@
(***************************************************************************)
signature ATP_COMMUNICATION =
sig
- val reconstruct : bool ref
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
string * string Array.array -> bool
@@ -26,9 +25,6 @@
structure AtpCommunication : ATP_COMMUNICATION =
struct
-(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
-val reconstruct = ref false;
-
val trace_path = Path.basic "atp_trace";
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
@@ -36,6 +32,128 @@
exception EOF;
+
+(**** retrieve the axioms that were used in the proof ****)
+
+(*Get names of axioms used. Axioms are indexed from 1, while the array is indexed from 0*)
+fun get_axiom_names (names_arr: string array) step_nums =
+ let fun is_axiom n = n <= Array.length names_arr
+ fun index i = Array.sub(names_arr, i-1)
+ val axnums = List.filter is_axiom step_nums
+ val axnames = sort_distinct string_ord (map index axnums)
+ in
+ if length axnums = length step_nums then "UNSOUND!!" :: axnames
+ else axnames
+ 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. *)
+fun get_spass_linenums proofstr =
+ 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
+ in List.mapPartial (inputno o toks) lines end
+
+fun get_axiom_names_spass proofstr names_arr =
+ get_axiom_names names_arr (get_spass_linenums proofstr);
+
+ (*String contains multiple lines. We want those of the form
+ "number : ...: ...: initial..." *)
+fun get_e_linenums proofstr =
+ let val fields = String.fields (fn c => c = #":")
+ val nospaces = String.translate (fn c => if c = #" " then "" else str c)
+ fun initial s = String.isPrefix "initial" (nospaces s)
+ fun firstno (line :: _ :: _ :: rule :: _) =
+ if initial rule then Int.fromString line else NONE
+ | firstno _ = NONE
+ val lines = String.tokens (fn c => c = #"\n") proofstr
+ in List.mapPartial (firstno o fields) lines end
+
+fun get_axiom_names_e proofstr names_arr =
+ get_axiom_names names_arr (get_e_linenums proofstr);
+
+ (*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 =
+ 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
+ in List.mapPartial (inputno o toks) lines end
+
+fun get_axiom_names_vamp proofstr names_arr =
+ get_axiom_names names_arr (get_vamp_linenums proofstr);
+
+fun rules_to_string [] = "NONE"
+ | rules_to_string xs = space_implode " " xs
+
+
+(*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 names_arr =
+ let val _ = trace
+ ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
+ "\nprobfile is " ^ probfile ^
+ " num of clauses is " ^ string_of_int (Array.length names_arr))
+ val axiom_names = getax proofstr names_arr
+ val ax_str = rules_to_string axiom_names
+ in
+ trace ("\nDone. Lemma list is " ^ ax_str);
+ TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
+ ax_str ^ "\n");
+ TextIO.output (toParent, probfile ^ "\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
+ end
+ handle exn => (*FIXME: exn handler is too general!*)
+ (trace ("\nprover_lemma_list_aux: In exception handler: " ^
+ Toplevel.exn_message exn);
+ 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));
+
+val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
+
+val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
+
+val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
+
+
+(**** Cutting lines of text FIXME: TIDY UP|!! ****)
+
+exception NOCUT
+fun remove_prefix [] l = l
+ | remove_prefix (h::t) [] = error "can't remove prefix"
+ | remove_prefix (h::t) (h'::t') = remove_prefix t t'
+fun ccut t [] = raise NOCUT
+ | ccut t s =
+ if is_prefix (op =) t s then ([], remove_prefix t s) else
+ let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
+fun cut t s =
+ let
+ val t' = explode t
+ val s' = explode s
+ val (a, b) = ccut t' s'
+ in
+ (implode a, implode b)
+ end
+
+fun cut_exists t s
+ = let val (a, b) = cut t s in true end handle NOCUT => false
+
+fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
+fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
+
+fun kill_lines 0 = Library.I
+ | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
+
+
+(**** Extracting proofs from an ATP's output ****)
+
val start_E = "# Proof object starts here."
val end_E = "# Proof object ends here."
val start_V6 = "%================== Proof: ======================"
@@ -44,7 +162,6 @@
val end_V8 = "======= End of refutation ======="
(*Identifies the start/end lines of an ATP's output*)
-local open Recon_Parse in
fun extract_proof s =
if cut_exists "Formulae used in the proof" s then (*SPASS*)
(kill_lines 0
@@ -56,7 +173,6 @@
(kill_lines 0 (*eproof*)
o fst o cut_before end_E) s
else "??extract_proof failed" (*Couldn't find a proof*)
-end;
(*********************************************************************************)
@@ -75,8 +191,8 @@
else if String.isPrefix endS thisLine
then let val proofextract = extract_proof (currentString^thisLine)
val lemma_list = if endS = end_V8
- then Recon_Transfer.vamp_lemma_list
- else Recon_Transfer.e_lemma_list
+ then vamp_lemma_list
+ else e_lemma_list
in
trace ("\nExtracted proof:\n" ^ proofextract);
lemma_list proofextract probfile toParent ppid names_arr
@@ -136,21 +252,6 @@
checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
end
-
-(**********************************************************************)
-(* Reconstruct the Spass proof w.r.t. thmstring (string version of *)
-(* Isabelle goal to be proved), then transfer the reconstruction *)
-(* steps as a string to the input pipe of the main Isabelle process *)
-(**********************************************************************)
-
-fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num names_arr =
- SELECT_GOAL
- (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac,
- METAHYPS(fn negs =>
- Recon_Transfer.spass_reconstruct proofextract probfile
- toParent ppid negs names_arr)]) sg_num;
-
-
fun transferSpassInput (fromChild, toParent, ppid, probfile,
currentString, thm, sg_num, names_arr) =
let val thisLine = TextIO.inputLine fromChild
@@ -164,10 +265,7 @@
let val proofextract = extract_proof (currentString^thisLine)
in
trace ("\nextracted spass proof: " ^ proofextract);
- if !reconstruct
- then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num
- names_arr thm; ())
- else Recon_Transfer.spass_lemma_list proofextract probfile toParent
+ spass_lemma_list proofextract probfile toParent
ppid names_arr
end
else transferSpassInput (fromChild, toParent, ppid, probfile,
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Sep 28 16:01:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,228 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-structure ReconOrderClauses =
-struct
-
-(*----------------------------------------------*)
-(* Reorder clauses for use in binary resolution *)
-(*----------------------------------------------*)
-
-fun remove_nth n [] = []
-| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
-
-(*Differs from List.nth: it counts from 1 rather than from 0*)
-fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs))
-
-
-exception Not_in_list;
-
-
-(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
-
- fun takeUntil ch [] res = (res, [])
- | takeUntil ch (x::xs) res = if x = ch
- then
- (res, xs)
- else
- takeUntil ch xs (res@[x]);
-
-fun contains_eq str = "=" mem str
-
-fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
- in (List.last uptoeq) <> "~" end
-
-fun get_eq_strs str = if eq_not_neq str (*not an inequality *)
- then
- let val (left, right) = takeUntil "=" str []
- in
- (#1 (split_last left), tl right)
- end
- else (* is an inequality *)
- let val (left, right) = takeUntil "~" str []
- in
- (#1 (split_last left), tl (tl right))
- end
-
-
-
-fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
- val (x_lhs, x_rhs) = get_eq_strs x
- in
- (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
- end
-
-fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
-
-fun var_equiv vars (a,b) = a=b orelse (is_var_pair (a,b) vars)
-
-fun all_true [] = false
-| all_true xs = null (List.filter (equal false ) xs)
-
-
-
-fun var_pos_eq vars x y =
- String.size x = String.size y andalso
- let val xs = explode x
- val ys = explode y
- val xsys = ListPair.zip (xs,ys)
- val are_var_pairs = map (var_equiv vars) xsys
- in
- all_true are_var_pairs
- end;
-
-fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
- | pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
- let val y = explode x
- val b = explode a
- in
- if b = y
- then
- (pos_num, symlist, nsymlist)
- else
- if (var_pos_eq allvars a x)
- then (* Equal apart from meta-vars having different names *)
- (pos_num, symlist, nsymlist)
- else
- if (contains_eq b) andalso (contains_eq y)
- then
- if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y )
- then (* both are equalities and equal under sym*)
- (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
- else
- if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y)
- then (* if they're equal under not_sym *)
- (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
- else
- raise Not_in_list
- else
- raise Not_in_list
- end
- | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) =
- let val y = explode x
- val b = explode a
- in
- if b = y
- then
- (pos_num, symlist, nsymlist)
-
- else
- if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
- then
- (pos_num, symlist, nsymlist)
- else
- if (contains_eq b) andalso (contains_eq y)
- then
- if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
- then
- (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
- if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
- then
- (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
- else
- pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
- else
- pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
-
- end;
-
-
- (* in
- if b = y
- then
- (pos_num, symlist, nsymlist)
- else if (contains_eq b) andalso (contains_eq y)
- then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
- then if (switch_equal b y ) (* if they're equal under sym *)
- then
- (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
- else
- pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
- else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *)
- then if (switch_equal b y ) (* if they're equal under not_sym *)
- then
- (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
- else
- pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
- else
- pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
- else
- pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
- else
- pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
- end
-
- *)
-
-
-(* checkorder Spass Isabelle [] *)
-
-fun checkorder [] strlist allvars (numlist, symlist, not_symlist) =
- (numlist,symlist, not_symlist)
-| checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =
- let val (posnum, symlist', not_symlist') =
- pos_in_list x strlist allvars (0, symlist, not_symlist)
- in
- checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist')
- end
-
-fun is_digit ch =
- ( ch >= "0" andalso ch <= "9")
-
-
-fun is_alpha ch =
- (ch >= "A" andalso ch <= "Z") orelse
- (ch >= "a" andalso ch <= "z")
-
-
-fun is_alpha_space_or_neg_or_eq ch =
- (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
-
-fun lit_string sg t =
- let val termstr = Sign.string_of_term sg t
- val exp_term = explode termstr
- in
- implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
- end
-
-fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
-
-
-fun is_alpha_space_or_neg_or_eq_or_bracket ch =
- is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
-
-fun lit_string_bracket sg t =
- let val termstr = Sign.string_of_term sg t
- val exp_term = explode termstr
- in
- implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
- end;
-
-fun get_meta_lits_bracket thm =
- map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
-
-
-fun apply_rule rule [] thm = thm
-| apply_rule rule (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
- in
- apply_rule rule xs thm'
- end
-
-
-
-(* resulting thm, clause-strs in spass order, vars *)
-
-fun rearrange_clause thm res_strlist allvars =
- let val isa_strlist = get_meta_lits thm
- (* change this to use Jia's code to get same looking thing as isastrlist? *)
- val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
- val symmed = apply_rule sym symlist thm
- val not_symmed = apply_rule not_sym not_symlist symmed
- in
- ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
- end
-
-end;
-
--- a/src/HOL/Tools/ATP/recon_parse.ML Thu Sep 28 16:01:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,408 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(* Parsing functions *)
-
-(* Auxiliary functions *)
-
-structure Recon_Parse =
-struct
-
-open ReconTranslateProof;
-
-exception NOPARSE_WORD
-exception NOPARSE_NUM
-fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
-
-fun string2int s =
- (case Int.fromString s of SOME i => i
- | NONE => error "string -> int failed");
-
-
-(* Parser combinators *)
-
-exception Noparse;
-
-fun (parser1 ++ parser2) input =
- let
- val (result1, rest1) = parser1 input
- val (result2, rest2) = parser2 rest1
- in
- ((result1, result2), rest2)
- end;
-
-fun many parser input =
- let (* Tree * token list*)
- val (result, next) = parser input
- val (results, rest) = many parser next
- in
- ((result::results), rest)
- end
- handle Noparse => ([], input)
-| NOPARSE_WORD => ([], input)
-| NOPARSE_NUM => ([], input);
-
-
-
-fun (parser >> treatment) input =
- let
- val (result, rest) = parser input
- in
- (treatment result, rest)
- end;
-
-fun (parser1 || parser2) input = parser1 input
-handle Noparse => parser2 input;
-
-infixr 8 ++; infixr 7 >>; infixr 6 ||;
-
-fun some p [] = raise Noparse
- | some p (h::t) = if p h then (h, t) else raise Noparse;
-
-fun a tok = some (fn item => item = tok);
-
-fun finished input = if input = [] then (0, input) else raise Noparse;
-
-
- (* Parsing the output from gandalf *)
-datatype token = Word of string
- | Number of int
- | Other of string
-
-
- exception NOCUT
- fun remove_prefix [] l = l
- | remove_prefix (h::t) [] = error "can't remove prefix"
- | remove_prefix (h::t) (h'::t') = remove_prefix t t'
- fun ccut t [] = raise NOCUT
- | ccut t s =
- if is_prefix (op =) t s then ([], remove_prefix t s) else
- let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
- fun cut t s =
- let
- val t' = explode t
- val s' = explode s
- val (a, b) = ccut t' s'
- in
- (implode a, implode b)
- end
-
- fun cut_exists t s
- = let val (a, b) = cut t s in true end handle NOCUT => false
-
- fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
- fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
-
-
- fun kill_lines 0 = Library.I
- | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
-
-
-fun several p = many (some p)
- fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
-
- fun lower_letter s = ("a" <= s) andalso (s <= "z")
- fun upper_letter s = ("A" <= s) andalso (s <= "Z")
- fun digit s = ("0" <= s) andalso (s <= "9")
- fun letter s = lower_letter s orelse upper_letter s
- fun alpha s = letter s orelse (s = "_")
- fun alphanum s = alpha s orelse digit s
- fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
- (* FIX this is stopping it picking up numbers *)
- val word = (some alpha ++ several alphanum) >> (Word o collect)
- val number =
- (some digit ++ several digit) >> (Number o string2int o collect)
- val other = some (K true) >> Other
-
- val token = (word || number || other) ++ several space >> fst
- val tokens = (several space ++ many token) >> snd
- val alltokens = (tokens ++ finished) >> fst
-
- (* val lex = fst ( alltokens ( (map str) explode))*)
- fun lex s = alltokens (explode s)
-
-
-(************************************************************)
-
-(**************************************************)
-(* Code to parse SPASS proofs *)
-(**************************************************)
-
-datatype Tree = Leaf of string
- | Branch of Tree * Tree
-
-
- fun number ((Number n)::rest) = (n, rest)
- | number _ = raise NOPARSE_NUM
- fun word ((Word w)::rest) = (w, rest)
- | word _ = raise NOPARSE_WORD
-
- fun other_char ( (Other p)::rest) = (p, rest)
- | other_char _ =raise NOPARSE_WORD
-
- val number_list =
- (number ++ many number)
- >> (fn (a, b) => (a::b))
-
- val term_num =
- (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
-
-
- val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
- >> (fn (a, b) => (a::b)))
-
- val axiom = (a (Word "Inp"))
- >> (fn (_) => Axiom)
-
-
- val binary = (a (Word "Res")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
-
-
-
- val factor = (a (Word "Fac")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Factor ((fst c), (snd c),(snd e)))
-
- val para = (a (Word "SPm")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
-
- val super_l = (a (Word "SpL")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
-
-
- val super_r = (a (Word "SpR")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
-
-
- val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
- >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
-
- val rewrite = (a (Word "Rew")) ++ (a (Other ":"))
- ++ term_num_list
- >> (fn (_, (_, (c))) => Rewrite (c))
-
-
- val mrr = (a (Word "MRR")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
-
- val ssi = (a (Word "SSi")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
-
- val unc = (a (Word "UnC")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
-
-
-
- val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
- >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
-
- val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
- >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
-
- val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
- >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
-
-(*
- val hyper = a (Word "hyper")
- ++ many ((a (Other ",") ++ number) >> snd)
- >> (Hyper o snd)
-*)
- (* val method = axiom ||binary || factor || para || hyper*)
-
- val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
-
- val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
- >> (fn (_, (_, a)) => Binary_s a)
- val factor_s = a (Word "factor_s")
- >> (fn _ => Factor_s ())
- val demod_s = a (Word "demod")
- ++ (many ((a (Other ",") ++ term_num) >> snd))
- >> (fn (_, a) => Demod_s a)
-
- val hyper_s = a (Word "hyper_s")
- ++ many ((a (Other ",") ++ number) >> snd)
- >> (Hyper_s o snd)
- val simp_method = binary_s || factor_s || demod_s || hyper_s
- val simp = a (Other ",") ++ simp_method >> snd
- val simps = many simp
-
-
- val justification =
- a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
- >> (fn (_,(_, (_,(b, _)))) => b)
-
-
-exception NOTERM
-
-(* FIX - should change the stars and pluses to many rather than explicit patterns *)
-
-fun trim_prefix a b =
- let val n = String.size a
- in String.substring (b, n, (size b) - n) end;
-
-
-(* FIX - add the other things later *)
-fun remove_typeinfo x =
- if String.isPrefix ResClause.fixed_var_prefix x
- then trim_prefix ResClause.fixed_var_prefix x
- else if String.isPrefix ResClause.schematic_var_prefix x
- then trim_prefix ResClause.schematic_var_prefix x
- else if String.isPrefix ResClause.const_prefix x
- then trim_prefix ResClause.const_prefix x
- else if String.isPrefix ResClause.tfree_prefix x
- then ""
- else if String.isPrefix ResClause.tvar_prefix x
- then ""
- else if String.isPrefix ResClause.tconst_prefix x
- then ""
- else x;
-
-fun term input = ( ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) => (a@b))
- ) input
-
-(* pterms are terms from the rhs of the -> in the spass proof. *)
-(* they should have a "~" in front of them so that they match with *)
-(* positive terms in the meta-clause *)
-(* nterm are terms from the lhs of the spass proof, and shouldn't *)
-(* "~"s added word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) => (a^" "^b)) *)
-
-and pterm input = (
- peqterm >> (fn (a) => a)
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
- >> (fn (a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
- >> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
- >> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
- >> (fn (a, (_,(b, (_,_)))) => ("~"^" "^(remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")")
- >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
-
- || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
-
-and nterm input =
-
- (
- neqterm >> (fn (a) => a)
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
- >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
- >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
- >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
- >> (fn ( a, (_,(b, (_,_)))) => ((remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "(") ++ arglist ++ a (Other ")")
- >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
-
- || word ++ a (Other "*") >> (fn (w,b) => (remove_typeinfo w))
- || word >> (fn w => (remove_typeinfo w))
- ) input
-
-
-and peqterm input =(
-
- a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
- >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "+")
- >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "*")
- >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*")
- >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
-
-
- ||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
-
-
-
-and neqterm input =(
-
- a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
- >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "+")
- >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*") ++ a (Other "*")
- >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
-
- || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- ++ a (Other "*")
- >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
-
-
- ||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
- >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
-
-
-
-and ptermlist input = (many pterm
- >> (fn (a) => (a))) input
-
-and ntermlist input = (many nterm
- >> (fn (a) => (a))) input
-
-(*and arglist input = ( nterm >> (fn (a) => (a))
- || nterm ++ many (a (Other ",") ++ nterm >> snd)
- >> (fn (a, b) => (a^" "^(space_implode " " b)))) input*)
-
-and arglist input = ( nterm ++ many (a (Other ",") ++ nterm >> snd)
- >> (fn (a, b) => (a^" "^(space_implode " " b)))
- || nterm >> (fn (a) => (a)))input
-
- val clause = term
-
-(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
- val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++
- a (Other "|") ++ clause ++ a (Other ".")
- >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
-
- val lines = many line
- val alllines = (lines ++ finished) >> fst
-
- val parse = fst o alllines
-
-end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 28 16:01:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,638 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-structure Recon_Transfer =
-struct
-
-open Recon_Parse
-
-infixr 8 ++; infixr 7 >>; infixr 6 ||;
-
-val trace_path = Path.basic "transfer_trace";
-
-fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
- else ();
-
-
-(* Versions that include type information *)
-
-(* FIXME rename to str_of_thm *)
-fun string_of_thm thm =
- setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm;
-
-
-(* check separate args in the watcher program for separating strings with a * or ; or something *)
-
-fun clause_strs_to_string [] str = str
-| clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
-
-fun thmvars_to_string [] str = str
-| thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
-
-
-fun proofstep_to_string Axiom = "Axiom()"
-| proofstep_to_string (Binary ((a,b), (c,d)))=
- "Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
-| proofstep_to_string (Factor (a,b,c)) =
- "Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
-| proofstep_to_string (Para ((a,b), (c,d)))=
- "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
-| proofstep_to_string (MRR ((a,b), (c,d))) =
- "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
-(*| proofstep_to_string (Rewrite((a,b),(c,d))) =
- "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
-
-
-fun proof_to_string (num,(step,clause_strs, thmvars)) =
- (string_of_int num)^(proofstep_to_string step)^
- "["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
-
-
-fun proofs_to_string [] str = str
-| proofs_to_string (x::xs) str = proofs_to_string xs (str ^ proof_to_string x)
-
-
-fun init_proofstep_to_string (num, step, clause_strs) =
- (string_of_int num)^" "^(proofstep_to_string step)^" "^
- (clause_strs_to_string clause_strs "")^" "
-
-fun init_proofsteps_to_string [] str = str
-| init_proofsteps_to_string (x::xs) str =
- init_proofsteps_to_string xs (str ^ init_proofstep_to_string x)
-
-
-
-(*** get a string representing the Isabelle ordered axioms ***)
-
-fun origAx_to_string (num,(meta,thmvars)) =
- let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
- in
- (string_of_int num)^"OrigAxiom()["^
- (clause_strs_to_string clause_strs "")^"]["^
- (thmvars_to_string thmvars "")^"]"
- end
-
-
-fun origAxs_to_string [] str = str
-| origAxs_to_string (x::xs) str =
- origAxs_to_string xs (str ^ origAx_to_string x )
-
-
-(*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
-
-fun extraAx_to_string (num, (meta,thmvars)) =
- let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
- in
- (string_of_int num)^"ExtraAxiom()["^
- (clause_strs_to_string clause_strs "")^"]"^
- "["^(thmvars_to_string thmvars "")^"]"
- end;
-
-fun extraAxs_to_string [] str = str
-| extraAxs_to_string (x::xs) str =
- let val newstr = extraAx_to_string x
- in
- extraAxs_to_string xs (str^newstr)
- end;
-
-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])
-
-exception Noassoc;
-
-fun assoc_snd a [] = raise Noassoc
- | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
-
-(* change to be something using check_order instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
-
-(*fun get_assoc_snds [] xs assocs= assocs
-| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
-*)
-(*FIX - should this have vars in it? *)
-fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true)
- handle _ => false
-
-fun assoc_out_of_order a [] = raise Noassoc
-| assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
-
-fun get_assoc_snds [] xs assocs= assocs
-| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
-
-fun add_if_not_inlist eq [] xs newlist = newlist
-| add_if_not_inlist eq (y::ys) xs newlist =
- if not (member eq xs y) then add_if_not_inlist eq ys xs (y::newlist)
- else add_if_not_inlist eq ys xs newlist
-
-(*Flattens a list of list of strings to one string*)
-fun onestr ls = String.concat (map String.concat ls);
-
-
-(**** retrieve the axioms that were obtained from the clasimpset ****)
-
-(*Get names of axioms used. Axioms are indexed from 1, while the array is indexed from 0*)
-fun get_axiom_names (names_arr: string array) step_nums =
- let fun is_axiom n = n <= Array.length names_arr
- fun index i = Array.sub(names_arr, i-1)
- val axnums = List.filter is_axiom step_nums
- val axnames = sort_distinct string_ord (map index axnums)
- in
- if length axnums = length step_nums then "UNSOUND!!" :: axnames
- else axnames
- 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. *)
-fun get_spass_linenums proofstr =
- 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
- in List.mapPartial (inputno o toks) lines end
-
-fun get_axiom_names_spass proofstr names_arr =
- get_axiom_names names_arr (get_spass_linenums proofstr);
-
- (*String contains multiple lines. We want those of the form
- "number : ...: ...: initial..." *)
-fun get_e_linenums proofstr =
- let val fields = String.fields (fn c => c = #":")
- val nospaces = String.translate (fn c => if c = #" " then "" else str c)
- fun initial s = String.isPrefix "initial" (nospaces s)
- fun firstno (line :: _ :: _ :: rule :: _) =
- if initial rule then Int.fromString line else NONE
- | firstno _ = NONE
- val lines = String.tokens (fn c => c = #"\n") proofstr
- in List.mapPartial (firstno o fields) lines end
-
-fun get_axiom_names_e proofstr names_arr =
- get_axiom_names names_arr (get_e_linenums proofstr);
-
- (*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 =
- 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
- in List.mapPartial (inputno o toks) lines end
-
-fun get_axiom_names_vamp proofstr names_arr =
- get_axiom_names names_arr (get_vamp_linenums proofstr);
-
-
-(***********************************************)
-(* get axioms for reconstruction *)
-(***********************************************)
-fun numclstr (vars, []) str = str
-| numclstr ( vars, ((num, thm)::rest)) str =
- let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
- in
- numclstr (vars,rest) newstr
- end
-
-fun addvars c (a,b) = (a,b,c)
-
-fun get_axioms_used proof_steps thms names_arr =
- let val axioms = (List.filter is_axiom) proof_steps
- val step_nums = get_step_nums axioms []
-
- val clauses = make_clauses thms (*FIXME: must this be repeated??*)
-
- val vars = map thm_varnames clauses
-
- val distvars = distinct (op =) (fold append vars [])
- val clause_terms = map prop_of clauses
- val clause_frees = List.concat (map term_frees clause_terms)
-
- val frees = map lit_string_with_nums clause_frees;
-
- val distfrees = distinct (op =) frees
-
- val metas = map Meson.make_meta_clause clauses
- val ax_strs = map #3 axioms
-
- (* literals of -all- axioms, not just those used by spass *)
- val meta_strs = map ReconOrderClauses.get_meta_lits metas
-
- val metas_and_strs = ListPair.zip (metas,meta_strs)
- val _ = trace ("\nAxioms: " ^ onestr ax_strs)
- val _ = trace ("\nMeta_strs: " ^ onestr meta_strs)
-
- (* get list of axioms as thms with their variables *)
-
- val ax_metas = get_assoc_snds ax_strs metas_and_strs []
- val ax_vars = map thm_varnames ax_metas
- val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
-
- (* get list of extra axioms as thms with their variables *)
- val extra_metas = add_if_not_inlist Thm.eq_thm metas ax_metas []
- val extra_vars = map thm_varnames extra_metas
- val extra_with_vars = if not (null extra_metas)
- then ListPair.zip (extra_metas,extra_vars)
- else []
- in
- (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
- end;
-
-
-(*********************************************************************)
-(* Pass in spass string of proof and string version of isabelle goal *)
-(* Get out reconstruction steps as a string to be sent to Isabelle *)
-(*********************************************************************)
-
-fun rules_to_string [] = "NONE"
- | rules_to_string xs = space_implode " " xs
-
-
-(*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 names_arr =
- let val _ = trace
- ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
- "\nprobfile is " ^ probfile ^
- " num of clauses is " ^ string_of_int (Array.length names_arr))
- val axiom_names = getax proofstr names_arr
- val ax_str = rules_to_string axiom_names
- in
- trace ("\nDone. Lemma list is " ^ ax_str);
- TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
- ax_str ^ "\n");
- TextIO.output (toParent, probfile ^ "\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
- end
- handle exn => (*FIXME: exn handler is too general!*)
- (trace ("\nprover_lemma_list_aux: In exception handler: " ^
- Toplevel.exn_message exn);
- 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));
-
-val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
-
-val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
-
-val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
-
-
-(**** Full proof reconstruction for SPASS (not really working) ****)
-
-fun spass_reconstruct proofstr probfile toParent ppid thms names_arr =
- let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
- val tokens = #1(lex proofstr)
-
- (* parse spass proof into datatype *)
- (***********************************)
- val proof_steps = parse tokens
- val _ = trace "\nParsing finished"
-
- (************************************)
- (* recreate original subgoal as thm *)
- (************************************)
- (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
- (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
- (* subgoal this is, and turn it into meta_clauses *)
- (* should prob add array and table here, so that we can get axioms*)
- (* produced from the clasimpset rather than the problem *)
- val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms names_arr
-
- (*val numcls_string = numclstr ( vars, numcls) ""*)
- val _ = trace "\ngot axioms"
-
- (************************************)
- (* translate proof *)
- (************************************)
- val _ = trace ("\nabout to translate proof, steps: "
- ^ (init_proofsteps_to_string proof_steps ""))
- val (newthm,proof) = translate_proof numcls proof_steps vars
- val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
- (***************************************************)
- (* transfer necessary steps as strings to Isabelle *)
- (***************************************************)
- (* turn the proof into a string *)
- val reconProofStr = proofs_to_string proof ""
- (* do the bit for the Isabelle ordered axioms at the top *)
- val ax_nums = map #1 numcls
- val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
- val numcls_strs = ListPair.zip (ax_nums,ax_strs)
- val num_cls_vars = map (addvars vars) numcls_strs;
- val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
-
- val extra_nums = if not (null extra_with_vars) then (1 upto (length extra_with_vars))
- else []
- val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
- val frees_str = "["^(thmvars_to_string frees "")^"]"
- val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
- val _ = trace ("\nReconstruction:\n" ^ reconstr)
- in
- TextIO.output (toParent, reconstr^"\n");
- TextIO.output (toParent, probfile ^ "\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- all_tac
- end
- handle exn => (*FIXME: exn handler is too general!*)
- (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
- TextIO.output (toParent,"Translation failed for SPASS proof:"^
- String.toString proofstr ^"\n");
- TextIO.output (toParent, probfile ^ "\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
-
-(**********************************************************************************)
-(* At other end, want to turn back into datatype so can apply reconstruct_proof. *)
-(* This will be done by the signal handler *)
-(**********************************************************************************)
-
-(* Parse in the string version of the proof steps for reconstruction *)
-(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*)
-
-
- val term_numstep =
- (number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c))
-
-val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")"))
- >> (fn (_) => ExtraAxiom)
-
-
-
-val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")"))
- >> (fn (_) => OrigAxiom)
-
-
- val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")"))
- >> (fn (_) => Axiom)
-
-
-
-
- val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "("))
- ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
- ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
- >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e))
-
-
- val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "("))
- ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
- ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
- >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e))
-
- val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "("))
- ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
- ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
- >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e))
-
-
- val factorstep = (a (Word "Factor")) ++ (a (Other "("))
- ++ number ++ (a (Other ","))
- ++ number ++ (a (Other ","))
- ++ number ++ (a (Other ")"))
-
- >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) => Factor (c,e,f))
-
-
-(*val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "("))
- ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
- ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
- >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
-
-val obviousstep = (a (Word "Obvious")) ++ (a (Other "("))
- ++ term_numstep ++ (a (Other ")"))
- >> (fn (_, (_, (c,_))) => Obvious (c))
-
- val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
-
-
- val number_list_step =
- ( number ++ many ((a (Other ",") ++ number)>> #2))
- >> (fn (a,b) => (a::b))
-
- val numberlist_step = a (Other "[") ++ a (Other "]")
- >>(fn (_,_) => ([]:int list))
- || a (Other "[") ++ number_list_step ++ a (Other "]")
- >>(fn (_,(a,_)) => a)
-
-
-
-(** change this to allow P (x U) *)
- fun arglist_step input =
- ( word ++ many word >> (fn (a, b) => (a^" "^(space_implode " " b)))
- ||word >> (fn (a) => (a)))input
-
-
-fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++ a (Other ")")
- >>(fn (a, (b, (c,d))) => (a^" ("^(c)^")"))
- || arglist_step >> (fn (a) => (a)))input
-
-
-
-(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
- || arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input
-*)
-
-
- fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
- || literal_step ++ a (Other "%")>> (fn (a,b) => a ))input
-
-
-
-
- val term_list_step =
- ( term_step ++ many ( term_step))
- >> (fn (a,b) => (a::b))
-
-
-val term_lists_step = a (Other "[") ++ a (Other "]")
- >>(fn (_,_) => ([]:string list))
- || a (Other "[") ++ term_list_step ++ a (Other "]")
- >>(fn (_,(a,_)) => a)
-
-
- val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
- >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
-
- val lines_step = many linestep
-
- val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
-
- val parse_step = #1 o alllines_step
-
-
- (*
-val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) -->(EX x::'a::type. P x) = (ALL y::'a::type. P y)"
-*)
-
-(************************************************************)
-(* Construct an Isar style proof from a list of proof steps *)
-(************************************************************)
-(* want to assume all axioms, then do haves for the other clauses*)
-(* then show for the last step *)
-
-(* replace ~ by not here *)
-val change_nots = String.translate (fn c => if c = #"~" then "\\<not>" else str c);
-
-fun clstrs_to_string xs = space_implode "; " (map change_nots xs);
-
-fun thmvars_to_quantstring [] str = str
-| thmvars_to_quantstring (x::[]) str =str^x^". "
-| thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
-
-
-fun clause_strs_to_isar clstrs [] =
- "\"\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\""
-| clause_strs_to_isar clstrs thmvars =
- "\"\\<And>"^(thmvars_to_quantstring thmvars "")^
- "\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\""
-
-fun frees_to_isar_str clstrs = space_implode " " (map change_nots clstrs)
-
-
-(***********************************************************************)
-(* functions for producing assumptions for the Isabelle ordered axioms *)
-(***********************************************************************)
-(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
-num, rule, clausestrs, vars*)
-
-
-(* assume the extra clauses - not used in Spass proof *)
-
-fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true
-| is_extraaxiom_step (num, _) = false
-
-fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs)
-
-fun assume_isar_extraaxiom [] str = str
-| assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
-
-
-
-fun assume_isar_extraaxioms [] = ""
-|assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n"
- in
- assume_isar_extraaxiom xs str
- end
-
-(* assume the Isabelle ordered clauses *)
-
-fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true
-| is_origaxiom_step (num, _) = false
-
-fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs)
-
-fun assume_isar_origaxiom [] str = str
-| assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
-
-
-
-fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n"
- in
- assume_isar_origaxiom xs str
- end
-
-
-
-fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true
-| is_axiom_step (num, _) = false
-
-fun get_axioms xs = List.filter (is_axiom_step) ( xs)
-
-fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
-
-fun by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n"
-
-
-fun isar_axiomline (numb, (step, clstrs, thmstrs)) = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) )
-
-
-fun isar_axiomlines [] str = str
-| isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x))
-
-
-fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
-(*FIX: ask Larry to add and mrr attribute *)
-
-fun by_isar_line ((Binary ((a,b), (c,d)))) =
- "by(rule cl"^
- (string_of_int a)^" [binary "^(string_of_int b)^" cl"^
- (string_of_int c)^" "^(string_of_int d)^"])\n"
-|by_isar_line ((MRR ((a,b), (c,d)))) =
- "by(rule cl"^
- (string_of_int a)^" [binary "^(string_of_int b)^" cl"^
- (string_of_int c)^" "^(string_of_int d)^"])\n"
-| by_isar_line ( (Para ((a,b), (c,d)))) =
- "by (rule cl"^
- (string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
- (string_of_int c)^" "^(string_of_int d)^"])\n"
-| by_isar_line ((Factor ((a,b,c)))) =
- "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
- (string_of_int c)^" ])\n"
-(*| by_isar_line ( (Rewrite ((a,b),(c,d)))) =
- "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
- (string_of_int c)^" "^(string_of_int d)^" ])\n"*)
-| by_isar_line ( (Obvious ((a,b)))) =
- "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
-
-fun isar_line (numb, (step, clstrs, thmstrs)) = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
-
-
-fun isar_lines [] str = str
-| isar_lines (x::xs) str = isar_lines xs (str^(isar_line x))
-
-fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
-
-
-fun to_isar_proof (frees, xs) =
- let val extraaxioms = get_extraaxioms xs
- val extraax_num = length extraaxioms
- val origaxioms_and_steps = Library.drop (extraax_num, xs)
-
- val origaxioms = get_origaxioms origaxioms_and_steps
- val origax_num = length origaxioms
- val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)
- val axioms = get_axioms axioms_and_steps
-
- val steps = Library.drop (origax_num, axioms_and_steps)
- val (firststeps, laststep) = split_last steps
-
- val isar_proof =
- ("show \"[your goal]\"\n")^
- ("proof (rule ccontr,skolemize, make_clauses) \n")^
- ("fix "^(frees_to_isar_str frees)^"\n")^
- (assume_isar_extraaxioms extraaxioms)^
- (assume_isar_origaxioms origaxioms)^
- (isar_axiomlines axioms "")^
- (isar_lines firststeps "")^
- (last_isar_line laststep)^
- ("qed")
- val _ = trace ("\nto_isar_proof returns " ^ isar_proof)
- in
- isar_proof
- end;
-
-(* get fix vars from axioms - all Frees *)
-(* check each clause for meta-vars and /\ over them at each step*)
-
-(*******************************************************)
-(* This assumes the thm list "numcls" is still there *)
-(* In reality, should probably label it with an *)
-(* ID number identifying the subgoal. This could *)
-(* be passed over to the watcher, e.g. numcls25 *)
-(*******************************************************)
-
-fun apply_res_thm str =
- let val tokens = #1 (lex str);
- val _ = trace ("\napply_res_thm. str is: "^str^"\n")
- val (frees,recon_steps) = parse_step tokens
- in
- to_isar_proof (frees, recon_steps)
- end
-
-end;
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Sep 28 16:01:34 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,421 +0,0 @@
-(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-structure ReconTranslateProof =
-struct
-
-fun thm_varnames thm =
- (Drule.fold_terms o Term.fold_aterms)
- (fn Var ((x, _), _) => insert (op =) x | _ => I) thm [];
-
-exception Reflex_equal;
-
-(********************************)
-(* Proofstep datatype *)
-(********************************)
-(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3] *)
-
-datatype Side = Left |Right
-
-datatype Proofstep = ExtraAxiom
- | OrigAxiom
- | VampInput
- | Axiom
- | Binary of (int * int) * (int * int) (* (clause1,lit1), (clause2, lit2) *)
- | MRR of (int * int) * (int * int)
- | Factor of (int * int * int) (* (clause,lit1, lit2) *)
- | Para of (int * int) * (int * int)
- | Super_l of (int * int) * (int * int)
- | Super_r of (int * int) * (int * int)
- (*| Rewrite of (int * int) * (int * int) *)
- | Rewrite of (int * int) list
- | SortSimp of (int * int) * (int * int)
- | UnitConf of (int * int) * (int * int)
- | Obvious of (int * int)
- | AED of (int*int)
- | EqualRes of (int*int)
- | Condense of (int*int)
- (*| Hyper of int list*)
- | Unusedstep of unit
-
-
-datatype Clausesimp = Binary_s of int * int
- | Factor_s of unit
- | Demod_s of (int * int) list
- | Hyper_s of int list
- | Unusedstep_s of unit
-
-
-
-datatype Step_label = T_info
- |P_info
-
-
-fun is_alpha_space_digit_or_neg ch =
- (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse
- (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
-
-fun string_of_term (Const(s,_)) = s
- | string_of_term (Free(s,_)) = s
- | string_of_term (Var(ix,_)) = Term.string_of_vname ix
- | string_of_term (Bound i) = string_of_int i
- | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
- | string_of_term (s $ t) =
- "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
-
-(* FIXME string_of_term is quite unreliable here *)
-fun lit_string_with_nums t = let val termstr = string_of_term t
- val exp_term = explode termstr
- in
- implode(List.filter is_alpha_space_digit_or_neg exp_term)
- end
-
-fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
-
-(************************************************)
-(* Reconstruct an axiom resolution step *)
-(* clauses is a list of (clausenum,clause) pairs*)
-(************************************************)
-
-fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
- let val this_axiom = (the o AList.lookup (op =) clauses) clausenum
- val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)
- val thmvars = thm_varnames res
- in
- (res, (Axiom,clause_strs,thmvars ) )
- end
- handle Option => reconstruction_failed "follow_axiom"
-
-(****************************************)
-(* Reconstruct a binary resolution step *)
-(****************************************)
-
- (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
-fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
- let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
- val thm2 = (the o AList.lookup (op =) thml) clause2
- val res = thm1 RSN ((lit2 +1), thm2)
- val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
- val thmvars = thm_varnames res
- in
- (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
- end
- handle Option => reconstruction_failed "follow_binary"
-
-
-
-(******************************************************)
-(* Reconstruct a matching replacement resolution step *)
-(******************************************************)
-
-
-fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
- let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
- val thm2 = (the o AList.lookup (op =) thml) clause2
- val res = thm1 RSN ((lit2 +1), thm2)
- val (res', numlist, symlist, nsymlist) =
- (ReconOrderClauses.rearrange_clause res clause_strs allvars)
- val thmvars = thm_varnames res
- in
- (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
- end
- handle Option => reconstruction_failed "follow_mrr"
-
-
-(*******************************************)
-(* Reconstruct a factoring resolution step *)
-(*******************************************)
-
-fun mksubstlist [] sublist = sublist
- |mksubstlist ((a, (_, b)) :: rest) sublist =
- let val vartype = type_of b
- val avar = Var(a,vartype)
- val newlist = ((avar,b)::sublist)
- in
- mksubstlist rest newlist
- end;
-
-(* based on Tactic.distinct_subgoals_tac *)
-
-fun delete_assump_tac state lit =
- let val (frozth,thawfn) = freeze_thaw state
- val froz_prems = cprems_of frozth
- val assumed = implies_elim_list frozth (map assume froz_prems)
- val new_prems = ReconOrderClauses.remove_nth lit froz_prems
- val implied = implies_intr_list new_prems assumed
- in
- Seq.single (thawfn implied)
- end
-
-
-
-
-
-(*************************************)
-(* Reconstruct a factoring step *)
-(*************************************)
-
-fun getnewenv seq = fst (fst (the (Seq.pull seq)));
-
-(*FIXME: share code with that in Tools/reconstruction.ML*)
-fun follow_factor clause lit1 lit2 allvars thml clause_strs =
- let
- val th = (the o AList.lookup (op =) thml) clause
- val prems = prems_of th
- val sign = sign_of_thm th
- val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
- val fac2 = ReconOrderClauses.get_nth (lit2+1) prems
- val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
- val newenv = getnewenv unif_env
- val envlist = Envir.alist_of newenv
-
- val (t1,t2)::_ = mksubstlist envlist []
- in
- if (is_Var t1)
- then
- let
- val str1 = lit_string_with_nums t1;
- val str2 = lit_string_with_nums t2;
- val facthm = read_instantiate [(str1,str2)] th;
- val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
- val (res', numlist, symlist, nsymlist) =
- ReconOrderClauses.rearrange_clause res clause_strs allvars
- val thmvars = thm_varnames res'
- in
- (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars))
- end
- else
- let
- val str2 = lit_string_with_nums t1;
- val str1 = lit_string_with_nums t2;
- val facthm = read_instantiate [(str1,str2)] th;
- val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
- val (res', numlist, symlist, nsymlist) =
- ReconOrderClauses.rearrange_clause res clause_strs allvars
- val thmvars = thm_varnames res'
- in
- (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars))
- end
- end
- handle Option => reconstruction_failed "follow_factor"
-
-
-
-fun get_unif_comb t eqterm =
- if ((type_of t) = (type_of eqterm))
- then t
- else
- let val _ $ rand = t
- in get_unif_comb rand eqterm end;
-
-fun get_unif_lit t eqterm =
- if (can HOLogic.dest_eq t)
- then
- let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
- in lhs end
- else
- get_unif_comb t eqterm;
-
-
-
-(*************************************)
-(* Reconstruct a paramodulation step *)
-(*************************************)
-
-val rev_subst = rotate_prems 1 subst;
-val rev_ssubst = rotate_prems 1 ssubst;
-
-
-fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
- let
- val th1 = (the o AList.lookup (op =) thml) clause1
- val th2 = (the o AList.lookup (op =) 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_head newth
- val (res, numlist, symlist, nsymlist) =
- (ReconOrderClauses.rearrange_clause newth' clause_strs allvars
- handle Not_in_list =>
- let val mod_lit_th' = mod_lit_th RS not_sym
- val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
- val newth' =negate_head newth
- in
- ReconOrderClauses.rearrange_clause newth' clause_strs allvars
- end)
- val thmvars = thm_varnames res
- in
- (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
- end
- handle Option => reconstruction_failed "follow_standard_para"
-
-
-(********************************)
-(* Reconstruct a rewriting step *)
-(********************************)
-
-(*
-
-val rev_subst = rotate_prems 1 subst;
-
-fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
- let val eq_lit_th = select_literal (lit1+1) cl1
- val mod_lit_th = select_literal (lit2+1) cl2
- val eqsubst = eq_lit_th RSN (2,rev_subst)
- val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
-eqsubst)
- in Meson.negated_asm_of_head newth end;
-
-val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
-eqsubst)
-
-val mod_lit_th' = mod_lit_th RS not_sym
-
-*)
-
-
-fun delete_assumps 0 th = th
-| delete_assumps n th = let val th_prems = length (prems_of th)
- val th' = hd (Seq.list_of(delete_assump_tac th (th_prems -1)))
- in
- delete_assumps (n-1) th'
- end
-
-(* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *)
-(* changed negate_nead to negate_head here too*)
- (* clause1, lit1 is thing to rewrite with *)
-(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
- let val th1 = (the o AList.lookup (op =) thml) clause1
- val th2 = (the o AList.lookup (op =) 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 eq_lit_prem_num = length (prems_of eq_lit_th)
- val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
- val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
- val newthm = negate_head newth
- val newthm' = delete_assumps eq_lit_prem_num newthm
- val (res, numlist, symlist, nsymlist) =
- ReconOrderClauses.rearrange_clause newthm clause_strs allvars
- val thmvars = thm_varnames res
- in
- (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars))
- end
- handle Option => reconstruction_failed "follow_rewrite"
-
-*)
-
-(*****************************************)
-(* Reconstruct an obvious reduction step *)
-(*****************************************)
-
-
-fun follow_obvious (clause1, lit1) allvars thml clause_strs =
- let val th1 = (the o AList.lookup (op =) thml) clause1
- val prems1 = prems_of th1
- val newthm = refl RSN ((lit1+ 1), th1)
- handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
- val (res, numlist, symlist, nsymlist) =
- ReconOrderClauses.rearrange_clause newthm clause_strs allvars
- val thmvars = thm_varnames res
- in
- (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
- end
- handle Option => reconstruction_failed "follow_obvious"
-
-(**************************************************************************************)
-(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
-(**************************************************************************************)
-
- fun follow_proof clauses allvars clausenum thml (Axiom ) clause_strs
- = follow_axiom clauses allvars clausenum thml clause_strs
-
- | follow_proof clauses allvars clausenum thml (Binary (a, b)) clause_strs
- = follow_binary (a, b) allvars thml clause_strs
-
- | follow_proof clauses allvars clausenum thml (MRR (a, b)) clause_strs
- = follow_mrr (a, b) allvars thml clause_strs
-
- | follow_proof clauses allvars clausenum thml (Factor (a, b, c)) clause_strs
- = follow_factor a b c allvars thml clause_strs
-
- | follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs
- = follow_standard_para (a, b) allvars thml clause_strs
-
- (* | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs
- = follow_rewrite (a,b) allvars thml clause_strs*)
-
- | follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs
- = follow_obvious (a,b) allvars thml clause_strs
-
- (*| follow_proof clauses clausenum thml (Hyper l)
- = follow_hyper l thml*)
- | follow_proof clauses allvars clausenum thml _ _ =
- error "proof step not implemented"
-
-
-
-
-(**************************************************************************************)
-(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
-(**************************************************************************************)
-
- fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons =
- let
- val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs
- in
- ((clause_num, thm)::thml, (clause_num,recon_fun)::recons)
- end
-
-(***************************************************************)
-(* follow through the res. proof, creating an Isabelle theorem *)
-(***************************************************************)
-
-fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
-
-fun proofstring x = let val exp = explode x
- in
- List.filter (is_proof_char ) exp
- end
-
-fun replace_clause_strs [] recons newrecons = (newrecons)
-| replace_clause_strs ((thmnum, thm)::thml)
- ((clausenum,(step,clause_strs,thmvars))::recons) newrecons =
- let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
- in
- replace_clause_strs thml recons
- ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
- end
-
-
-fun follow clauses [] allvars thml recons =
- let
- val new_recons = replace_clause_strs thml recons []
- in
- (#2(hd thml), new_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
-
-(* 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 *)
-
-(* takes original axioms, proof_steps parsed from spass, variables *)
-
-fun translate_proof clauses proof allvars
- = let val (thm, recons) = follow clauses proof allvars [] []
- in
- (thm, (recons))
- end
-
-end;
--- a/src/HOL/Tools/ATP/watcher.ML Thu Sep 28 16:01:34 2006 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Sep 28 16:01:48 2006 +0200
@@ -371,10 +371,7 @@
Output.debug ("In signal handler. outcome = \"" ^ outcome ^
"\"\nprobfile = " ^ probfile ^
"\nGoals being watched: "^ Int.toString (!goals_being_watched));
- if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
- then (priority (Recon_Transfer.apply_res_thm outcome);
- decr_watched())
- else if String.isPrefix "Invalid" outcome
+ if String.isPrefix "Invalid" outcome
then (report ("Subgoal is not provable:\n" ^ text);
decr_watched())
else if String.isPrefix "Failure" outcome
--- a/src/HOL/Tools/reconstruction.ML Thu Sep 28 16:01:34 2006 +0200
+++ b/src/HOL/Tools/reconstruction.ML Thu Sep 28 16:01:48 2006 +0200
@@ -43,6 +43,8 @@
Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
end;
+fun getnewenv seq = fst (fst (the (Seq.pull seq)));
+
fun factor_rule (cl, lit1, lit2) =
let
val prems = prems_of cl
@@ -50,7 +52,7 @@
val fac2 = List.nth (prems,lit2)
val sign = sign_of_thm cl
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
- val newenv = ReconTranslateProof.getnewenv unif_env
+ val newenv = getnewenv unif_env
val envlist = Envir.alist_of newenv
in
inst_subst sign (mksubstlist envlist []) cl