1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
     1.3 @@ -580,11 +580,8 @@
     1.4           case (core, (poly, level, heaviness)) of
     1.5             ("simple", (NONE, _, Lightweight)) => Simple_Types level
     1.6           | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
     1.7 -         | ("tags", (SOME Polymorphic, All_Types, _)) =>
     1.8 -           Tags (Polymorphic, All_Types, heaviness)
     1.9           | ("tags", (SOME Polymorphic, _, _)) =>
    1.10 -           (* The actual light encoding is very unsound. *)
    1.11 -           Tags (Polymorphic, level, Heavyweight)
    1.12 +           Tags (Polymorphic, level, heaviness)
    1.13           | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
    1.14           | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
    1.15             Preds (poly, Const_Arg_Types, Lightweight)
    1.16 @@ -1039,15 +1036,26 @@
    1.17    | is_var_or_bound_var (CombVar _) = true
    1.18    | is_var_or_bound_var _ = false
    1.19  
    1.20 -datatype tag_site = Top_Level | Eq_Arg | Elsewhere
    1.21 +datatype tag_site =
    1.22 +  Top_Level of bool option |
    1.23 +  Eq_Arg of bool option |
    1.24 +  Elsewhere
    1.25  
    1.26 -fun should_tag_with_type _ _ _ Top_Level _ _ = false
    1.27 -  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
    1.28 +fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
    1.29 +  | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
    1.30 +                         u T =
    1.31      (case heaviness of
    1.32         Heavyweight => should_encode_type ctxt nonmono_Ts level T
    1.33       | Lightweight =>
    1.34         case (site, is_var_or_bound_var u) of
    1.35 -         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
    1.36 +         (Eq_Arg pos, true) =>
    1.37 +         (* The first disjunct prevents a subtle soundness issue explained in
    1.38 +            Blanchette's Ph.D. thesis. See also
    1.39 +            "formula_lines_for_lightweight_tags_sym_decl". *)
    1.40 +         (pos <> SOME false andalso poly = Polymorphic andalso
    1.41 +          level <> All_Types andalso heaviness = Lightweight andalso
    1.42 +          exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
    1.43 +         should_encode_type ctxt nonmono_Ts level T
    1.44         | _ => false)
    1.45    | should_tag_with_type _ _ _ _ _ _ = false
    1.46  
    1.47 @@ -1466,10 +1474,10 @@
    1.48  fun mk_const_aterm format type_sys x T_args args =
    1.49    ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args)
    1.50  
    1.51 -fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
    1.52 +fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
    1.53    CombConst (type_tag, T --> T, [T])
    1.54    |> enforce_type_arg_policy_in_combterm ctxt format type_sys
    1.55 -  |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
    1.56 +  |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
    1.57    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
    1.58  and term_from_combterm ctxt format nonmono_Ts type_sys =
    1.59    let
    1.60 @@ -1481,14 +1489,18 @@
    1.61              CombConst (name, _, T_args) => (name, T_args)
    1.62            | CombVar (name, _) => (name, [])
    1.63            | CombApp _ => raise Fail "impossible \"CombApp\""
    1.64 -        val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
    1.65 -                       else Elsewhere
    1.66 +        val (pos, arg_site) =
    1.67 +          case site of
    1.68 +            Top_Level pos =>
    1.69 +            (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
    1.70 +          | Eq_Arg pos => (pos, Elsewhere)
    1.71 +          | Elsewhere => (NONE, Elsewhere)
    1.72          val t = mk_const_aterm format type_sys x T_args
    1.73                      (map (aux arg_site) args)
    1.74          val T = combtyp_of u
    1.75        in
    1.76          t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
    1.77 -                tag_with_type ctxt format nonmono_Ts type_sys T
    1.78 +                tag_with_type ctxt format nonmono_Ts type_sys pos T
    1.79                else
    1.80                  I)
    1.81        end
    1.82 @@ -1496,7 +1508,8 @@
    1.83  and formula_from_combformula ctxt format nonmono_Ts type_sys
    1.84                               should_predicate_on_var =
    1.85    let
    1.86 -    val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
    1.87 +    fun do_term pos =
    1.88 +      term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
    1.89      val do_bound_type =
    1.90        case type_sys of
    1.91          Simple_Types level =>
    1.92 @@ -1508,7 +1521,7 @@
    1.93               (fn () => should_predicate_on_var pos phi universal name) T then
    1.94          CombVar (name, T)
    1.95          |> type_pred_combterm ctxt format type_sys T
    1.96 -        |> do_term |> AAtom |> SOME
    1.97 +        |> do_term pos |> AAtom |> SOME
    1.98        else
    1.99          NONE
   1.100      fun do_formula pos (AQuant (q, xs, phi)) =
   1.101 @@ -1527,7 +1540,7 @@
   1.102                        phi)
   1.103          end
   1.104        | do_formula pos (AConn conn) = aconn_map pos do_formula conn
   1.105 -      | do_formula _ (AAtom tm) = AAtom (do_term tm)
   1.106 +      | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   1.107    in do_formula o SOME end
   1.108  
   1.109  fun bound_tvars type_sys Ts =
   1.110 @@ -1736,8 +1749,14 @@
   1.111        |> bound_tvars type_sys atomic_Ts
   1.112        |> close_formula_universally
   1.113        |> maybe_negate
   1.114 -    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
   1.115 -    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
   1.116 +    (* See also "should_tag_with_type". *)
   1.117 +    fun should_encode T =
   1.118 +      should_encode_type ctxt nonmono_Ts All_Types T orelse
   1.119 +      (case type_sys of
   1.120 +         Tags (Polymorphic, level, Lightweight) =>
   1.121 +         level <> All_Types andalso Monomorph.typ_has_tvars T
   1.122 +       | _ => false)
   1.123 +    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys NONE
   1.124      val add_formula_for_res =
   1.125        if should_encode res_T then
   1.126          cons (Formula (ident_base ^ "_res", kind,