# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 8ea9c6fa8b53d8aee8717166f23cb87cf8aa7a10
# Parent  d83802e7348e9bd39743724a094f93b2bdf7f162
fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP

diff -r d83802e7348e -r 8ea9c6fa8b53 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
@@ -171,6 +171,7 @@
       | keep (c :: cs) = c :: keep cs
   in String.explode #> rev #> keep #> rev #> String.implode end
 
+(* Long names can slow down the ATPs. *)
 val max_readable_name_size = 20
 
 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
diff -r d83802e7348e -r 8ea9c6fa8b53 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu May 12 15:29:19 2011 +0200
@@ -357,7 +357,9 @@
               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
           end
         | SOME s =>
-          let val (s', mangled_us) = s |> unmangled_const |>> invert_const in
+          let
+            val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
+          in
             if s' = type_tag_name then
               case mangled_us @ us of
                 [typ_u, term_u] =>
@@ -380,14 +382,12 @@
                 val term_ts = map (aux NONE []) term_us
                 val extra_ts = map (aux NONE []) extra_us
                 val T =
-                  case opt_T of
-                    SOME T => map fastype_of term_ts ---> T
-                  | NONE =>
-                    if num_type_args thy s' = length type_us then
-                      Sign.const_instance thy
-                          (s', map (typ_from_fo_term tfrees) type_us)
-                    else
-                      HOLogic.typeT
+                  if num_type_args thy s' = length type_us then
+                    Sign.const_instance thy
+                        (s', map (typ_from_fo_term tfrees) type_us)
+                  else case opt_T of
+                    SOME T => map fastype_of (term_ts @ extra_ts) ---> T
+                  | NONE => HOLogic.typeT
                 val s' = s' |> unproxify_const
               in list_comb (Const (s', T), term_ts @ extra_ts) end
           end
@@ -424,14 +424,17 @@
    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
 
-fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
-  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
-  | uncombine_term (t as Const (x as (s, _))) =
-    (case AList.lookup (op =) combinator_table s of
-       SOME thm => thm |> prop_of |> specialize_type @{theory} x
-                       |> Logic.dest_equals |> snd
-     | NONE => t)
-  | uncombine_term t = t
+fun uncombine_term thy =
+  let
+    fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
+      | aux (Abs (s, T, t')) = Abs (s, T, aux t')
+      | aux (t as Const (x as (s, _))) =
+        (case AList.lookup (op =) combinator_table s of
+           SOME thm => thm |> prop_of |> specialize_type thy x
+                           |> Logic.dest_equals |> snd
+         | NONE => t)
+      | aux t = t
+  in aux end
 
 (* Update schematic type variables with detected sort constraints. It's not
    totally clear whether this code is necessary. *)
@@ -487,8 +490,8 @@
 
 fun check_formula ctxt =
   Type.constraint HOLogic.boolT
-  #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-
+  #> Syntax.check_term
+         (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
 
 (**** Translation of TSTP files to Isar Proofs ****)
 
@@ -505,7 +508,7 @@
       val t2 = prop_from_formula thy sym_tab tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
-        |> unvarify_args |> uncombine_term |> check_formula ctxt
+        |> unvarify_args |> uncombine_term thy |> check_formula ctxt
         |> HOLogic.dest_eq
     in
       (Definition (name, t1, t2),
@@ -515,7 +518,7 @@
     let
       val thy = Proof_Context.theory_of ctxt
       val t = u |> prop_from_formula thy sym_tab tfrees
-                |> uncombine_term |> check_formula ctxt
+                |> uncombine_term thy |> check_formula ctxt
     in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
@@ -910,10 +913,10 @@
 
 fun string_for_proof ctxt0 i n =
   let
-    val ctxt = ctxt0
-      |> Config.put show_free_types false
-      |> Config.put show_types true
-      |> Config.put show_sorts true
+    val ctxt =
+      ctxt0 |> Config.put show_free_types false
+            |> Config.put show_types true
+            |> Config.put show_sorts true
     fun fix_print_mode f x =
       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                                (print_mode_value ())) f x
diff -r d83802e7348e -r 8ea9c6fa8b53 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -269,7 +269,8 @@
 
 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   | generic_mangled_type_name f (ATerm (name, tys)) =
-    f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
+    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
+    ^ ")"
 val mangled_type_name =
   fo_term_from_typ
   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),