# HG changeset patch
# User fleury
# Date 1402928499 -7200
# Node ID 0d5e34ba4d280dfa950dc87aea7b727e9a0b5a96
# Parent  cf43583f9bb9de3ee0ff69b337e491c08ebb7b81
Correcting the type parser

diff -r cf43583f9bb9 -r 0d5e34ba4d28 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 16:18:34 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 16:21:39 2014 +0200
@@ -289,7 +289,6 @@
 
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
-val dummy_aterm = ATerm (("", []), [])
 val dummy_atype = AType(("", []), [])
 
 (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
@@ -384,23 +383,38 @@
 
 fun is_same_term subst tm1 tm2 =
   let
-    fun do_term_pair _ NONE = NONE
-      | do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) =
+    fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2))
+          (SOME subst) =
+        if typ1 <> typ2 andalso length args1 = length args2 then NONE
+        else
+          let val ls = length subst in
+            SOME ((var1, var2) :: subst)
+            |> do_term_pair body1 body2
+            |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst)
+                 | NONE => NONE)
+            |> (if length args1 = length args2
+              then fold2 do_term_pair args1 args2
+              else (fn _ => NONE))
+          end
+      | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) =
         (case pairself is_tptp_variable (s1, s2) of
           (true, true) =>
           (case AList.lookup (op =) subst s1 of
-             SOME s2' => if s2' = s2 then SOME subst else NONE
-           | NONE =>
-             if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst)
-             else NONE)
+            SOME s2' => if s2' = s2 then SOME subst else NONE
+          | NONE =>
+            if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst)
+            else NONE)
         | (false, false) =>
-          if s1 = s2 andalso length tm1 = length tm2 then
-            SOME subst |> fold do_term_pair (tm1 ~~ tm2)
+          if s1 = s2 then
+            SOME subst
           else
             NONE
-        | _ => NONE)
+        | _ => NONE) |> (if length args1 = length args2
+                       then fold2 do_term_pair args1 args2
+                       else (fn _ => NONE))
+      | do_term_pair _ _ _ = NONE
   in
-    SOME subst |> do_term_pair (tm1, tm2) |> is_some
+    SOME subst |> do_term_pair tm1 tm2 |> is_some
   end
 
 fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
@@ -442,14 +456,14 @@
                              tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
 
 fun parse_binary_op x =
-  foldl1 (op ||) (map Scan.this_string tptp_binary_op_list) x
+  (foldl1 (op ||) (map Scan.this_string tptp_binary_op_list)
+    >> (fn c => if c = tptp_equal then "equal" else c)) x
 
 fun parse_thf0_type x =
-  ($$ "(" |-- parse_thf0_type --| $$ ")" --| $$ tptp_fun_type -- parse_thf0_type >> AFun
-   || scan_general_id --| $$ tptp_fun_type --
-parse_thf0_type >> apfst (fn t => AType ((t, []), [])) >> AFun
-   || scan_general_id >> (fn t => AType ((t, []), []))
-   || $$ "(" |-- parse_thf0_type --| $$ ")") x
+  (($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
+     -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
+  >> (fn (a, NONE) => a
+       | (a, SOME b) => AFun (a, b))) x
 
 fun mk_ho_of_fo_quant q =
   if q = tptp_forall then tptp_ho_forall
@@ -470,56 +484,51 @@
      --| Scan.option (Scan.this_string ","))
    || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
 
-fun parse_literal_hol x =
-  ((Scan.repeat ($$ tptp_not) >> length)
-   -- ($$ "(" |-- parse_formula_hol_raw --| $$ ")"
-       || scan_general_id >> mk_simple_aterm
-       || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var,typ) => ATerm(((var,[typ]),[])))
-       || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm)
-   >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_app (mk_simple_aterm tptp_not))) x
-
-and parse_formula_hol_raw x =
-  (((parse_literal_hol
-      -- parse_binary_op
-      -- parse_formula_hol_raw)
-    >> (fn ((phi1, c) , phi2) =>
-        if c = tptp_app then mk_app phi1 phi2
-        else mk_apps (mk_simple_aterm c) [phi1, phi2]))
-   || (Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
-        -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_formula_hol_raw
-      >> (fn ((q, t), phi) =>
-        if q <> tptp_lambda then
+fun parse_simple_thf0_term x =
+  ((Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
+        -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
+      >> (fn ((q, ys), t) =>
           fold_rev
             (fn (var, ty) => fn r =>
-              mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm)
-                (AAbs (((var, the_default dummy_atype ty), r), [])))
-            t phi
-        else
-          fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []))
-                   t phi)
-   || Scan.this_string tptp_not |-- parse_formula_hol_raw >> (mk_app (mk_simple_aterm tptp_not))
-   || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
-   || parse_literal_hol
-   || scan_general_id >> mk_simple_aterm) x
+                AAbs (((var, the_default dummy_atype ty), r), [])
+                |> (if tptp_lambda <> q then
+                      mk_app (q |> mk_ho_of_fo_quant
+                                |> mk_simple_aterm)
+                    else I))
+            ys t)
+  || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
+  || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
+  || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm
+  || $$ "(" |-- parse_thf0_term --| $$ ")"
+  || scan_general_id >> mk_simple_aterm) x
+and parse_thf0_term x =
+  (parse_simple_thf0_term
+      -- Scan.option (parse_binary_op
+      -- parse_thf0_term)
+    >> (fn (t1, SOME (c, t2)) =>
+           if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2]
+         | (t, NONE) => t)) x
 
-fun parse_formula_hol x = (parse_formula_hol_raw #>> remove_thf_app #>> AAtom) x
+fun parse_thf0_formula x = (parse_thf0_term #>> remove_thf_app #>> AAtom) x
 
-fun parse_tstp_line_hol problem =
+fun parse_tstp_thf0_line problem =
   ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
     || Scan.this_string tptp_tff || Scan.this_string tptp_thf)
   -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
-  -- parse_formula_hol -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
+  -- parse_thf0_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
   >> (fn (((num, role), phi), deps) =>
       let
+        val role' = role_of_tptp_string role
         val ((name, phi), rule, deps) =
           (case deps of
-             File_Source (_, SOME s) =>
-             (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
-          | File_Source _ =>
-             (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
+            File_Source (_, SOME s) =>
+            if role' = Definition then
+              (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
+            else
+              (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
           | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
       in
-        [(name, role_of_tptp_string role, phi, rule, map (rpair []) deps)]
+        [(name, role', phi, rule, map (rpair []) deps)]
       end)
 
 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
@@ -559,7 +568,7 @@
                  AAtom (ATerm (("equal", _), _)) =>
                   (* Vampire's equality proxy axiom *)
                   (name, Definition, phi, rule, map (rpair []) deps)
-                | _ => mk_step ())
+               | _ => mk_step ())
              | _ => mk_step ())]
           end)
 
@@ -641,7 +650,7 @@
    >> map (core_inference z3_tptp_core_rule)) x
 
 fun parse_line name problem =
-  if name = leo2N then parse_tstp_line_hol problem
+  if name = leo2N then parse_tstp_thf0_line problem
   else if name = satallaxN then parse_satallax_core_line
   else if name = spassN then parse_spass_line
   else if name = spass_pirateN then parse_spass_pirate_line
diff -r cf43583f9bb9 -r 0d5e34ba4d28 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 16:18:34 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 16:21:39 2014 +0200
@@ -189,6 +189,19 @@
 val vampire_skolem_prefix = "sK"
 
 
+fun var_index_of_textual textual = if textual then 0 else 1
+
+fun quantify_over_var textual quant_of var_s var_T t =
+  let
+    val vars = ((var_s, var_index_of_textual textual), var_T) ::
+                 filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
+    val normTs = vars |> AList.group (op =) |> map (apsnd hd)
+    fun norm_var_types (Var (x, T)) =
+        Var (x, the_default T (AList.lookup (op =) normTs x))
+      | norm_var_types t = t
+  in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
+
+
 (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
    are typed.
 
@@ -196,14 +209,16 @@
 fun term_of_atp_ho ctxt textual sym_tab =
   let
     val thy = Proof_Context.theory_of ctxt
-    val var_index = if textual then 0 else 1
+    val var_index = var_index_of_textual textual
 
     fun do_term opt_T u =
       (case u of
         AAbs(((var, ty), term), []) =>
-        let val typ = typ_of_atp_type ctxt ty in
-          absfree (repair_var_name textual var, typ) (do_term NONE term)
-        end
+        let
+          val typ = typ_of_atp_type ctxt ty
+          val var_name = repair_var_name textual var
+          val tm = do_term NONE term
+        in quantify_over_var textual lambda' var_name typ tm end
       | ATerm ((s, tys), us) =>
         if s = ""
         then error "Isar proof reconstruction failed because the ATP proof \
@@ -284,7 +299,7 @@
     (* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise
        conflict with variable constraints in the goal. At least, type inference often fails
        otherwise. See also "axiom_inference" in "Metis_Reconstruct". *)
-    val var_index = if textual then 0 else 1
+    val var_index = var_index_of_textual textual
 
     fun do_term extra_ts opt_T u =
       (case u of
@@ -409,15 +424,6 @@
       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
 
-fun quantify_over_var quant_of var_s t =
-  let
-    val vars = filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
-    val normTs = vars |> AList.group (op =) |> map (apsnd hd)
-    fun norm_var_types (Var (x, T)) =
-        Var (x, the_default T (AList.lookup (op =) normTs x))
-      | norm_var_types t = t
-  in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
-
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
    formula. *)
 fun prop_of_atp ctxt format type_enc textual sym_tab phi =
@@ -428,8 +434,8 @@
       | AQuant (q, (s, _) :: xs, phi') =>
         do_formula pos (AQuant (q, xs, phi'))
         (* FIXME: TFF *)
-        #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of)
-          (repair_var_name textual s)
+        #>> quantify_over_var textual (case q of AForall => forall_of | AExists => exists_of)
+          (repair_var_name textual s) dummyT
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1