# HG changeset patch
# User blanchet
# Date 1315423881 -7200
# Node ID 52318464c73b850f57b5e3810ddf2d2836210905
# Parent  d7094cae7df451bad264b6eff45c93646b8e827c
also implemented ghost version of the tagged encodings

diff -r d7094cae7df4 -r 52318464c73b src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
@@ -1094,28 +1094,31 @@
       t
     else
       let
-        fun aux Ts t =
+        fun trans Ts t =
           case t of
-            @{const Not} $ t1 => @{const Not} $ aux Ts t1
+            @{const Not} $ t1 => @{const Not} $ trans Ts t1
           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
-            t0 $ Abs (s, T, aux (T :: Ts) t')
+            t0 $ Abs (s, T, trans (T :: Ts) t')
           | (t0 as Const (@{const_name All}, _)) $ t1 =>
-            aux Ts (t0 $ eta_expand Ts t1 1)
+            trans Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
-            t0 $ Abs (s, T, aux (T :: Ts) t')
+            t0 $ Abs (s, T, trans (T :: Ts) t')
           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
-            aux Ts (t0 $ eta_expand Ts t1 1)
-          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+            trans Ts (t0 $ eta_expand Ts t1 1)
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
+            t0 $ trans Ts t1 $ trans Ts t2
+          | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
+            t0 $ trans Ts t1 $ trans Ts t2
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
+            t0 $ trans Ts t1 $ trans Ts t2
           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
-            t0 $ aux Ts t1 $ aux Ts t2
+            t0 $ trans Ts t1 $ trans Ts t2
           | _ =>
             if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
             else t |> Envir.eta_contract |> do_lambdas ctxt Ts
         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
-      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+      in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
   end
 
 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
@@ -1153,12 +1156,12 @@
    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
 fun freeze_term t =
   let
-    fun aux (t $ u) = aux t $ aux u
-      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
-      | aux (Var ((s, i), T)) =
+    fun freeze (t $ u) = freeze t $ freeze u
+      | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
+      | freeze (Var ((s, i), T)) =
         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
-      | aux t = t
-  in t |> exists_subterm is_Var t ? aux end
+      | freeze t = t
+  in t |> exists_subterm is_Var t ? freeze end
 
 fun presimp_prop ctxt presimp_consts t =
   let
@@ -1203,6 +1206,30 @@
 
 (** Finite and infinite type inference **)
 
+fun tvar_footprint thy s ary =
+  (case strip_prefix_and_unascii const_prefix s of
+     SOME s =>
+     s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
+       |> map (fn T => Term.add_tvarsT T [] |> map fst)
+   | NONE => [])
+  handle TYPE _ => []
+
+fun ghost_type_args thy s ary =
+  let
+    val footprint = tvar_footprint thy s ary
+    fun ghosts _ [] = []
+      | ghosts seen ((i, tvars) :: args) =
+        ghosts (union (op =) seen tvars) args
+        |> exists (not o member (op =) seen) tvars ? cons i
+  in
+    if forall null footprint then
+      []
+    else
+      0 upto length footprint - 1 ~~ footprint
+      |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
+      |> ghosts []
+  end
+
 type monotonicity_info =
   {maybe_finite_Ts : typ list,
    surely_finite_Ts : typ list,
@@ -1256,15 +1283,21 @@
 datatype tag_site =
   Top_Level of bool option |
   Eq_Arg of bool option |
+  Arg of string * int |
   Elsewhere
 
 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
-    (if granularity_of_type_level level = All_Vars then
-       should_encode_type ctxt mono level T
-     else case (site, is_maybe_universal_var u) of
-       (Eq_Arg _, true) => should_encode_type ctxt mono level T
-     | _ => false)
+    (case granularity_of_type_level level of
+       All_Vars => should_encode_type ctxt mono level T
+     | grain =>
+       case (site, is_maybe_universal_var u) of
+         (Eq_Arg _, true) => should_encode_type ctxt mono level T
+       | (Arg (s, j), true) =>
+         grain = Ghost_Type_Arg_Vars andalso
+         member (op =)
+                (ghost_type_args (Proof_Context.theory_of ctxt) s (j + 1)) j
+       | _ => false)
   | should_tag_with_type _ _ _ _ _ _ = false
 
 fun fused_type ctxt mono level =
@@ -1653,30 +1686,6 @@
     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   | is_var_positively_naked_in_term _ _ _ _ = true
 
-fun tvar_footprint thy s ary =
-  (case strip_prefix_and_unascii const_prefix s of
-     SOME s =>
-     s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
-       |> map (fn T => Term.add_tvarsT T [] |> map fst)
-   | NONE => [])
-  handle TYPE _ => []
-
-fun ghost_type_args thy s ary =
-  let
-    val footprint = tvar_footprint thy s ary
-    fun ghosts _ [] = []
-      | ghosts seen ((i, tvars) :: args) =
-        ghosts (union (op =) seen tvars) args
-        |> exists (not o member (op =) seen) tvars ? cons i
-  in
-    if forall null footprint then
-      []
-    else
-      0 upto length footprint - 1 ~~ footprint
-      |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
-      |> ghosts []
-  end
-
 fun is_var_ghost_type_arg_in_term thy name pos tm accum =
   is_var_positively_naked_in_term name pos tm accum orelse
   let
@@ -1721,27 +1730,29 @@
        | _ => raise Fail "unexpected lambda-abstraction")
 and ho_term_from_iterm ctxt format mono type_enc =
   let
-    fun aux site u =
+    fun term site u =
       let
         val (head, args) = strip_iterm_comb u
         val pos =
           case site of
             Top_Level pos => pos
           | Eq_Arg pos => pos
-          | Elsewhere => NONE
+          | _ => NONE
         val t =
           case head of
             IConst (name as (s, _), _, T_args) =>
             let
-              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
+              fun arg_site j =
+                if is_tptp_equal s then Eq_Arg pos else Arg (s, j)
             in
-              mk_aterm format type_enc name T_args (map (aux arg_site) args)
+              mk_aterm format type_enc name T_args
+                       (map2 (term o arg_site) (0 upto length args - 1) args)
             end
           | IVar (name, _) =>
-            mk_aterm format type_enc name [] (map (aux Elsewhere) args)
+            mk_aterm format type_enc name [] (map (term Elsewhere) args)
           | IAbs ((name, T), tm) =>
             AAbs ((name, ho_type_from_typ format type_enc true 0 T),
-                  aux Elsewhere tm)
+                  term Elsewhere tm)
           | IApp _ => raise Fail "impossible \"IApp\""
         val T = ityp_of u
       in
@@ -1750,7 +1761,7 @@
               else
                 I)
       end
-  in aux end
+  in term end
 and formula_from_iformula ctxt format mono type_enc should_guard_var =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -2087,9 +2098,7 @@
       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
       else (Axiom, I)
     val (arg_Ts, res_T) = chop_fun ary T
-    val num_args = length arg_Ts
-    val bound_names =
-      1 upto num_args |> map (`I o make_bound_var o string_of_int)
+    val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
     val bounds =
       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
     val bound_Ts =
@@ -2100,12 +2109,12 @@
           if granularity_of_type_level level = Ghost_Type_Arg_Vars then
             let val ghosts = ghost_type_args thy s ary in
               map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
-                   (0 upto num_args - 1) arg_Ts
+                   (0 upto ary - 1) arg_Ts
             end
           else
-            replicate num_args NONE
+            replicate ary NONE
       else
-        replicate num_args NONE
+        replicate ary NONE
   in
     Formula (guards_sym_formula_prefix ^ s ^
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
@@ -2124,6 +2133,9 @@
 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
+    val thy = Proof_Context.theory_of ctxt
+    val level = level_of_type_enc type_enc
+    val grain = granularity_of_type_level level
     val ident_base =
       tags_sym_formula_prefix ^ s ^
       (if n > 1 then "_" ^ string_of_int j else "")
@@ -2131,19 +2143,28 @@
       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
       else (Axiom, I)
     val (arg_Ts, res_T) = chop_fun ary T
-    val bound_names =
-      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
+    val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
     val bounds = bound_names |> map (fn name => ATerm (name, []))
     val cst = mk_aterm format type_enc (s, s') T_args
     val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
-    val should_encode =
-      should_encode_type ctxt mono (level_of_type_enc type_enc)
+    val should_encode = should_encode_type ctxt mono level
     val tag_with = tag_with_type ctxt format mono type_enc NONE
     val add_formula_for_res =
       if should_encode res_T then
-        cons (Formula (ident_base ^ "_res", kind,
-                       eq (tag_with res_T (cst bounds)) (cst bounds),
-                       isabelle_info simpN, NONE))
+        let
+          val tagged_bounds =
+            if grain = Ghost_Type_Arg_Vars then
+              let val ghosts = ghost_type_args thy s ary in
+                map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
+                     (0 upto ary - 1 ~~ arg_Ts) bounds
+              end
+            else
+              bounds
+        in
+          cons (Formula (ident_base ^ "_res", kind,
+                         eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
+                         isabelle_info simpN, NONE))
+        end
       else
         I
     fun add_formula_for_arg k =
@@ -2161,7 +2182,8 @@
       end
   in
     [] |> not pred_sym ? add_formula_for_res
-       |> Config.get ctxt type_tag_arguments
+       |> (Config.get ctxt type_tag_arguments andalso
+           grain = Positively_Naked_Vars)
           ? fold add_formula_for_arg (ary - 1 downto 0)
   end