diff -r 7a6f69cf5a86 -r a7a5157c5e75 src/HOL/Tools/ATP/recon_parse.ML --- 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;