1.1 --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
1.3 @@ -118,7 +118,7 @@
1.4 let
1.5 val thy = Proof_Context.theory_of ctxt
1.6 val prob_file = File.tmp_path (Path.explode "prob")
1.7 - val atp = if format = DFG then spassN else eN
1.8 + val atp = case format of DFG _ => spassN | _ => eN
1.9 val {exec, arguments, proof_delims, known_failures, ...} =
1.10 get_atp thy atp ()
1.11 val ord = effective_term_order ctxt atp
1.12 @@ -174,7 +174,7 @@
1.13 let
1.14 val type_enc = type_enc |> type_enc_from_string Strict
1.15 |> adjust_type_enc format
1.16 - val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic
1.17 + val mono = not (is_type_enc_polymorphic type_enc)
1.18 val path = file_name |> Path.explode
1.19 val _ = File.write path ""
1.20 val facts = facts_of thy
1.21 @@ -213,7 +213,7 @@
1.22 val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
1.23 val atp_problem =
1.24 atp_problem
1.25 - |> (format <> DFG ? add_inferences_to_problem infers)
1.26 + |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
1.27 |> order_problem_facts name_ord
1.28 val ord = effective_term_order ctxt eN (* dummy *)
1.29 val ss = lines_for_atp_problem format ord (K []) atp_problem
2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
2.3 @@ -28,7 +28,7 @@
2.4 gen_prec : bool,
2.5 gen_simp : bool}
2.6
2.7 - datatype polymorphism = Monomorphic | Polymorphic
2.8 + datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
2.9 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
2.10 datatype thf_choice = THF_Without_Choice | THF_With_Choice
2.11 datatype thf_defs = THF_Without_Defs | THF_With_Defs
2.12 @@ -39,7 +39,7 @@
2.13 FOF |
2.14 TFF of polymorphism * tptp_explicitness |
2.15 THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.16 - DFG
2.17 + DFG of polymorphism
2.18
2.19 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.20 datatype 'a problem_line =
2.21 @@ -160,7 +160,7 @@
2.22 gen_prec : bool,
2.23 gen_simp : bool}
2.24
2.25 -datatype polymorphism = Monomorphic | Polymorphic
2.26 +datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
2.27 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
2.28 datatype thf_choice = THF_Without_Choice | THF_With_Choice
2.29 datatype thf_defs = THF_Without_Defs | THF_With_Defs
2.30 @@ -171,7 +171,7 @@
2.31 FOF |
2.32 TFF of polymorphism * tptp_explicitness |
2.33 THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.34 - DFG
2.35 + DFG of polymorphism
2.36
2.37 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.38 datatype 'a problem_line =
2.39 @@ -306,7 +306,7 @@
2.40 | is_format_higher_order _ = false
2.41 fun is_format_typed (TFF _) = true
2.42 | is_format_typed (THF _) = true
2.43 - | is_format_typed DFG = true
2.44 + | is_format_typed (DFG _) = true
2.45 | is_format_typed _ = false
2.46
2.47 fun tptp_string_for_role Axiom = "axiom"
2.48 @@ -336,7 +336,7 @@
2.49
2.50 fun str_for_type format ty =
2.51 let
2.52 - val dfg = (format = DFG)
2.53 + val dfg = case format of DFG _ => true | _ => false
2.54 fun str _ (AType (s, [])) =
2.55 if dfg andalso s = tptp_individual_type then dfg_individual_type else s
2.56 | str _ (AType (s, tys)) =
2.57 @@ -438,7 +438,7 @@
2.58 | tptp_string_for_format FOF = tptp_fof
2.59 | tptp_string_for_format (TFF _) = tptp_tff
2.60 | tptp_string_for_format (THF _) = tptp_thf
2.61 - | tptp_string_for_format DFG = raise Fail "non-TPTP format"
2.62 + | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
2.63
2.64 fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
2.65 tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
2.66 @@ -464,7 +464,7 @@
2.67 fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
2.68 | binder_atypes _ = []
2.69
2.70 -fun dfg_string_for_formula gen_simp info =
2.71 +fun dfg_string_for_formula poly gen_simp info =
2.72 let
2.73 fun suffix_tag top_level s =
2.74 if top_level then
2.75 @@ -492,7 +492,7 @@
2.76 | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
2.77 fun str_for_formula top_level (AQuant (q, xs, phi)) =
2.78 str_for_quant q ^ "(" ^ "[" ^
2.79 - commas (map (string_for_bound_var DFG) xs) ^ "], " ^
2.80 + commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
2.81 str_for_formula top_level phi ^ ")"
2.82 | str_for_formula top_level (AConn (c, phis)) =
2.83 str_for_conn top_level c ^ "(" ^
2.84 @@ -503,19 +503,19 @@
2.85 fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
2.86 | maybe_enclose bef aft s = bef ^ s ^ aft
2.87
2.88 -fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
2.89 +fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
2.90 let
2.91 fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
2.92 fun ary sym = curry spair sym o arity_of_type
2.93 fun fun_typ sym ty =
2.94 - "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")."
2.95 + "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")."
2.96 fun pred_typ sym ty =
2.97 "predicate(" ^
2.98 - commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")."
2.99 + commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")."
2.100 fun formula pred (Formula (ident, kind, phi, _, info)) =
2.101 if pred kind then
2.102 let val rank = extract_isabelle_rank info in
2.103 - "formula(" ^ dfg_string_for_formula gen_simp info phi ^
2.104 + "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
2.105 ", " ^ ident ^
2.106 (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
2.107 ")." |> SOME
2.108 @@ -587,7 +587,9 @@
2.109 fun lines_for_atp_problem format ord ord_info problem =
2.110 "% This file was generated by Isabelle (most likely Sledgehammer)\n\
2.111 \% " ^ timestamp () ^ "\n" ::
2.112 - (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem
2.113 + (case format of
2.114 + DFG poly => dfg_lines poly ord ord_info
2.115 + | _ => tptp_lines format) problem
2.116
2.117
2.118 (** CNF (Metis) and CNF UEQ (Waldmeister) **)
2.119 @@ -787,7 +789,7 @@
2.120 val avoid_clash =
2.121 case format of
2.122 TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
2.123 - | DFG => avoid_clash_with_dfg_keywords
2.124 + | DFG _ => avoid_clash_with_dfg_keywords
2.125 | _ => I
2.126 val nice_name = nice_name avoid_clash
2.127 fun nice_type (AType (name, tys)) =
3.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
3.3 @@ -22,7 +22,6 @@
3.4 General | Induction | Intro | Inductive | Elim | Simp | Def
3.5 type stature = scope * status
3.6
3.7 - datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.8 datatype strictness = Strict | Non_Strict
3.9 datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
3.10 datatype type_level =
3.11 @@ -86,7 +85,7 @@
3.12 val atp_irrelevant_consts : string list
3.13 val atp_schematic_consts_of : term -> typ list Symtab.table
3.14 val is_type_enc_higher_order : type_enc -> bool
3.15 - val polymorphism_of_type_enc : type_enc -> polymorphism
3.16 + val is_type_enc_polymorphic : type_enc -> bool
3.17 val level_of_type_enc : type_enc -> type_level
3.18 val is_type_enc_sound : type_enc -> bool
3.19 val type_enc_from_string : strictness -> string -> type_enc
3.20 @@ -126,7 +125,12 @@
3.21 datatype order =
3.22 First_Order |
3.23 Higher_Order of thf_choice
3.24 -datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.25 +datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
3.26 +datatype polymorphism =
3.27 + Type_Class_Polymorphic |
3.28 + Raw_Polymorphic of phantom_policy |
3.29 + Raw_Monomorphic |
3.30 + Mangled_Monomorphic
3.31 datatype strictness = Strict | Non_Strict
3.32 datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
3.33 datatype type_level =
3.34 @@ -149,6 +153,12 @@
3.35 | polymorphism_of_type_enc (Guards (poly, _)) = poly
3.36 | polymorphism_of_type_enc (Tags (poly, _)) = poly
3.37
3.38 +fun is_type_enc_polymorphic type_enc =
3.39 + case polymorphism_of_type_enc type_enc of
3.40 + Raw_Polymorphic _ => true
3.41 + | Type_Class_Polymorphic => true
3.42 + | _ => false
3.43 +
3.44 fun level_of_type_enc (Native (_, _, level)) = level
3.45 | level_of_type_enc (Guards (_, level)) = level
3.46 | level_of_type_enc (Tags (_, level)) = level
3.47 @@ -173,10 +183,6 @@
3.48 val keep_lamsN = "keep_lams"
3.49 val lam_liftingN = "lam_lifting" (* legacy *)
3.50
3.51 -(* It's still unclear whether all TFF1 implementations will support type
3.52 - signatures such as "!>[A : $tType] : $o", with phantom type variables. *)
3.53 -val avoid_first_order_phantom_type_vars = false
3.54 -
3.55 val bound_var_prefix = "B_"
3.56 val all_bound_var_prefix = "A_"
3.57 val exist_bound_var_prefix = "E_"
3.58 @@ -606,15 +612,21 @@
3.59 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
3.60
3.61 fun type_enc_from_string strictness s =
3.62 - (case try (unprefix "poly_") s of
3.63 - SOME s => (SOME Raw_Polymorphic, s)
3.64 + (case try (unprefix "tc_") s of
3.65 + SOME s => (SOME Type_Class_Polymorphic, s)
3.66 | NONE =>
3.67 - case try (unprefix "raw_mono_") s of
3.68 - SOME s => (SOME Raw_Monomorphic, s)
3.69 - | NONE =>
3.70 - case try (unprefix "mono_") s of
3.71 - SOME s => (SOME Mangled_Monomorphic, s)
3.72 - | NONE => (NONE, s))
3.73 + case try (unprefix "poly_") s of
3.74 + (* It's still unclear whether all TFF1 implementations will support
3.75 + type signatures such as "!>[A : $tType] : $o", with phantom type
3.76 + variables. *)
3.77 + SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
3.78 + | NONE =>
3.79 + case try (unprefix "raw_mono_") s of
3.80 + SOME s => (SOME Raw_Monomorphic, s)
3.81 + | NONE =>
3.82 + case try (unprefix "mono_") s of
3.83 + SOME s => (SOME Mangled_Monomorphic, s)
3.84 + | NONE => (NONE, s))
3.85 ||> (fn s =>
3.86 case try_unsuffixes queries s of
3.87 SOME s =>
3.88 @@ -629,26 +641,25 @@
3.89 case (core, (poly, level)) of
3.90 ("native", (SOME poly, _)) =>
3.91 (case (poly, level) of
3.92 - (Raw_Polymorphic, All_Types) =>
3.93 - Native (First_Order, Raw_Polymorphic, All_Types)
3.94 - | (Mangled_Monomorphic, _) =>
3.95 + (Mangled_Monomorphic, _) =>
3.96 if granularity_of_type_level level = All_Vars then
3.97 Native (First_Order, Mangled_Monomorphic, level)
3.98 else
3.99 raise Same.SAME
3.100 - | _ => raise Same.SAME)
3.101 + | (Raw_Monomorphic, _) => raise Same.SAME
3.102 + | (poly, All_Types) => Native (First_Order, poly, All_Types))
3.103 | ("native_higher", (SOME poly, _)) =>
3.104 (case (poly, level) of
3.105 - (Raw_Polymorphic, All_Types) =>
3.106 - Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types)
3.107 - | (_, Nonmono_Types _) => raise Same.SAME
3.108 + (_, Nonmono_Types _) => raise Same.SAME
3.109 | (Mangled_Monomorphic, _) =>
3.110 if granularity_of_type_level level = All_Vars then
3.111 Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,
3.112 level)
3.113 else
3.114 raise Same.SAME
3.115 - | _ => raise Same.SAME)
3.116 + | (Raw_Monomorphic, _) => raise Same.SAME
3.117 + | (poly, All_Types) =>
3.118 + Native (Higher_Order THF_With_Choice, poly, All_Types))
3.119 | ("guards", (SOME poly, _)) =>
3.120 if poly = Mangled_Monomorphic andalso
3.121 granularity_of_type_level level = Undercover_Vars then
3.122 @@ -666,7 +677,7 @@
3.123 if poly = Mangled_Monomorphic then raise Same.SAME
3.124 else Guards (poly, Const_Types true)
3.125 | ("erased", (NONE, All_Types (* naja *))) =>
3.126 - Guards (Raw_Polymorphic, No_Types)
3.127 + Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
3.128 | _ => raise Same.SAME)
3.129 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
3.130
3.131 @@ -682,7 +693,9 @@
3.132 Native (adjust_order choice order, Mangled_Monomorphic, level)
3.133 | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
3.134 Native (First_Order, Mangled_Monomorphic, level)
3.135 - | adjust_type_enc DFG (Native (_, _, level)) =
3.136 + | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
3.137 + Native (First_Order, poly, level)
3.138 + | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
3.139 Native (First_Order, Mangled_Monomorphic, level)
3.140 | adjust_type_enc (TFF _) (Native (_, poly, level)) =
3.141 Native (First_Order, poly, level)
3.142 @@ -774,7 +787,7 @@
3.143 fun lift_lams_part_1 ctxt type_enc =
3.144 map close_form #> rpair ctxt
3.145 #-> Lambda_Lifting.lift_lambdas
3.146 - (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
3.147 + (SOME ((if is_type_enc_polymorphic type_enc then
3.148 lam_lifted_poly_prefix
3.149 else
3.150 lam_lifted_mono_prefix) ^ "_a"))
3.151 @@ -839,7 +852,8 @@
3.152 if s = type_tag_name then
3.153 if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
3.154 else case type_enc of
3.155 - Native (_, Raw_Polymorphic, _) => All_Type_Args
3.156 + Native (_, Raw_Polymorphic _, _) => All_Type_Args
3.157 + | Native (_, Type_Class_Polymorphic, _) => All_Type_Args
3.158 | Tags (_, All_Types) => No_Type_Args
3.159 | _ =>
3.160 let val level = level_of_type_enc type_enc in
3.161 @@ -877,9 +891,8 @@
3.162 fun type_class_formula type_enc class arg =
3.163 AAtom (ATerm (class, arg ::
3.164 (case type_enc of
3.165 - Native (First_Order, Raw_Polymorphic, _) =>
3.166 - if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])]
3.167 - else []
3.168 + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
3.169 + [ATerm (TYPE_name, [arg])]
3.170 | _ => [])))
3.171 fun formulas_for_types type_enc add_sorts_on_typ Ts =
3.172 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
3.173 @@ -981,7 +994,7 @@
3.174 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
3.175 | to_poly_atype _ = raise Fail "unexpected type abstraction"
3.176 val to_atype =
3.177 - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype
3.178 + if is_type_enc_polymorphic type_enc then to_poly_atype
3.179 else to_mangled_atype
3.180 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
3.181 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
3.182 @@ -1703,7 +1716,9 @@
3.183 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
3.184 |> map (apsnd (map (apsnd zero_var_indexes)))
3.185
3.186 -fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types
3.187 +fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
3.188 + | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
3.189 + SOME atype_of_types (* ### FIXME *)
3.190 | atype_of_type_vars _ = NONE
3.191
3.192 fun bound_tvars type_enc sorts Ts =
3.193 @@ -1730,7 +1745,7 @@
3.194 val type_tag = `(make_fixed_const NONE) type_tag_name
3.195
3.196 fun could_specialize_helpers type_enc =
3.197 - polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso
3.198 + not (is_type_enc_polymorphic type_enc) andalso
3.199 level_of_type_enc type_enc <> No_Types
3.200 fun should_specialize_helper type_enc t =
3.201 could_specialize_helpers type_enc andalso
3.202 @@ -2118,7 +2133,7 @@
3.203 |> close_formula_universally
3.204 |> bound_tvars type_enc true atomic_types, NONE, [])
3.205
3.206 -fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true
3.207 +fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
3.208 | type_enc_needs_free_types (Native _) = false
3.209 | type_enc_needs_free_types _ = true
3.210
3.211 @@ -2136,12 +2151,12 @@
3.212
3.213 (** Symbol declarations **)
3.214
3.215 -fun decl_line_for_class order s =
3.216 +fun decl_line_for_class order phantoms s =
3.217 let val name as (s, _) = `make_type_class s in
3.218 Decl (sym_decl_prefix ^ s, name,
3.219 if order = First_Order then
3.220 ATyAbs ([tvar_a_name],
3.221 - if avoid_first_order_phantom_type_vars then
3.222 + if phantoms = Without_Phantom_Type_Vars then
3.223 AFun (a_itself_atype, bool_atype)
3.224 else
3.225 bool_atype)
3.226 @@ -2151,8 +2166,8 @@
3.227
3.228 fun decl_lines_for_classes type_enc classes =
3.229 case type_enc of
3.230 - Native (order, Raw_Polymorphic, _) =>
3.231 - map (decl_line_for_class order) classes
3.232 + Native (order, Raw_Polymorphic phantoms, _) =>
3.233 + map (decl_line_for_class order phantoms) classes
3.234 | _ => []
3.235
3.236 fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
3.237 @@ -2192,7 +2207,7 @@
3.238 fold add_formula_var_types phis
3.239 | add_formula_var_types _ = I
3.240 fun var_types () =
3.241 - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a]
3.242 + if is_type_enc_polymorphic type_enc then [tvar_a]
3.243 else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
3.244 fun add_undefined_const T =
3.245 let
3.246 @@ -2217,9 +2232,8 @@
3.247 ? (fold (fold add_fact_syms) [conjs, facts]
3.248 #> fold add_iterm_syms extra_tms
3.249 #> (case type_enc of
3.250 - Native (First_Order, Raw_Polymorphic, _) =>
3.251 - if avoid_first_order_phantom_type_vars then add_TYPE_const ()
3.252 - else I
3.253 + Native (First_Order, Raw_Polymorphic phantoms, _) =>
3.254 + phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
3.255 | Native _ => I
3.256 | _ => fold add_undefined_const (var_types ())))
3.257 end
3.258 @@ -2284,7 +2298,7 @@
3.259 add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
3.260 fun monotonic_types_for_facts ctxt mono type_enc facts =
3.261 let val level = level_of_type_enc type_enc in
3.262 - [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso
3.263 + [] |> (is_type_enc_polymorphic type_enc andalso
3.264 is_type_level_monotonicity_based level andalso
3.265 granularity_of_type_level level <> Undercover_Vars)
3.266 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
3.267 @@ -2631,7 +2645,7 @@
3.268 Full_App_Op_And_Predicator
3.269 else if length facts + length hyp_ts
3.270 > app_op_and_predicator_threshold then
3.271 - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op
3.272 + if is_type_enc_polymorphic type_enc then Min_App_Op
3.273 else Sufficient_App_Op
3.274 else
3.275 Sufficient_App_Op_And_Predicator
3.276 @@ -2680,6 +2694,8 @@
3.277 map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
3.278 (not exporter) mono type_enc (rank_of_fact_num num_facts))
3.279 (0 upto num_facts - 1 ~~ facts)
3.280 + val class_rel_lines =
3.281 + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses
3.282 val helper_lines =
3.283 0 upto length helpers - 1 ~~ helpers
3.284 |> map (formula_line_for_fact ctxt helper_prefix I false true mono
3.285 @@ -2689,8 +2705,7 @@
3.286 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
3.287 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
3.288 (factsN, fact_lines),
3.289 - (class_relsN,
3.290 - map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
3.291 + (class_relsN, class_rel_lines),
3.292 (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
3.293 (helpersN, helper_lines),
3.294 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
4.3 @@ -54,6 +54,7 @@
4.4 val satallaxN : string
4.5 val snarkN : string
4.6 val spassN : string
4.7 + val spass_polyN : string
4.8 val vampireN : string
4.9 val waldmeisterN : string
4.10 val z3_tptpN : string
4.11 @@ -149,6 +150,7 @@
4.12 val satallaxN = "satallax"
4.13 val snarkN = "snark"
4.14 val spassN = "spass"
4.15 +val spass_polyN = "spass_poly"
4.16 val vampireN = "vampire"
4.17 val waldmeisterN = "waldmeister"
4.18 val z3_tptpN = "z3_tptp"
4.19 @@ -409,14 +411,14 @@
4.20 prem_role = Conjecture,
4.21 best_slices = fn _ =>
4.22 (* FUDGE *)
4.23 - [(0.1667, (false, ((150, DFG, "mono_native", combsN, true), ""))),
4.24 - (0.1667, (false, ((500, DFG, "mono_native", liftingN, true), spass_H2SOS))),
4.25 - (0.1666, (false, ((50, DFG, "mono_native", liftingN, true), spass_H2LR0LT0))),
4.26 - (0.1000, (false, ((250, DFG, "mono_native", combsN, true), spass_H2NuVS0))),
4.27 - (0.1000, (false, ((1000, DFG, "mono_native", liftingN, true), spass_H1SOS))),
4.28 - (0.1000, (false, ((150, DFG, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
4.29 - (0.1000, (false, ((300, DFG, "mono_native", combsN, true), spass_H2SOS))),
4.30 - (0.1000, (false, ((100, DFG, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
4.31 + [(0.1667, (false, ((150, DFG Monomorphic, "mono_native", combsN, true), ""))),
4.32 + (0.1667, (false, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS))),
4.33 + (0.1666, (false, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0))),
4.34 + (0.1000, (false, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0))),
4.35 + (0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))),
4.36 + (0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
4.37 + (0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))),
4.38 + (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
4.39 best_max_mono_iters = default_max_mono_iters,
4.40 best_max_new_mono_instances = default_max_new_mono_instances}
4.41
4.42 @@ -495,7 +497,7 @@
4.43 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
4.44
4.45
4.46 -(* Not really a prover: Experimental Polymorphic TFF and THF output *)
4.47 +(* Not really a prover: Experimental Polymorphic THF and DFG output *)
4.48
4.49 fun dummy_config format type_enc : atp_config =
4.50 {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
4.51 @@ -516,6 +518,9 @@
4.52 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
4.53 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
4.54
4.55 +val spass_poly_format = DFG Polymorphic
4.56 +val spass_poly_config = dummy_config spass_poly_format "tc_native"
4.57 +val spass_poly = (spass_polyN, fn () => spass_poly_config)
4.58
4.59 (* Remote ATP invocation via SystemOnTPTP *)
4.60
4.61 @@ -667,8 +672,8 @@
4.62 end
4.63
4.64 val atps=
4.65 - [alt_ergo, e, leo2, dummy_thf, satallax, spass, vampire, z3_tptp, remote_e,
4.66 - remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
4.67 + [alt_ergo, e, leo2, satallax, spass, spass_poly, vampire, z3_tptp, dummy_thf,
4.68 + remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
4.69 remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
4.70 remote_waldmeister]
4.71
5.1 --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
5.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
5.3 @@ -211,7 +211,7 @@
5.4 fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
5.5 let
5.6 val (conj_clauses, fact_clauses) =
5.7 - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
5.8 + if is_type_enc_polymorphic type_enc then
5.9 (conj_clauses, fact_clauses)
5.10 else
5.11 conj_clauses @ fact_clauses
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
6.3 @@ -717,7 +717,7 @@
6.4 |> not sound
6.5 ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
6.6 |> take num_facts
6.7 - |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic
6.8 + |> not (is_type_enc_polymorphic type_enc)
6.9 ? monomorphize_facts
6.10 |> map (apsnd prop_of)
6.11 |> prepare_atp_problem ctxt format prem_role type_enc