# HG changeset patch
# User blanchet
# Date 1324476268 -3600
# Node ID aa8100cc02dc531893cba852ab290a659cdc08b0
# Parent  e586f6d136b7b0aa1b4afed3f3e8620e9ab4ceac
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")

diff -r e586f6d136b7 -r aa8100cc02dc src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 21 14:38:21 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 21 15:04:28 2011 +0100
@@ -743,7 +743,7 @@
   Mangled_Type_Args |
   No_Type_Args
 
-fun type_arg_policy type_enc s =
+fun type_arg_policy monom_constrs type_enc s =
   let val poly = polymorphism_of_type_enc type_enc in
     if s = type_tag_name then
       if poly = Mangled_Monomorphic then Mangled_Type_Args
@@ -758,6 +758,9 @@
           No_Type_Args
         else if poly = Mangled_Monomorphic then
           Mangled_Type_Args
+        else if member (op =) monom_constrs s andalso
+                granularity_of_type_level level = Positively_Naked_Vars then
+          No_Type_Args
         else
           Explicit_Type_Args
               (level = All_Types orelse
@@ -986,7 +989,7 @@
           (case unprefix_and_unascii const_prefix s of
              NONE => tm
            | SOME s'' =>
-             case type_arg_policy type_enc (invert_const s'') of
+             case type_arg_policy [] type_enc (invert_const s'') of
                Mangled_Type_Args =>
                IConst (mangled_const_name format type_enc T_args name, T, [])
              | _ => tm)
@@ -1014,7 +1017,7 @@
     end
     handle TYPE _ => T_args
 
-fun filter_type_args_in_iterm thy type_enc =
+fun filter_type_args_in_iterm thy monom_constrs type_enc =
   let
     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
       | filt _ (tm as IConst (_, _, [])) = tm
@@ -1032,7 +1035,7 @@
              fun filter_T_args false = T_args
                | filter_T_args true = filter_const_type_args thy s'' ary T_args
            in
-             case type_arg_policy type_enc s'' of
+             case type_arg_policy monom_constrs type_enc s'' of
                Explicit_Type_Args infer_from_term_args =>
                (name, filter_T_args infer_from_term_args)
              | No_Type_Args => (name, [])
@@ -1246,6 +1249,8 @@
    | NONE => [])
   handle TYPE _ => []
 
+(* TODO: Shouldn't both arguments of equality be ghosts, since it is
+   symmetric? *)
 fun ghost_type_args thy s ary =
   let
     val footprint = tvar_footprint thy s ary
@@ -1489,7 +1494,7 @@
 fun list_app head args = fold (curry (IApp o swap)) args head
 fun predicator tm = IApp (predicator_combconst, tm)
 
-fun firstorderize_fact thy format type_enc sym_tab =
+fun firstorderize_fact thy monom_constrs format type_enc sym_tab =
   let
     fun do_app arg head =
       let
@@ -1516,7 +1521,7 @@
     val do_iterm =
       not (is_type_enc_higher_order type_enc)
       ? (introduce_app_ops #> introduce_predicators)
-      #> filter_type_args_in_iterm thy type_enc
+      #> filter_type_args_in_iterm thy monom_constrs type_enc
   in update_iformula (formula_map do_iterm) end
 
 (** Helper facts **)
@@ -2006,7 +2011,7 @@
       let
         val (s, s') =
           `(make_fixed_const NONE) @{const_name undefined}
-          |> (case type_arg_policy type_enc @{const_name undefined} of
+          |> (case type_arg_policy [] type_enc @{const_name undefined} of
                 Mangled_Type_Args => mangled_const_name format type_enc [T]
               | _ => I)
       in
@@ -2390,6 +2395,28 @@
       |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
   in (implicit_declsN, decls) :: problem end
 
+fun exists_subdtype P =
+  let
+    fun ex U = P U orelse
+      (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
+  in ex end
+
+fun is_poly_constr (_, Us) =
+  exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
+
+fun all_monomorphic_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
+
+(* Forcing explicit applications is expensive for polymorphic encodings, because
+   it takes only one existential variable ranging over "'a => 'b" to ruin
+   everything. Hence we do it only if there are few facts (is normally the case
+   for "metis" and the minimizer. *)
 val explicit_apply_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
@@ -2397,9 +2424,6 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
-    (* Forcing explicit applications is expensive for polymorphic encodings,
-       because it takes only one existential variable ranging over "'a => 'b" to
-       ruin everything. Hence we do it only if there are few facts. *)
     val explicit_apply =
       if polymorphism_of_type_enc type_enc <> Polymorphic orelse
          length facts <= explicit_apply_threshold then
@@ -2419,7 +2443,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 firstorderize = firstorderize_fact thy format type_enc sym_tab
+    val monom_constrs = all_monomorphic_constrs_of_polymorphic_datatypes thy
+    val firstorderize =
+      firstorderize_fact thy monom_constrs format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
     val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
     val helpers =