1.1 --- a/src/HOL/TPTP/atp_problem_import.ML Wed Apr 18 23:13:10 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Apr 18 23:13:11 2012 +0200
1.3 @@ -17,119 +17,29 @@
1.4 structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
1.5 struct
1.6
1.7 -open ATP_Util
1.8 -open ATP_Problem
1.9 -open ATP_Proof
1.10 +(** TPTP parsing **)
1.11
1.12 -
1.13 -(** Crude TPTP CNF and FOF parsing **)
1.14 -
1.15 -exception SYNTAX of string
1.16 -exception THF of unit
1.17 -
1.18 -val tptp_explode = raw_explode o strip_spaces_except_between_idents
1.19 -
1.20 -fun parse_file_path (c :: ss) =
1.21 - if c = "'" orelse c = "\"" then
1.22 - ss |> chop_while (curry (op <>) c) |>> implode ||> tl
1.23 - else
1.24 - raise SYNTAX "invalid file path"
1.25 - | parse_file_path [] = raise SYNTAX "invalid file path"
1.26 -
1.27 -fun parse_include x =
1.28 - let
1.29 - val (file_name, rest) =
1.30 - (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
1.31 - --| $$ ".") x
1.32 - val path = file_name |> Path.explode
1.33 - val path =
1.34 - path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
1.35 - in ((), (path |> File.read |> tptp_explode) @ rest) end
1.36 -
1.37 -val parse_cnf_or_fof =
1.38 - (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
1.39 - Scan.many (not_equal ",") |-- $$ "," |--
1.40 - (Scan.this_string "axiom" || Scan.this_string "definition"
1.41 - || Scan.this_string "theorem" || Scan.this_string "lemma"
1.42 - || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
1.43 - || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
1.44 - --| $$ ")" --| $$ "."
1.45 - >> (fn ("conjecture", phi) => (true, AConn (ANot, [phi]))
1.46 - | (_, phi) => (false, phi))
1.47 - || Scan.this_string "thf" >> (fn _ => raise THF ())
1.48 -
1.49 -val parse_problem =
1.50 - Scan.repeat parse_include
1.51 - |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
1.52 -
1.53 -val parse_tptp_problem =
1.54 - Scan.finite Symbol.stopper
1.55 - (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
1.56 - parse_problem))
1.57 - o tptp_explode
1.58 -
1.59 -val iota_T = @{typ iota}
1.60 -val quant_T = @{typ "(iota => bool) => bool"}
1.61 -
1.62 -fun is_variable s = Char.isUpper (String.sub (s, 0))
1.63 -
1.64 -fun hol_term_from_fo_term res_T (ATerm (x, us)) =
1.65 - let val ts = map (hol_term_from_fo_term iota_T) us in
1.66 - list_comb ((case x of
1.67 - "$true" => @{const_name True}
1.68 - | "$false" => @{const_name False}
1.69 - | "=" => @{const_name HOL.eq}
1.70 - | "equal" => @{const_name HOL.eq}
1.71 - | _ => x, map fastype_of ts ---> res_T)
1.72 - |> (if is_variable x then Free else Const), ts)
1.73 - end
1.74 -
1.75 -fun hol_prop_from_formula phi =
1.76 - case phi of
1.77 - AQuant (_, [], phi') => hol_prop_from_formula phi'
1.78 - | AQuant (q, (x, _) :: xs, phi') =>
1.79 - Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
1.80 - quant_T)
1.81 - $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
1.82 - | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
1.83 - | AConn (c, [u1, u2]) =>
1.84 - pairself hol_prop_from_formula (u1, u2)
1.85 - |> (case c of
1.86 - AAnd => HOLogic.mk_conj
1.87 - | AOr => HOLogic.mk_disj
1.88 - | AImplies => HOLogic.mk_imp
1.89 - | AIff => HOLogic.mk_eq
1.90 - | ANot => raise Fail "binary \"ANot\"")
1.91 - | AConn _ => raise Fail "malformed AConn"
1.92 - | AAtom u => hol_term_from_fo_term @{typ bool} u
1.93 -
1.94 -fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
1.95 -
1.96 -fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
1.97 +(* cf. "close_form" in "refute.ML" *)
1.98 +fun close_form t =
1.99 + fold (fn ((s, i), T) => fn t' =>
1.100 + Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
1.101 + (Term.add_vars t []) t
1.102
1.103 fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
1.104
1.105 fun get_tptp_formula (_, role, P, _) =
1.106 - P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
1.107 + P |> Logic.varify_global |> close_form
1.108 + |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
1.109
1.110 fun read_tptp_file thy file_name =
1.111 - let val path = Path.explode file_name in
1.112 - (case parse_tptp_problem (File.read path) of
1.113 - (_, s :: ss) =>
1.114 - raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
1.115 - | (problem, []) =>
1.116 - (exists fst problem,
1.117 - map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd)
1.118 - problem))
1.119 - handle THF () =>
1.120 - let
1.121 - val problem =
1.122 - TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
1.123 - |> fst |> #3
1.124 - in
1.125 - (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
1.126 - map get_tptp_formula problem)
1.127 - end
1.128 + let
1.129 + val path = Path.explode file_name
1.130 + val problem =
1.131 + TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
1.132 + |> fst |> #3
1.133 + in
1.134 + (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
1.135 + map get_tptp_formula problem)
1.136 end
1.137
1.138 (** Isabelle (combination of provers) **)