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 @@ -174,7 +174,7 @@
1.4 let
1.5 val type_enc = type_enc |> type_enc_from_string Strict
1.6 |> adjust_type_enc format
1.7 - val mono = polymorphism_of_type_enc type_enc <> Polymorphic
1.8 + val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic
1.9 val path = file_name |> Path.explode
1.10 val _ = File.write path ""
1.11 val facts = facts_of thy
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 tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
2.8 + datatype polymorphism = Monomorphic | Polymorphic
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 @@ -37,8 +37,8 @@
2.13 CNF |
2.14 CNF_UEQ |
2.15 FOF |
2.16 - TFF of tptp_polymorphism * tptp_explicitness |
2.17 - THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.18 + TFF of polymorphism * tptp_explicitness |
2.19 + THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.20 DFG
2.21
2.22 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.23 @@ -160,7 +160,7 @@
2.24 gen_prec : bool,
2.25 gen_simp : bool}
2.26
2.27 -datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
2.28 +datatype polymorphism = Monomorphic | Polymorphic
2.29 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
2.30 datatype thf_choice = THF_Without_Choice | THF_With_Choice
2.31 datatype thf_defs = THF_Without_Defs | THF_With_Defs
2.32 @@ -169,8 +169,8 @@
2.33 CNF |
2.34 CNF_UEQ |
2.35 FOF |
2.36 - TFF of tptp_polymorphism * tptp_explicitness |
2.37 - THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.38 + TFF of polymorphism * tptp_explicitness |
2.39 + THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
2.40 DFG
2.41
2.42 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.43 @@ -786,7 +786,7 @@
2.44 if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
2.45 val avoid_clash =
2.46 case format of
2.47 - TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
2.48 + TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
2.49 | DFG => avoid_clash_with_dfg_keywords
2.50 | _ => I
2.51 val nice_name = nice_name avoid_clash
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,7 @@
3.4 General | Induction | Intro | Inductive | Elim | Simp | Def
3.5 type stature = scope * status
3.6
3.7 - datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.8 + datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.9 datatype strictness = Strict | Non_Strict
3.10 datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
3.11 datatype type_level =
3.12 @@ -126,7 +126,7 @@
3.13 datatype order =
3.14 First_Order |
3.15 Higher_Order of thf_choice
3.16 -datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.17 +datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.18 datatype strictness = Strict | Non_Strict
3.19 datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
3.20 datatype type_level =
3.21 @@ -607,7 +607,7 @@
3.22
3.23 fun type_enc_from_string strictness s =
3.24 (case try (unprefix "poly_") s of
3.25 - SOME s => (SOME Polymorphic, s)
3.26 + SOME s => (SOME Raw_Polymorphic, s)
3.27 | NONE =>
3.28 case try (unprefix "raw_mono_") s of
3.29 SOME s => (SOME Raw_Monomorphic, s)
3.30 @@ -629,8 +629,8 @@
3.31 case (core, (poly, level)) of
3.32 ("native", (SOME poly, _)) =>
3.33 (case (poly, level) of
3.34 - (Polymorphic, All_Types) =>
3.35 - Native (First_Order, Polymorphic, All_Types)
3.36 + (Raw_Polymorphic, All_Types) =>
3.37 + Native (First_Order, Raw_Polymorphic, All_Types)
3.38 | (Mangled_Monomorphic, _) =>
3.39 if granularity_of_type_level level = All_Vars then
3.40 Native (First_Order, Mangled_Monomorphic, level)
3.41 @@ -639,8 +639,8 @@
3.42 | _ => raise Same.SAME)
3.43 | ("native_higher", (SOME poly, _)) =>
3.44 (case (poly, level) of
3.45 - (Polymorphic, All_Types) =>
3.46 - Native (Higher_Order THF_With_Choice, Polymorphic, All_Types)
3.47 + (Raw_Polymorphic, All_Types) =>
3.48 + Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types)
3.49 | (_, Nonmono_Types _) => raise Same.SAME
3.50 | (Mangled_Monomorphic, _) =>
3.51 if granularity_of_type_level level = All_Vars then
3.52 @@ -666,7 +666,7 @@
3.53 if poly = Mangled_Monomorphic then raise Same.SAME
3.54 else Guards (poly, Const_Types true)
3.55 | ("erased", (NONE, All_Types (* naja *))) =>
3.56 - Guards (Polymorphic, No_Types)
3.57 + Guards (Raw_Polymorphic, No_Types)
3.58 | _ => raise Same.SAME)
3.59 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
3.60
3.61 @@ -674,13 +674,13 @@
3.62 Higher_Order THF_Without_Choice
3.63 | adjust_order _ type_enc = type_enc
3.64
3.65 -fun adjust_type_enc (THF (TPTP_Polymorphic, _, choice, _))
3.66 +fun adjust_type_enc (THF (Polymorphic, _, choice, _))
3.67 (Native (order, poly, level)) =
3.68 Native (adjust_order choice order, poly, level)
3.69 - | adjust_type_enc (THF (TPTP_Monomorphic, _, choice, _))
3.70 + | adjust_type_enc (THF (Monomorphic, _, choice, _))
3.71 (Native (order, _, level)) =
3.72 Native (adjust_order choice order, Mangled_Monomorphic, level)
3.73 - | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
3.74 + | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
3.75 Native (First_Order, Mangled_Monomorphic, level)
3.76 | adjust_type_enc DFG (Native (_, _, level)) =
3.77 Native (First_Order, Mangled_Monomorphic, level)
3.78 @@ -774,7 +774,7 @@
3.79 fun lift_lams_part_1 ctxt type_enc =
3.80 map close_form #> rpair ctxt
3.81 #-> Lambda_Lifting.lift_lambdas
3.82 - (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
3.83 + (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
3.84 lam_lifted_poly_prefix
3.85 else
3.86 lam_lifted_mono_prefix) ^ "_a"))
3.87 @@ -839,7 +839,7 @@
3.88 if s = type_tag_name then
3.89 if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
3.90 else case type_enc of
3.91 - Native (_, Polymorphic, _) => All_Type_Args
3.92 + Native (_, Raw_Polymorphic, _) => All_Type_Args
3.93 | Tags (_, All_Types) => No_Type_Args
3.94 | _ =>
3.95 let val level = level_of_type_enc type_enc in
3.96 @@ -877,7 +877,7 @@
3.97 fun type_class_formula type_enc class arg =
3.98 AAtom (ATerm (class, arg ::
3.99 (case type_enc of
3.100 - Native (First_Order, Polymorphic, _) =>
3.101 + Native (First_Order, Raw_Polymorphic, _) =>
3.102 if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])]
3.103 else []
3.104 | _ => [])))
3.105 @@ -981,7 +981,7 @@
3.106 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
3.107 | to_poly_atype _ = raise Fail "unexpected type abstraction"
3.108 val to_atype =
3.109 - if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
3.110 + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype
3.111 else to_mangled_atype
3.112 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
3.113 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
3.114 @@ -1703,7 +1703,7 @@
3.115 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
3.116 |> map (apsnd (map (apsnd zero_var_indexes)))
3.117
3.118 -fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types
3.119 +fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types
3.120 | atype_of_type_vars _ = NONE
3.121
3.122 fun bound_tvars type_enc sorts Ts =
3.123 @@ -1730,7 +1730,7 @@
3.124 val type_tag = `(make_fixed_const NONE) type_tag_name
3.125
3.126 fun could_specialize_helpers type_enc =
3.127 - polymorphism_of_type_enc type_enc <> Polymorphic andalso
3.128 + polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso
3.129 level_of_type_enc type_enc <> No_Types
3.130 fun should_specialize_helper type_enc t =
3.131 could_specialize_helpers type_enc andalso
3.132 @@ -2118,7 +2118,7 @@
3.133 |> close_formula_universally
3.134 |> bound_tvars type_enc true atomic_types, NONE, [])
3.135
3.136 -fun type_enc_needs_free_types (Native (_, Polymorphic, _)) = true
3.137 +fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true
3.138 | type_enc_needs_free_types (Native _) = false
3.139 | type_enc_needs_free_types _ = true
3.140
3.141 @@ -2151,7 +2151,8 @@
3.142
3.143 fun decl_lines_for_classes type_enc classes =
3.144 case type_enc of
3.145 - Native (order, Polymorphic, _) => map (decl_line_for_class order) classes
3.146 + Native (order, Raw_Polymorphic, _) =>
3.147 + map (decl_line_for_class order) classes
3.148 | _ => []
3.149
3.150 fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
3.151 @@ -2191,7 +2192,7 @@
3.152 fold add_formula_var_types phis
3.153 | add_formula_var_types _ = I
3.154 fun var_types () =
3.155 - if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
3.156 + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a]
3.157 else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
3.158 fun add_undefined_const T =
3.159 let
3.160 @@ -2216,7 +2217,7 @@
3.161 ? (fold (fold add_fact_syms) [conjs, facts]
3.162 #> fold add_iterm_syms extra_tms
3.163 #> (case type_enc of
3.164 - Native (First_Order, Polymorphic, _) =>
3.165 + Native (First_Order, Raw_Polymorphic, _) =>
3.166 if avoid_first_order_phantom_type_vars then add_TYPE_const ()
3.167 else I
3.168 | Native _ => I
3.169 @@ -2283,7 +2284,7 @@
3.170 add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
3.171 fun monotonic_types_for_facts ctxt mono type_enc facts =
3.172 let val level = level_of_type_enc type_enc in
3.173 - [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
3.174 + [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso
3.175 is_type_level_monotonicity_based level andalso
3.176 granularity_of_type_level level <> Undercover_Vars)
3.177 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
3.178 @@ -2630,7 +2631,7 @@
3.179 Full_App_Op_And_Predicator
3.180 else if length facts + length hyp_ts
3.181 > app_op_and_predicator_threshold then
3.182 - if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op
3.183 + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op
3.184 else Sufficient_App_Op
3.185 else
3.186 Sufficient_App_Op_And_Predicator
4.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
4.3 @@ -55,8 +55,7 @@
4.4 val satallax_unsat_coreN : string
4.5 val parse_formula :
4.6 string list -> (string, 'a, (string, 'a) ho_term) formula * string list
4.7 - val atp_proof_from_tstplike_proof :
4.8 - string problem -> string -> string -> string proof
4.9 + val atp_proof_from_tstplike_proof : string problem -> string -> string proof
4.10 val clean_up_atp_proof_dependencies : string proof -> string proof
4.11 val map_term_names_in_atp_proof :
4.12 (string -> string) -> string proof -> string proof
4.13 @@ -485,8 +484,8 @@
4.14 (Scan.repeat1 (parse_line problem))))
4.15 |> fst
4.16
4.17 -fun atp_proof_from_tstplike_proof _ _ "" = []
4.18 - | atp_proof_from_tstplike_proof problem output tstp =
4.19 +fun atp_proof_from_tstplike_proof _ "" = []
4.20 + | atp_proof_from_tstplike_proof problem tstp =
4.21 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
4.22 |> parse_proof problem
4.23 |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
5.3 @@ -185,7 +185,7 @@
5.4
5.5 (* Alt-Ergo *)
5.6
5.7 -val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
5.8 +val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
5.9
5.10 val alt_ergo_config : atp_config =
5.11 {exec = (["WHY3_HOME"], "why3"),
5.12 @@ -330,7 +330,7 @@
5.13 (* LEO-II supports definitions, but it performs significantly better on our
5.14 benchmarks when they are not used. *)
5.15 val leo2_thf0 =
5.16 - THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
5.17 + THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
5.18
5.19 val leo2_config : atp_config =
5.20 {exec = (["LEO2_HOME"], "leo"),
5.21 @@ -359,7 +359,7 @@
5.22 (* Satallax *)
5.23
5.24 val satallax_thf0 =
5.25 - THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
5.26 + THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
5.27
5.28 val satallax_config : atp_config =
5.29 {exec = (["SATALLAX_HOME"], "satallax"),
5.30 @@ -429,7 +429,7 @@
5.31 fun is_new_vampire_version () =
5.32 string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
5.33
5.34 -val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
5.35 +val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
5.36
5.37 val vampire_config : atp_config =
5.38 {exec = (["VAMPIRE_HOME"], "vampire"),
5.39 @@ -473,7 +473,7 @@
5.40
5.41 (* Z3 with TPTP syntax *)
5.42
5.43 -val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
5.44 +val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
5.45
5.46 val z3_tptp_config : atp_config =
5.47 {exec = (["Z3_HOME"], "z3"),
5.48 @@ -512,7 +512,7 @@
5.49 best_max_new_mono_instances = default_max_new_mono_instances}
5.50
5.51 val dummy_thf_format =
5.52 - THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
5.53 + THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
5.54 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
5.55 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
5.56
5.57 @@ -587,7 +587,7 @@
5.58 (remote_prefix ^ name,
5.59 remotify_config system_name system_versions best_slice o config)
5.60
5.61 -val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
5.62 +val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
5.63
5.64 val remote_e =
5.65 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
6.1 --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
6.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
6.3 @@ -211,7 +211,7 @@
6.4 fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
6.5 let
6.6 val (conj_clauses, fact_clauses) =
6.7 - if polymorphism_of_type_enc type_enc = Polymorphic then
6.8 + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
6.9 (conj_clauses, fact_clauses)
6.10 else
6.11 conj_clauses @ fact_clauses
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
7.3 @@ -717,7 +717,7 @@
7.4 |> not sound
7.5 ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
7.6 |> take num_facts
7.7 - |> polymorphism_of_type_enc type_enc <> Polymorphic
7.8 + |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic
7.9 ? monomorphize_facts
7.10 |> map (apsnd prop_of)
7.11 |> prepare_atp_problem ctxt format prem_role type_enc
7.12 @@ -750,7 +750,7 @@
7.13 (accum,
7.14 extract_tstplike_proof_and_outcome verbose complete
7.15 proof_delims known_failures output
7.16 - |>> atp_proof_from_tstplike_proof atp_problem output
7.17 + |>> atp_proof_from_tstplike_proof atp_problem
7.18 handle UNRECOGNIZED_ATP_PROOF () =>
7.19 ([], SOME ProofIncomplete)))
7.20 handle TimeLimit.TimeOut =>