# 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 =