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) **)