# HG changeset patch # User blanchet # Date 1335253660 -7200 # Node ID d6683fe037b152b871e1c8829458271faacefc71 # Parent bd0683000a0fb20671bdb3e406deb8bbe4c675e8 get rid of old parser, hopefully for good diff -r bd0683000a0f -r d6683fe037b1 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Tue Apr 24 09:47:40 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Tue Apr 24 09:47:40 2012 +0200 @@ -11,8 +11,6 @@ declare [[show_consts]] (* for Refute *) -typedecl iota (* for TPTP *) - use "atp_problem_import.ML" end diff -r bd0683000a0f -r d6683fe037b1 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200 @@ -22,92 +22,6 @@ open ATP_Proof -(** Crude TPTP CNF and FOF parsing (obsolescent) **) - -exception SYNTAX of string -exception THF of unit - -val tptp_explode = raw_explode o strip_spaces_except_between_idents - -fun parse_file_path (c :: ss) = - if c = "'" orelse c = "\"" then - ss |> chop_while (curry (op <>) c) |>> implode ||> tl - else - raise SYNTAX "invalid file path" - | parse_file_path [] = raise SYNTAX "invalid file path" - -fun parse_include x = - let - val (file_name, rest) = - (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")" - --| $$ ".") x - val path = file_name |> Path.explode - val path = - path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP") - in ((), (path |> File.read |> tptp_explode) @ rest) end - -val parse_cnf_or_fof = - (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |-- - Scan.many (not_equal ",") |-- $$ "," |-- - (Scan.this_string "axiom" || Scan.this_string "definition" - || Scan.this_string "theorem" || Scan.this_string "lemma" - || Scan.this_string "hypothesis" || Scan.this_string "conjecture" - || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula - --| $$ ")" --| $$ "." - >> (fn ("conjecture", phi) => (true, AConn (ANot, [phi])) - | (_, phi) => (false, phi)) - || Scan.this_string "thf" >> (fn _ => raise THF ()) - -val parse_problem = - Scan.repeat parse_include - |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include) - -val parse_tptp_problem = - Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input") - parse_problem)) - o tptp_explode - -val iota_T = @{typ iota} -val quant_T = @{typ "(iota => bool) => bool"} - -fun is_variable s = Char.isUpper (String.sub (s, 0)) - -fun hol_term_from_fo_term res_T (ATerm (x, us)) = - let val ts = map (hol_term_from_fo_term iota_T) us in - list_comb ((case x of - "$true" => @{const_name True} - | "$false" => @{const_name False} - | "=" => @{const_name HOL.eq} - | "equal" => @{const_name HOL.eq} - | _ => x, map fastype_of ts ---> res_T) - |> (if is_variable x then Free else Const), ts) - end - -fun hol_prop_from_formula phi = - case phi of - AQuant (_, [], phi') => hol_prop_from_formula phi' - | AQuant (q, (x, _) :: xs, phi') => - Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex}, - quant_T) - $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi'))) - | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u') - | AConn (c, [u1, u2]) => - pairself hol_prop_from_formula (u1, u2) - |> (case c of - AAnd => HOLogic.mk_conj - | AOr => HOLogic.mk_disj - | AImplies => HOLogic.mk_imp - | AIff => HOLogic.mk_eq - | ANot => raise Fail "binary \"ANot\"") - | AConn _ => raise Fail "malformed AConn" - | AAtom u => hol_term_from_fo_term @{typ bool} u - -fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t - -fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t - - (** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **) fun mk_meta_not P = Logic.mk_implies (P, @{prop False}) @@ -129,23 +43,11 @@ |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD")) + val ((_, _, problem), thy) = + TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy in - (case parse_tptp_problem (File.read path) of - (_, s :: ss) => - raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss))) - | (problem, []) => - (exists fst problem, - map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd) - problem)) - handle THF () => - let - val problem = - TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy - |> fst |> #3 - in - (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem, - map get_tptp_formula problem) - end + (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem, + map get_tptp_formula problem, thy) end (** Isabelle (combination of provers) **) @@ -157,8 +59,9 @@ fun nitpick_tptp_file timeout file_name = let - val (falsify, ts) = read_tptp_file @{theory} file_name - val state = Proof.init @{context} + val (falsify, ts, thy) = read_tptp_file @{theory} file_name + val ctxt = Proof_Context.init_global thy + val state = Proof.init ctxt val params = [("card", "1\100"), ("box", "false"), @@ -173,7 +76,7 @@ ("format", "1000"), ("max_potential", "0"), ("timeout", string_of_int timeout)] - |> Nitpick_Isar.default_params @{theory} + |> Nitpick_Isar.default_params thy val i = 1 val n = 1 val step = 0 @@ -196,11 +99,13 @@ fun refute_tptp_file timeout file_name = let - val (falsify, ts) = read_tptp_file @{theory} file_name + val (falsify, ts, thy) = read_tptp_file @{theory} file_name + val ctxt = Proof_Context.init_global thy val params = - [("maxtime", string_of_int timeout)] + [("maxtime", string_of_int timeout), + ("maxvars", "100000")] in - Refute.refute_term @{context} params ts @{prop False} + Refute.refute_term ctxt params ts @{prop False} |> print_szs_from_outcome falsify end