--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,482 @@
+(*use "Translate_Proof";*)
+(* Parsing functions *)
+
+(* Auxiliary functions *)
+
+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 = id
+ | 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 ^ (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))
+
+ 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
+
+
+
+
+
+
+(*
+ fun gandalf_parse s =
+ let
+ val e = extract_proof;
+ val t = fst(lex e)
+ val r = parse t
+ in
+ r
+ end
+
+*)