# HG changeset patch
# User blanchet
# Date 1324476268 -3600
# Node ID 7eccf8147f5764a2ce69b7fce5e3a0b6483a1669
# Parent  428db0387f320486ca767574c9e63970cadbd278
treat polymorphic constructors specially in @? encodings

diff -r 428db0387f32 -r 7eccf8147f57 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 21 15:04:28 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 21 15:04:28 2011 +0100
@@ -1317,26 +1317,33 @@
   | is_maybe_universal_var (IVar _) = true
   | is_maybe_universal_var _ = false
 
-datatype tag_site =
+datatype site =
   Top_Level of bool option |
   Eq_Arg of bool option |
   Arg of string * int * int |
   Elsewhere
 
-fun should_tag_with_type _ _ _ [Top_Level _] _ _ = false
-  | should_tag_with_type ctxt mono (Tags (_, level)) sites u T =
+fun should_tag_with_type _ _ _ _ [Top_Level _] _ _ = false
+  | should_tag_with_type ctxt polym_constrs mono (Tags (_, level)) sites u T =
     (case granularity_of_type_level level of
        All_Vars => should_encode_type ctxt mono level T
      | grain =>
-       case (hd sites, is_maybe_universal_var u) of
-         (Eq_Arg _, true) => should_encode_type ctxt mono level T
-       | (Arg (s, j, ary), true) =>
-         let val thy = Proof_Context.theory_of ctxt in
-           grain = Ghost_Type_Arg_Vars andalso
-           member (op =) (ghost_type_args thy s ary) j
+       case (sites, is_maybe_universal_var u) of
+         (Eq_Arg _ :: _, true) => should_encode_type ctxt mono level T
+       | (Arg (s, j, ary) :: site0 :: _, true) =>
+         grain = Ghost_Type_Arg_Vars andalso
+         let
+           val thy = Proof_Context.theory_of ctxt
+           fun is_ghost_type_arg s j ary =
+             member (op =) (ghost_type_args thy s ary) j
+           fun is_ghost_site (Arg (s, j, ary)) = is_ghost_type_arg s j ary
+             | is_ghost_site _ = true
+         in
+           is_ghost_type_arg s j ary andalso
+           (not (member (op =) polym_constrs s) orelse is_ghost_site site0)
          end
        | _ => false)
-  | should_tag_with_type _ _ _ _ _ _ = false
+  | should_tag_with_type _ _ _ _ _ _ _ = false
 
 fun fused_type ctxt mono level =
   let
@@ -1803,13 +1810,13 @@
 fun mk_aterm format type_enc name T_args args =
   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
 
-fun tag_with_type ctxt format mono type_enc pos T tm =
+fun tag_with_type ctxt polym_constrs format mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
   |> mangle_type_args_in_iterm format type_enc
-  |> ho_term_from_iterm ctxt format mono type_enc pos
+  |> ho_term_from_iterm ctxt polym_constrs format mono type_enc pos
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt format mono type_enc =
+and ho_term_from_iterm ctxt polym_constrs format mono type_enc =
   let
     fun term sites u =
       let
@@ -1839,17 +1846,18 @@
           | IApp _ => raise Fail "impossible \"IApp\""
         val T = ityp_of u
       in
-        t |> (if should_tag_with_type ctxt mono type_enc sites u T then
-                tag_with_type ctxt format mono type_enc pos T
-              else
-                I)
+        if should_tag_with_type ctxt polym_constrs mono type_enc sites u T then
+          tag_with_type ctxt polym_constrs format mono type_enc pos T t
+        else
+          t
       end
   in term o single o Top_Level end
-and formula_from_iformula ctxt format mono type_enc should_guard_var =
+and formula_from_iformula ctxt polym_constrs format mono type_enc
+                          should_guard_var =
   let
     val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
-    val do_term = ho_term_from_iterm ctxt format mono type_enc
+    val do_term = ho_term_from_iterm ctxt polym_constrs format mono type_enc
     val do_bound_type =
       case type_enc of
         Simple_Types _ => fused_type ctxt mono level 0
@@ -1864,7 +1872,7 @@
       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
         let
           val var = ATerm (name, [])
-          val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
+          val tagged_var = tag_with_type ctxt [] format mono type_enc pos T var
         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
       else
         NONE
@@ -1890,13 +1898,12 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
-                          (j, {name, locality, kind, iformula, atomic_types}) =
+fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
+        mono type_enc (j, {name, locality, kind, iformula, atomic_types}) =
   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
    iformula
-   |> formula_from_iformula ctxt format mono type_enc
-                            should_guard_var_in_formula
-                            (if pos then SOME true else NONE)
+   |> formula_from_iformula ctxt polym_constrs format mono type_enc
+          should_guard_var_in_formula (if pos then SOME true else NONE)
    |> close_formula_universally
    |> bound_tvars type_enc true atomic_types,
    NONE,
@@ -1932,11 +1939,11 @@
                   (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
            isabelle_info format introN, NONE)
 
-fun formula_line_for_conjecture ctxt format mono type_enc
+fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
            iformula
-           |> formula_from_iformula ctxt format mono type_enc
+           |> formula_from_iformula ctxt polym_constrs format mono type_enc
                   should_guard_var_in_formula (SOME false)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types, NONE, NONE)
@@ -2133,7 +2140,7 @@
            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm format type_enc T
            |> AAtom
-           |> formula_from_iformula ctxt format mono type_enc
+           |> formula_from_iformula ctxt [] format mono type_enc
                                     (K (K (K (K (K (K true)))))) (SOME true)
            |> close_formula_universally
            |> bound_tvars type_enc true (atomic_types_of T),
@@ -2145,8 +2152,8 @@
              ascii_of (mangled_type format type_enc T),
              Axiom,
              eq_formula type_enc (atomic_types_of T) false
-                        (tag_with_type ctxt format mono type_enc NONE T x_var)
-                        x_var,
+                  (tag_with_type ctxt [] format mono type_enc NONE T x_var)
+                  x_var,
              isabelle_info format simpN, NONE)
   end
 
@@ -2211,7 +2218,7 @@
              |> fold (curry (IApp o swap)) bounds
              |> type_guard_iterm format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_iformula ctxt format mono type_enc
+             |> formula_from_iformula ctxt [] format mono type_enc
                                       (K (K (K (K (K (K true)))))) (SOME true)
              |> close_formula_universally
              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
@@ -2237,7 +2244,7 @@
     val cst = mk_aterm format type_enc (s, s') T_args
     val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
     val should_encode = should_encode_type ctxt mono level
-    val tag_with = tag_with_type ctxt format mono type_enc NONE
+    val tag_with = tag_with_type ctxt [] format mono type_enc NONE
     val add_formula_for_res =
       if should_encode res_T then
         let
@@ -2324,7 +2331,7 @@
       problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
     val decl_lines =
       fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
-                                                     mono type_enc)
+                             mono type_enc)
                syms []
   in mono_lines @ decl_lines end
 
@@ -2407,14 +2414,14 @@
 fun is_poly_constr (_, Us) =
   exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
 
-fun all_monomorphic_constrs_of_polymorphic_datatypes thy =
+fun all_constrs_of_polymorphic_datatypes thy =
   Symtab.fold (snd
                #> #descr
                #> maps (snd #> #3)
                #> (fn cs => exists is_poly_constr cs ? append cs))
               (Datatype.get_all thy) []
-  |> filter_out is_poly_constr
-  |> map fst
+  |> List.partition is_poly_constr
+  |> pairself (map fst)
 
 (* Forcing explicit applications is expensive for polymorphic encodings, because
    it takes only one existential variable ranging over "'a => 'b" to ruin
@@ -2446,7 +2453,9 @@
                          concl_t facts
     val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
-    val monom_constrs = all_monomorphic_constrs_of_polymorphic_datatypes thy
+    val (polym_constrs, monom_constrs) =
+      all_constrs_of_polymorphic_datatypes thy
+      |>> map (make_fixed_const (SOME format))
     val firstorderize =
       firstorderize_fact thy monom_constrs format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
@@ -2464,8 +2473,8 @@
                                                type_enc mono_Ts
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
-      |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
-                                    type_enc)
+      |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
+                                    false true mono type_enc)
       |> (if needs_type_tag_idempotence ctxt type_enc then
             cons (type_tag_idempotence_fact format type_enc)
           else
@@ -2475,8 +2484,8 @@
     val problem =
       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
        (factsN,
-        map (formula_line_for_fact ctxt format fact_prefix ascii_of
-                                   (not exporter) (not exporter) mono type_enc)
+        map (formula_line_for_fact ctxt polym_constrs format fact_prefix
+                 ascii_of (not exporter) (not exporter) mono type_enc)
             (0 upto length facts - 1 ~~ facts)),
        (class_relsN,
         map (formula_line_for_class_rel_clause format type_enc)
@@ -2485,7 +2494,8 @@
         map (formula_line_for_arity_clause format type_enc) arity_clauses),
        (helpersN, helper_lines),
        (conjsN,
-        map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
+        map (formula_line_for_conjecture ctxt polym_constrs format mono
+                                         type_enc) conjs),
        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
     val problem =
       problem