src/HOL/Tools/ATP/atp_problem.ML

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -28,7 +28,7 @@
      gen_prec : bool,
      gen_simp : bool}
 
-  datatype polymorphism = Monomorphic | Polymorphic
+  datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
   datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
   datatype thf_choice = THF_Without_Choice | THF_With_Choice
   datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -39,7 +39,7 @@
     FOF |
     TFF of polymorphism * tptp_explicitness |
     THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
-    DFG
+    DFG of polymorphism
 
   datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
@@ -160,7 +160,7 @@
    gen_prec : bool,
    gen_simp : bool}
 
-datatype polymorphism = Monomorphic | Polymorphic
+datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
 datatype thf_choice = THF_Without_Choice | THF_With_Choice
 datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -171,7 +171,7 @@
   FOF |
   TFF of polymorphism * tptp_explicitness |
   THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
-  DFG
+  DFG of polymorphism
 
 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
@@ -306,7 +306,7 @@
   | is_format_higher_order _ = false
 fun is_format_typed (TFF _) = true
   | is_format_typed (THF _) = true
-  | is_format_typed DFG = true
+  | is_format_typed (DFG _) = true
   | is_format_typed _ = false
 
 fun tptp_string_for_role Axiom = "axiom"
@@ -336,7 +336,7 @@
 
 fun str_for_type format ty =
   let
-    val dfg = (format = DFG)
+    val dfg = case format of DFG _ => true | _ => false
     fun str _ (AType (s, [])) =
         if dfg andalso s = tptp_individual_type then dfg_individual_type else s
       | str _ (AType (s, tys)) =
@@ -438,7 +438,7 @@
   | tptp_string_for_format FOF = tptp_fof
   | tptp_string_for_format (TFF _) = tptp_tff
   | tptp_string_for_format (THF _) = tptp_thf
-  | tptp_string_for_format DFG = raise Fail "non-TPTP format"
+  | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
 
 fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
     tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
@@ -464,7 +464,7 @@
 fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
   | binder_atypes _ = []
 
-fun dfg_string_for_formula gen_simp info =
+fun dfg_string_for_formula poly gen_simp info =
   let
     fun suffix_tag top_level s =
       if top_level then
@@ -492,7 +492,7 @@
       | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
     fun str_for_formula top_level (AQuant (q, xs, phi)) =
         str_for_quant q ^ "(" ^ "[" ^
-        commas (map (string_for_bound_var DFG) xs) ^ "], " ^
+        commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
         str_for_formula top_level phi ^ ")"
       | str_for_formula top_level (AConn (c, phis)) =
         str_for_conn top_level c ^ "(" ^
@@ -503,19 +503,19 @@
 fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
   | maybe_enclose bef aft s = bef ^ s ^ aft
 
-fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
+fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
   let
     fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
     fun ary sym = curry spair sym o arity_of_type
     fun fun_typ sym ty =
-      "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")."
+      "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")."
     fun pred_typ sym ty =
       "predicate(" ^
-      commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")."
+      commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")."
     fun formula pred (Formula (ident, kind, phi, _, info)) =
         if pred kind then
           let val rank = extract_isabelle_rank info in
-            "formula(" ^ dfg_string_for_formula gen_simp info phi ^
+            "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
             ", " ^ ident ^
             (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
             ")." |> SOME
@@ -587,7 +587,9 @@
 fun lines_for_atp_problem format ord ord_info problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
-  (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem
+  (case format of
+     DFG poly => dfg_lines poly ord ord_info
+   | _ => tptp_lines format) problem
 
 
 (** CNF (Metis) and CNF UEQ (Waldmeister) **)
@@ -787,7 +789,7 @@
     val avoid_clash =
       case format of
         TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
-      | DFG => avoid_clash_with_dfg_keywords
+      | DFG _ => avoid_clash_with_dfg_keywords
       | _ => I
     val nice_name = nice_name avoid_clash
     fun nice_type (AType (name, tys)) =