# HG changeset patch
# User blanchet
# Date 1406537853 -7200
# Node ID 44341963ade3496f4f5a832c2790909c07bb5dc9
# Parent  fb71c6f100f814d82a840a12d4480164b8448139
correctly translate THF functions from terms to types

diff -r fb71c6f100f8 -r 44341963ade3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Jul 27 21:11:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 28 10:57:33 2014 +0200
@@ -2,6 +2,7 @@
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Mathias Fleury, ENS Rennes
 
 Abstract representation of ATP proofs and TSTP/SPASS syntax.
 *)
@@ -295,7 +296,7 @@
 
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
-val dummy_atype = AType(("", []), [])
+val dummy_atype = AType (("", []), [])
 
 (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
 fun parse_dependency x =
@@ -459,16 +460,17 @@
   | role_of_tptp_string "type" = Type_Role
   | role_of_tptp_string _ = Unknown
 
-val tptp_binary_op_list = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if,
-                             tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
+val tptp_binary_ops =
+  [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
+   tptp_equal, tptp_app]
 
 fun parse_binary_op x =
-  (foldl1 (op ||) (map Scan.this_string tptp_binary_op_list)
-    >> (fn c => if c = tptp_equal then "equal" else c)) x
+  (foldl1 (op ||) (map Scan.this_string tptp_binary_ops)
+   >> (fn c => if c = tptp_equal then "equal" else c)) x
 
 fun parse_thf0_type x =
   (($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
-     -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
+   -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
   >> (fn (a, NONE) => a
        | (a, SOME b) => AFun (a, b))) x
 
diff -r fb71c6f100f8 -r 44341963ade3 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Jul 27 21:11:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 28 10:57:33 2014 +0200
@@ -116,25 +116,33 @@
 (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information
    from type literals, or by type inference. *)
 fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) =
-  let val Ts = map (typ_of_atp_type ctxt) tys in
-    (case unprefix_and_unascii type_const_prefix a of
-      SOME b => Type (invert_const b, Ts)
-    | NONE =>
-      if not (null tys) then
-        raise ATP_TYPE [ty] (* only "tconst"s have type arguments *)
-      else
-        (case unprefix_and_unascii tfree_prefix a of
-          SOME b => make_tfree ctxt b
-        | NONE =>
-          (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
-             Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
-             forces us to use a type parameter in all cases. *)
-          Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
-            (if null clss then @{sort type} else map class_of_atp_class clss))))
+    let val Ts = map (typ_of_atp_type ctxt) tys in
+      (case unprefix_and_unascii type_const_prefix a of
+        SOME b => Type (invert_const b, Ts)
+      | NONE =>
+        if not (null tys) then
+          raise ATP_TYPE [ty] (* only "tconst"s have type arguments *)
+        else
+          (case unprefix_and_unascii tfree_prefix a of
+            SOME b => make_tfree ctxt b
+          | NONE =>
+            (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
+               Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
+               forces us to use a type parameter in all cases. *)
+            Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
+              (if null clss then @{sort type} else map class_of_atp_class clss))))
+    end
+  | typ_of_atp_type ctxt (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2
+
+fun atp_type_of_atp_term (ATerm ((s, _), us)) =
+  let val tys = map atp_type_of_atp_term us in
+    if s = tptp_fun_type then
+      (case tys of
+        [ty1, ty2] => AFun (ty1, ty2)
+      | _ => raise ATP_TYPE tys)
+    else
+      AType ((s, []), tys)
   end
-  | typ_of_atp_type ctxt (AFun (a, tys)) = typ_of_atp_type ctxt a --> typ_of_atp_type ctxt tys
-
-fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
 
 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term