Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
(* ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
(*use "Translate_Proof";*)
(* Parsing functions *)
(* Auxiliary functions *)
structure Recon_Parse =
struct
exception ASSERTION of string;
exception NOPARSE_WORD
exception NOPARSE_NUM
fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
fun string2int s =
let
val io = Int.fromString s
in
case io of
(SOME i) => i
| _ => raise ASSERTION "string -> int failed"
end
(* Parser combinators *)
exception Noparse;
exception SPASSError of string;
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 is_prefix [] l = true
| is_prefix (h::t) [] = false
| is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
fun remove_prefix [] l = l
| remove_prefix (h::t) [] = raise (ASSERTION "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 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 extract_proof s
= if cut_exists "EMPTY CLAUSE DERIVED" s then
(kill_lines 6
o snd o cut_after "EMPTY CLAUSE DERIVED"
o fst o cut_after "contradiction.\n") s
else
raise (GandalfError "Couldn't find a proof.")
*)
val proofstring =
"0:00:00.00 for the reduction.\
\\
\Here is a proof with depth 3, length 7 :\
\1[0:Inp] || -> P(xa)*.\
\2[0:Inp] || -> Q(xb)*.\
\3[0:Inp] || R(U)* -> .\
\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
\11[0:Res:2.0,9.0] || P(U)* -> .\
\12[0:Res:1.0,11.0] || -> .\
\Formulae used in the proof :\
\\
\--------------------------SPASS-STOP------------------------------"
fun extract_proof s
= if cut_exists "Here is a proof with" s then
(kill_lines 0
o snd o cut_after ":"
o snd o cut_after "Here is a proof with"
o fst o cut_after " || -> .") s
else
raise SPASSError "Couldn't find a proof."
fun several p = many (some p)
fun collect (h, t) = h ^ (Utils.itlist (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)
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 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 rewrite = (a (Word "Rew")) ++ (a (Other ":"))
++ term_num ++ (a (Other ","))
++ term_num
>> (fn (_, (_, (c, (_, e)))) => Rewrite (c, e))
val mrr = (a (Word "MRR")) ++ (a (Other ":"))
++ term_num ++ (a (Other ","))
++ term_num
>> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
>> (fn (_, (_, c)) => Obvious ((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 || rewrite || mrr || obv
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
fun implode_with_space [] = implode []
| implode_with_space [x] = implode [x]
| implode_with_space (x::[y]) = x^" "^y
| implode_with_space (x::xs) = (x^" "^(implode_with_space xs))
(* FIX - should change the stars and pluses to many rather than explicit patterns *)
(* FIX - add the other things later *)
fun remove_typeinfo x = if (String.isPrefix "v_" x )
then
(String.substring (x,2, ((size x) - 2)))
else if (String.isPrefix "V_" x )
then
(String.substring (x,2, ((size x) - 2)))
else if (String.isPrefix "typ_" x )
then
""
else if (String.isPrefix "Typ_" x )
then
""
else if (String.isPrefix "tconst_" x )
then
""
else if (String.isPrefix "const_" x )
then
(String.substring (x,6, ((size x) - 6)))
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 >> (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 >> (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^" "^(implode_with_space b)))) input*)
and arglist input = ( nterm ++ many (a (Other ",") ++ nterm >> snd)
>> (fn (a, b) => (a^" "^(implode_with_space b)))
|| nterm >> (fn (a) => (a)))input
val clause = term
(*val line = number ++ justification ++ a (Other "|") ++
a (Other "|") ++ clause ++ a (Other ".")
>> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)
(* 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
val s = proofstring;
fun dropUntilNot ch [] = ( [])
| dropUntilNot ch (x::xs) = if not(x = ch )
then
(x::xs)
else
dropUntilNot ch xs
fun remove_spaces str [] = str
| remove_spaces str (x::[]) = if x = " "
then
str
else
(str^x)
| remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
val (next) = dropUntilNot " " rest
in
if next = []
then
(str^(implode first))
else remove_spaces (str^(implode first)^" ") next
end
fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
fun all_spaces xs = List.filter (not_equal " " ) xs
fun just_change_space [] = []
| just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
in
if (all_spaces newstrs = [] ) (* all type_info *) then
(clausenum, step, newstrs)::(just_change_space xs)
else
(clausenum, step, newstrs)::(just_change_space xs)
end
fun change_space [] = []
| change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
in
if (all_spaces newstrs = [] ) (* all type_info *)
then
(clausenum, step, T_info, newstrs)::(change_space xs)
else
(clausenum, step, P_info, newstrs)::(change_space xs)
end
end;