--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
@@ -174,7 +174,7 @@
let
val type_enc = type_enc |> type_enc_from_string Strict
|> adjust_type_enc format
- val mono = polymorphism_of_type_enc type_enc <> Polymorphic
+ val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
--- 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 tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+ datatype polymorphism = Monomorphic | Polymorphic
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
@@ -37,8 +37,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism * tptp_explicitness |
+ THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
DFG
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -160,7 +160,7 @@
gen_prec : bool,
gen_simp : bool}
-datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+datatype polymorphism = Monomorphic | Polymorphic
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
@@ -169,8 +169,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism * tptp_explicitness |
+ THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
DFG
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -786,7 +786,7 @@
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
val avoid_clash =
case format of
- TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
+ TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
| DFG => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -22,7 +22,7 @@
General | Induction | Intro | Inductive | Elim | Simp | Def
type stature = scope * status
- datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
+ datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
@@ -126,7 +126,7 @@
datatype order =
First_Order |
Higher_Order of thf_choice
-datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
+datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
@@ -607,7 +607,7 @@
fun type_enc_from_string strictness s =
(case try (unprefix "poly_") s of
- SOME s => (SOME Polymorphic, s)
+ SOME s => (SOME Raw_Polymorphic, s)
| NONE =>
case try (unprefix "raw_mono_") s of
SOME s => (SOME Raw_Monomorphic, s)
@@ -629,8 +629,8 @@
case (core, (poly, level)) of
("native", (SOME poly, _)) =>
(case (poly, level) of
- (Polymorphic, All_Types) =>
- Native (First_Order, Polymorphic, All_Types)
+ (Raw_Polymorphic, All_Types) =>
+ Native (First_Order, Raw_Polymorphic, All_Types)
| (Mangled_Monomorphic, _) =>
if granularity_of_type_level level = All_Vars then
Native (First_Order, Mangled_Monomorphic, level)
@@ -639,8 +639,8 @@
| _ => raise Same.SAME)
| ("native_higher", (SOME poly, _)) =>
(case (poly, level) of
- (Polymorphic, All_Types) =>
- Native (Higher_Order THF_With_Choice, Polymorphic, All_Types)
+ (Raw_Polymorphic, All_Types) =>
+ Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types)
| (_, Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if granularity_of_type_level level = All_Vars then
@@ -666,7 +666,7 @@
if poly = Mangled_Monomorphic then raise Same.SAME
else Guards (poly, Const_Types true)
| ("erased", (NONE, All_Types (* naja *))) =>
- Guards (Polymorphic, No_Types)
+ Guards (Raw_Polymorphic, No_Types)
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
@@ -674,13 +674,13 @@
Higher_Order THF_Without_Choice
| adjust_order _ type_enc = type_enc
-fun adjust_type_enc (THF (TPTP_Polymorphic, _, choice, _))
+fun adjust_type_enc (THF (Polymorphic, _, choice, _))
(Native (order, poly, level)) =
Native (adjust_order choice order, poly, level)
- | adjust_type_enc (THF (TPTP_Monomorphic, _, choice, _))
+ | adjust_type_enc (THF (Monomorphic, _, choice, _))
(Native (order, _, level)) =
Native (adjust_order choice order, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
+ | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc DFG (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
@@ -774,7 +774,7 @@
fun lift_lams_part_1 ctxt type_enc =
map close_form #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
- (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
+ (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
lam_lifted_poly_prefix
else
lam_lifted_mono_prefix) ^ "_a"))
@@ -839,7 +839,7 @@
if s = type_tag_name then
if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
else case type_enc of
- Native (_, Polymorphic, _) => All_Type_Args
+ Native (_, Raw_Polymorphic, _) => All_Type_Args
| Tags (_, All_Types) => No_Type_Args
| _ =>
let val level = level_of_type_enc type_enc in
@@ -877,7 +877,7 @@
fun type_class_formula type_enc class arg =
AAtom (ATerm (class, arg ::
(case type_enc of
- Native (First_Order, Polymorphic, _) =>
+ Native (First_Order, Raw_Polymorphic, _) =>
if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])]
else []
| _ => [])))
@@ -981,7 +981,7 @@
fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
| to_poly_atype _ = raise Fail "unexpected type abstraction"
val to_atype =
- if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
+ if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype
else to_mangled_atype
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
@@ -1703,7 +1703,7 @@
@{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
|> map (apsnd (map (apsnd zero_var_indexes)))
-fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types
+fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types
| atype_of_type_vars _ = NONE
fun bound_tvars type_enc sorts Ts =
@@ -1730,7 +1730,7 @@
val type_tag = `(make_fixed_const NONE) type_tag_name
fun could_specialize_helpers type_enc =
- polymorphism_of_type_enc type_enc <> Polymorphic andalso
+ polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso
level_of_type_enc type_enc <> No_Types
fun should_specialize_helper type_enc t =
could_specialize_helpers type_enc andalso
@@ -2118,7 +2118,7 @@
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
-fun type_enc_needs_free_types (Native (_, Polymorphic, _)) = true
+fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true
| type_enc_needs_free_types (Native _) = false
| type_enc_needs_free_types _ = true
@@ -2151,7 +2151,8 @@
fun decl_lines_for_classes type_enc classes =
case type_enc of
- Native (order, Polymorphic, _) => map (decl_line_for_class order) classes
+ Native (order, Raw_Polymorphic, _) =>
+ map (decl_line_for_class order) classes
| _ => []
fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2191,7 +2192,7 @@
fold add_formula_var_types phis
| add_formula_var_types _ = I
fun var_types () =
- if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
+ if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a]
else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
fun add_undefined_const T =
let
@@ -2216,7 +2217,7 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (First_Order, Polymorphic, _) =>
+ Native (First_Order, Raw_Polymorphic, _) =>
if avoid_first_order_phantom_type_vars then add_TYPE_const ()
else I
| Native _ => I
@@ -2283,7 +2284,7 @@
add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
fun monotonic_types_for_facts ctxt mono type_enc facts =
let val level = level_of_type_enc type_enc in
- [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
+ [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso
is_type_level_monotonicity_based level andalso
granularity_of_type_level level <> Undercover_Vars)
? fold (add_fact_monotonic_types ctxt mono type_enc) facts
@@ -2630,7 +2631,7 @@
Full_App_Op_And_Predicator
else if length facts + length hyp_ts
> app_op_and_predicator_threshold then
- if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op
+ if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op
else Sufficient_App_Op
else
Sufficient_App_Op_And_Predicator
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200
@@ -55,8 +55,7 @@
val satallax_unsat_coreN : string
val parse_formula :
string list -> (string, 'a, (string, 'a) ho_term) formula * string list
- val atp_proof_from_tstplike_proof :
- string problem -> string -> string -> string proof
+ val atp_proof_from_tstplike_proof : string problem -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
(string -> string) -> string proof -> string proof
@@ -485,8 +484,8 @@
(Scan.repeat1 (parse_line problem))))
|> fst
-fun atp_proof_from_tstplike_proof _ _ "" = []
- | atp_proof_from_tstplike_proof problem output tstp =
+fun atp_proof_from_tstplike_proof _ "" = []
+ | atp_proof_from_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
|> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
@@ -185,7 +185,7 @@
(* Alt-Ergo *)
-val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
+val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], "why3"),
@@ -330,7 +330,7 @@
(* LEO-II supports definitions, but it performs significantly better on our
benchmarks when they are not used. *)
val leo2_thf0 =
- THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
+ THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
{exec = (["LEO2_HOME"], "leo"),
@@ -359,7 +359,7 @@
(* Satallax *)
val satallax_thf0 =
- THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
+ THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val satallax_config : atp_config =
{exec = (["SATALLAX_HOME"], "satallax"),
@@ -429,7 +429,7 @@
fun is_new_vampire_version () =
string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
-val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
+val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
val vampire_config : atp_config =
{exec = (["VAMPIRE_HOME"], "vampire"),
@@ -473,7 +473,7 @@
(* Z3 with TPTP syntax *)
-val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
+val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
val z3_tptp_config : atp_config =
{exec = (["Z3_HOME"], "z3"),
@@ -512,7 +512,7 @@
best_max_new_mono_instances = default_max_new_mono_instances}
val dummy_thf_format =
- THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
+ THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
@@ -587,7 +587,7 @@
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice o config)
-val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
+val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
--- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -211,7 +211,7 @@
fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
val (conj_clauses, fact_clauses) =
- if polymorphism_of_type_enc type_enc = Polymorphic then
+ if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
(conj_clauses, fact_clauses)
else
conj_clauses @ fact_clauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
@@ -717,7 +717,7 @@
|> not sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
- |> polymorphism_of_type_enc type_enc <> Polymorphic
+ |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic
? monomorphize_facts
|> map (apsnd prop_of)
|> prepare_atp_problem ctxt format prem_role type_enc
@@ -750,7 +750,7 @@
(accum,
extract_tstplike_proof_and_outcome verbose complete
proof_delims known_failures output
- |>> atp_proof_from_tstplike_proof atp_problem output
+ |>> atp_proof_from_tstplike_proof atp_problem
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>