--- 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;