# HG changeset patch
# User blanchet
# Date 1340702080 -7200
# Node ID b755096701ec8b2d3d020d6f3f92255e8ed715ad
# Parent  cd4a4b9f1c76b44bd5bd94b336ad848f77be1a22
generate type classes for polymorphic DFG format (SPASS)

diff -r cd4a4b9f1c76 -r b755096701ec src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -494,6 +494,8 @@
 fun dfg_string_for_formula poly gen_simp info =
   let
     val str_for_typ = string_for_type (DFG poly)
+    fun str_for_bound_typ (ty, []) = str_for_typ ty
+      | str_for_bound_typ (ty, sorts) = str_for_typ ty ^ " : " ^ commas sorts
     fun suffix_tag top_level s =
       if top_level then
         case extract_isabelle_status info of
@@ -521,7 +523,7 @@
       | str_for_conn _ AImplies = "implies"
       | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
     fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
-        str_for_quant q ^ "_sorts([" ^ commas (map (str_for_typ o fst) xs) ^
+        str_for_quant q ^ "_sorts([" ^ commas (map str_for_bound_typ xs) ^
         "], " ^ str_for_formula top_level phi ^ ")"
       | str_for_formula top_level (AQuant (q, xs, phi)) =
         str_for_quant q ^ "([" ^
@@ -546,7 +548,6 @@
     fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
     fun pred_typ sym ty =
       let
-        val ((ty_vars, tys), _) = strip_atype ty
         val (ty_vars, tys) =
           strip_atype ty |> fst
           |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
diff -r cd4a4b9f1c76 -r b755096701ec src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -1739,12 +1739,17 @@
   case filter is_TVar Ts of
     [] => I
   | Ts =>
-    (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
-    #> (if is_type_enc_native type_enc then
-          mk_atyquant AForall
-              (map (fn TVar (x, S) =>
-                       (AType (tvar_name x, []), map (`make_type_class) S)) Ts)
-        else
+    ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic)
+       ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
+    #> (case type_enc of
+          Native (_, poly, _) =>
+          mk_atyquant AForall (map (fn TVar (x, S) =>
+                                       (AType (tvar_name x, []),
+                                        if poly = Type_Class_Polymorphic then
+                                          map (`make_type_class) S
+                                        else
+                                          [])) Ts)
+        | _ =>
           mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
 
 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =