src/HOL/Tools/ATP/atp_translate.ML

--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
@@ -580,11 +580,8 @@
          case (core, (poly, level, heaviness)) of
            ("simple", (NONE, _, Lightweight)) => Simple_Types level
          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
-         | ("tags", (SOME Polymorphic, All_Types, _)) =>
-           Tags (Polymorphic, All_Types, heaviness)
          | ("tags", (SOME Polymorphic, _, _)) =>
-           (* The actual light encoding is very unsound. *)
-           Tags (Polymorphic, level, Heavyweight)
+           Tags (Polymorphic, level, heaviness)
          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
          | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
            Preds (poly, Const_Arg_Types, Lightweight)
@@ -1039,15 +1036,26 @@
   | is_var_or_bound_var (CombVar _) = true
   | is_var_or_bound_var _ = false
 
-datatype tag_site = Top_Level | Eq_Arg | Elsewhere
+datatype tag_site =
+  Top_Level of bool option |
+  Eq_Arg of bool option |
+  Elsewhere
 
-fun should_tag_with_type _ _ _ Top_Level _ _ = false
-  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
+fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
+  | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
+                         u T =
     (case heaviness of
        Heavyweight => should_encode_type ctxt nonmono_Ts level T
      | Lightweight =>
        case (site, is_var_or_bound_var u) of
-         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
+         (Eq_Arg pos, true) =>
+         (* The first disjunct prevents a subtle soundness issue explained in
+            Blanchette's Ph.D. thesis. See also
+            "formula_lines_for_lightweight_tags_sym_decl". *)
+         (pos <> SOME false andalso poly = Polymorphic andalso
+          level <> All_Types andalso heaviness = Lightweight andalso
+          exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
+         should_encode_type ctxt nonmono_Ts level T
        | _ => false)
   | should_tag_with_type _ _ _ _ _ _ = false
 
@@ -1466,10 +1474,10 @@
 fun mk_const_aterm format type_sys x T_args args =
   ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args)
 
-fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
+fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
   CombConst (type_tag, T --> T, [T])
   |> enforce_type_arg_policy_in_combterm ctxt format type_sys
-  |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
+  |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
 and term_from_combterm ctxt format nonmono_Ts type_sys =
   let
@@ -1481,14 +1489,18 @@
             CombConst (name, _, T_args) => (name, T_args)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
-        val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
-                       else Elsewhere
+        val (pos, arg_site) =
+          case site of
+            Top_Level pos =>
+            (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
+          | Eq_Arg pos => (pos, Elsewhere)
+          | Elsewhere => (NONE, Elsewhere)
         val t = mk_const_aterm format type_sys x T_args
                     (map (aux arg_site) args)
         val T = combtyp_of u
       in
         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
-                tag_with_type ctxt format nonmono_Ts type_sys T
+                tag_with_type ctxt format nonmono_Ts type_sys pos T
               else
                 I)
       end
@@ -1496,7 +1508,8 @@
 and formula_from_combformula ctxt format nonmono_Ts type_sys
                              should_predicate_on_var =
   let
-    val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
+    fun do_term pos =
+      term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
     val do_bound_type =
       case type_sys of
         Simple_Types level =>
@@ -1508,7 +1521,7 @@
              (fn () => should_predicate_on_var pos phi universal name) T then
         CombVar (name, T)
         |> type_pred_combterm ctxt format type_sys T
-        |> do_term |> AAtom |> SOME
+        |> do_term pos |> AAtom |> SOME
       else
         NONE
     fun do_formula pos (AQuant (q, xs, phi)) =
@@ -1527,7 +1540,7 @@
                       phi)
         end
       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
-      | do_formula _ (AAtom tm) = AAtom (do_term tm)
+      | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   in do_formula o SOME end
 
 fun bound_tvars type_sys Ts =
@@ -1736,8 +1749,14 @@
       |> bound_tvars type_sys atomic_Ts
       |> close_formula_universally
       |> maybe_negate
-    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
-    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
+    (* See also "should_tag_with_type". *)
+    fun should_encode T =
+      should_encode_type ctxt nonmono_Ts All_Types T orelse
+      (case type_sys of
+         Tags (Polymorphic, level, Lightweight) =>
+         level <> All_Types andalso Monomorph.typ_has_tvars T
+       | _ => false)
+    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys NONE
     val add_formula_for_res =
       if should_encode res_T then
         cons (Formula (ident_base ^ "_res", kind,