use ":" for type information (looks good in Metis's output) and handle it in new path finder

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -52,7 +52,6 @@
 
   type translated_formula
 
-  val type_tag_name : string
   val bound_var_prefix : string
   val schematic_var_prefix: string
   val fixed_var_prefix: string
@@ -70,6 +69,7 @@
   val typed_helper_suffix : string
   val predicator_name : string
   val app_op_name : string
+  val type_tag_name : string
   val type_pred_name : string
   val simple_type_prefix : string
   val ascii_of: string -> string
@@ -146,8 +146,6 @@
 val elim_info = useful_isabelle_info "elim"
 val simp_info = useful_isabelle_info "simp"
 
-val type_tag_name = "ti"
-
 val bound_var_prefix = "B_"
 val schematic_var_prefix = "V_"
 val fixed_var_prefix = "v_"
@@ -178,6 +176,7 @@
 
 val predicator_name = "hBOOL"
 val app_op_name = "hAPP"
+val type_tag_name = "ti"
 val type_pred_name = "is"
 val simple_type_prefix = "ty_"
 

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
@@ -180,20 +180,20 @@
           else
             Const (c, dummyT)
         end
-      fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
+      fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
              (case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
-        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
+        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
             Const (@{const_name HOL.eq}, HOLogic.typeT)
-        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
+        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_unascii const_prefix x of
                 SOME c => do_const c
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
               | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
-        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
+        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
             cvt tm1 $ cvt tm2
         | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
             cvt tm1 $ cvt tm2
@@ -215,11 +215,13 @@
   in fol_tm |> cvt end
 
 fun atp_name_from_metis s =
-  case AList.find (op =) metis_name_table s of
-    (s', ary) :: _ => (s', SOME ary)
-  | _ => (s, NONE)
+  case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
+    SOME ((s, _), (_, swap)) => (s, swap)
+  | _ => (s, false)
 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
-    ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms)
+    let val (s, swap) = atp_name_from_metis s in
+      ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
+    end
   | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
 
 fun hol_term_from_metis_MX sym_tab ctxt =
@@ -487,6 +489,14 @@
       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
+      fun path_finder_fail mode tm ps t =
+        raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+                    "equality_inf, path_finder_" ^ string_of_mode mode ^
+                    ": path = " ^ space_implode " " (map string_of_int ps) ^
+                    " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+                    (case t of
+                       SOME t => " fol-term: " ^ Metis_Term.toString t
+                     | NONE => ""))
       fun path_finder_FO tm [] = (tm, Bound 0)
         | path_finder_FO tm (p::ps) =
             let val (tm1,args) = strip_comb tm
@@ -507,27 +517,22 @@
       fun path_finder_HO tm [] = (tm, Bound 0)
         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
-        | path_finder_HO tm ps =
-          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
-                      "equality_inf, path_finder_HO: path = " ^
-                      space_implode " " (map string_of_int ps) ^
-                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
+        | path_finder_HO tm ps = path_finder_fail HO tm ps NONE
       fun path_finder_FT tm [] _ = (tm, Bound 0)
-        | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
+        | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) =
             path_finder_FT tm ps t1
         | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
         | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
-        | path_finder_FT tm ps t =
-          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
-                      "equality_inf, path_finder_FT: path = " ^
-                      space_implode " " (map string_of_int ps) ^
-                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
-                      " fol-term: " ^ Metis_Term.toString t)
+        | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
       fun path_finder_MX tm [] _ = (tm, Bound 0)
         | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
-          if s = metis_app_op (* FIXME ### mangled etc. *) then
+          (* FIXME ### what if these are mangled? *) 
+          if s = metis_type_tag then
+            if p = 1 then path_finder_MX tm ps (nth ts 1)
+            else path_finder_fail MX tm (p :: ps) (SOME t)
+          else if s = metis_app_op then
             let
               val (tm1, tm2) = dest_comb tm in
               if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)
@@ -540,21 +545,13 @@
               val p' = if adjustment > p then p else p - adjustment
               val tm_p = nth args p'
                 handle Subscript =>
-                       raise METIS ("equality_inf",
-                                    string_of_int p ^ " adj " ^
-                                    string_of_int adjustment ^ " term " ^
-                                    Syntax.string_of_term ctxt tm)
+                       path_finder_fail MX tm (p :: ps) (SOME t)
               val _ = trace_msg ctxt (fn () =>
                   "path_finder: " ^ string_of_int p ^ "  " ^
                   Syntax.string_of_term ctxt tm_p)
               val (r, t) = path_finder_MX tm_p ps (nth ts p)
             in (r, list_comb (tm1, replace_item_list t p' args)) end
-        | path_finder_MX tm ps t =
-          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
-                      "equality_inf, path_finder_MX: path = " ^
-                      space_implode " " (map string_of_int ps) ^
-                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
-                      " fol-term: " ^ Metis_Term.toString t)
+        | path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t)
       fun path_finder FO tm ps _ = path_finder_FO tm ps
         | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
              (*equality: not curried, as other predicates are*)

--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -20,10 +20,11 @@
      old_skolems : (string * term) list}
 
   val metis_equal : string
+  val metis_type_tag : string
   val metis_predicator : string
   val metis_app_op : string
   val metis_generated_var_prefix : string
-  val metis_name_table : ((string * int) * string) list
+  val metis_name_table : ((string * int) * (string * bool)) list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val string_of_mode : mode -> string
   val prepare_metis_problem :
@@ -40,13 +41,15 @@
 val metis_equal = "="
 val metis_predicator = "{}"
 val metis_app_op = "."
+val metis_type_tag = ":"
 val metis_generated_var_prefix = "_"
 
 val metis_name_table =
-  [((tptp_equal, 2), metis_equal),
-   ((tptp_old_equal, 2), metis_equal),
-   ((const_prefix ^ predicator_name, 1), metis_predicator),
-   ((const_prefix ^ app_op_name, 2), metis_app_op)]
+  [((tptp_equal, 2), (metis_equal, false)),
+   ((tptp_old_equal, 2), (metis_equal, false)),
+   ((const_prefix ^ predicator_name, 1), (metis_predicator, false)),
+   ((const_prefix ^ app_op_name, 2), (metis_app_op, false)),
+   ((const_prefix ^ type_tag_name, 2), (metis_type_tag, true))]
 
 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   | predicate_of thy (t, pos) =
@@ -160,7 +163,7 @@
 
 (*The fully-typed translation, to avoid type errors*)
 fun tag_with_type tm T =
-  Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T])
+  Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T])
 
 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
     tag_with_type (Metis_Term.Var s) ty
@@ -283,15 +286,18 @@
   in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
 
 fun metis_name_from_atp s ary =
-  AList.lookup (op =) metis_name_table (s, ary) |> the_default s
+  AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false)
 fun metis_term_from_atp (ATerm (s, tms)) =
   if is_tptp_variable s then
     Metis_Term.Var s
   else
-    Metis_Term.Fn (metis_name_from_atp s (length tms),
-                   map metis_term_from_atp tms)
-fun metis_atom_from_atp (AAtom (ATerm (s, tms))) =
-    (metis_name_from_atp s (length tms), map metis_term_from_atp tms)
+    let val (s, swap) = metis_name_from_atp s (length tms) in
+      Metis_Term.Fn (s, tms |> map metis_term_from_atp |> swap ? rev)
+    end
+fun metis_atom_from_atp (AAtom tm) =
+    (case metis_term_from_atp tm of
+       Metis_Term.Fn x => x
+     | _ => raise Fail "non CNF -- expected function")
   | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
 fun metis_literal_from_atp (AConn (ANot, [phi])) =
     (false, metis_atom_from_atp phi)