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