# HG changeset patch
# User blanchet
# Date 1314308289 -7200
# Node ID 5bde887b47858e0fff2c795f18618f8479448a64
# Parent  dbd98b5495978b8e35b0227f8ac2a1f48c640d55
make polymorphic encodings more complete

diff -r dbd98b549597 -r 5bde887b4785 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 22:06:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 23:38:09 2011 +0200
@@ -202,10 +202,10 @@
 
 fun formula_fold pos f =
   let
-    fun aux pos (AQuant (_, _, phi)) = aux pos phi
-      | aux pos (AConn conn) = aconn_fold pos aux conn
-      | aux pos (AAtom tm) = f pos tm
-  in aux pos end
+    fun fld pos (AQuant (_, _, phi)) = fld pos phi
+      | fld pos (AConn conn) = aconn_fold pos fld conn
+      | fld pos (AAtom tm) = f pos tm
+  in fld pos end
 
 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
diff -r dbd98b549597 -r 5bde887b4785 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:06:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:38:09 2011 +0200
@@ -1020,7 +1020,7 @@
 fun preprocess_abstractions_in_terms trans_lambdas facts =
   let
     val (facts, lambda_ts) =
-      facts |> map (snd o snd) |> trans_lambdas 
+      facts |> map (snd o snd) |> trans_lambdas
             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
     val lambda_facts =
       map2 (fn t => fn j =>
@@ -1246,8 +1246,8 @@
       end
   in add true end
 fun add_fact_syms_to_table ctxt explicit_apply =
-  formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
-  |> fact_lift
+  K (add_iterm_syms_to_table ctxt explicit_apply)
+  |> formula_fold NONE |> fact_lift
 
 val tvar_a = TVar (("'a", 0), HOLogic.typeS)
 
@@ -1789,7 +1789,7 @@
         #> fold (add_iterm_syms in_conj) args
       end
     fun add_fact_syms in_conj =
-      fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
+      K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
     fun add_formula_var_types (AQuant (_, xs, phi)) =
         fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
         #> add_formula_var_types phi
@@ -1885,6 +1885,22 @@
        ? fold (add_fact_mononotonicity_info ctxt level) facts
   end
 
+fun add_iformula_monotonic_types ctxt mono type_enc =
+  let
+    val level = level_of_type_enc type_enc
+    val should_encode = should_encode_type ctxt mono level
+    fun add_type T = should_encode T ? insert_type ctxt I T
+    fun add_term (tm as IApp (tm1, tm2)) =
+        add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
+      | add_term tm = add_type (ityp_of tm)
+  in formula_fold NONE (K add_term) end
+fun add_fact_monotonic_types ctxt mono type_enc =
+  add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
+fun monotonic_types_for_facts ctxt mono type_enc facts =
+  [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
+         is_type_level_monotonicity_based (level_of_type_enc type_enc))
+        ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
+
 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
   Formula (guards_sym_formula_prefix ^
            ascii_of (mangled_type format type_enc T),
@@ -2046,17 +2062,9 @@
        end)
 
 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
-                                     sym_decl_tab =
+                                     mono_Ts sym_decl_tab =
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
-    val mono_Ts =
-      if polymorphism_of_type_enc type_enc = Polymorphic then
-        syms |> maps (map result_type_of_decl o snd)
-             |> filter_out (should_encode_type ctxt mono
-                                (level_of_type_enc type_enc))
-             |> rpair [] |-> fold (insert_type ctxt I)
-      else
-        []
     val mono_lines =
       problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
     val decl_lines =
@@ -2131,11 +2139,14 @@
     val helpers =
       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
                        |> map repair
+    val mono_Ts =
+      helpers @ conjs @ facts
+      |> monotonic_types_for_facts ctxt mono type_enc
     val sym_decl_lines =
       (conjs, helpers @ facts)
       |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
-                                               type_enc
+                                               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