open ATP_Util

 (** TPTP parsing **)

 open ATP_Problem

 open ATP_Proof

 (* cf. "close_form" in "refute.ML" *)

 (** Crude TPTP CNF and FOF parsing **)

 fun close_form t =

   fold (fn ((s, i), T) => fn t' =>

 exception SYNTAX of string

            Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))

 exception THF of unit

        (Term.add_vars t []) t

 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

   P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not

   P |> Logic.varify_global |> close_form

     |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not

   let val path = Path.explode file_name in

   let

     (case parse_tptp_problem (File.read path) of

     val path = Path.explode file_name

        (_, s :: ss) =>

     val problem =

        raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))

       TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy

      | (problem, []) =>

       |> fst |> #3

        (exists fst problem,

   in

         map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd)

     (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,

             problem))

      map get_tptp_formula 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