--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Nov 12 18:47:07 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Nov 12 00:10:16 2021 +0100
@@ -153,10 +153,8 @@
Const_Types of ctr_optim |
No_Types
-type syntax = {with_ite: bool}
-
datatype type_enc =
- Native of order * fool * syntax * polymorphism * type_level |
+ Native of order * fool * polymorphism * type_level |
Guards of polymorphism * type_level |
Tags of polymorphism * type_level
@@ -165,17 +163,20 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _, _)) = false
- | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
+ | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_full_higher_order _ = false
-fun is_type_enc_fool (Native (_, With_FOOL, _, _, _)) = true
+fun is_type_enc_fool (Native (_, With_FOOL _, _, _)) = true
| is_type_enc_fool _ = false
-fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_higher_order _ = false
-fun has_type_enc_ite (Native (_, _, {with_ite, ...}, _, _)) = with_ite
+
+fun has_type_enc_ite (Native (_, With_FOOL {with_ite, ...}, _, _)) = with_ite
| has_type_enc_ite _ = false
+fun has_type_enc_let (Native (_, With_FOOL {with_let, ...}, _, _)) = with_let
+ | has_type_enc_let _ = false
-fun polymorphism_of_type_enc (Native (_, _, _, poly, _)) = poly
+fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
@@ -188,7 +189,7 @@
fun is_type_enc_mangling type_enc =
polymorphism_of_type_enc type_enc = Mangled_Monomorphic
-fun level_of_type_enc (Native (_, _, _, _, level)) = level
+fun level_of_type_enc (Native (_, _, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
@@ -391,7 +392,7 @@
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
- | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _, _))) c =
+ | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c =
if c = choice_const then tptp_choice else default c
| make_fixed_const _ c = default c
end
@@ -680,34 +681,50 @@
fun native_of_string s =
let
+ val (with_let, s) =
+ (case try (unsuffix "_let") s of
+ SOME s => (true, s)
+ | NONE => (false, s))
+ val (with_ite, s) =
+ (case try (unsuffix "_ite") s of
+ SOME s => (true, s)
+ | NONE => (false, s))
+ val syntax = {with_ite = with_ite, with_let = with_let}
val (fool, core) =
(case try (unsuffix "_fool") s of
- SOME s => (With_FOOL, s)
+ SOME s => (With_FOOL syntax, s)
| NONE => (Without_FOOL, s))
- val syntax = {with_ite = (fool = With_FOOL)}
+
+ fun validate_syntax (type_enc as Native (_, Without_FOOL, _, _)) =
+ if with_ite orelse with_let then
+ error "\"ite\" and \"let\" options require \"native_fool\" or \"native_higher\"."
+ else
+ type_enc
+ | validate_syntax type_enc = type_enc
in
(case (core, poly) of
("native", SOME poly) =>
(case (poly, level) of
(Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (First_Order, fool, syntax, Mangled_Monomorphic, level)
+ Native (First_Order, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (Raw_Monomorphic, _) => raise Same.SAME
- | (poly, All_Types) => Native (First_Order, fool, syntax, poly, All_Types))
+ | (poly, All_Types) => Native (First_Order, fool, poly, All_Types))
| ("native_higher", SOME poly) =>
(case (poly, level) of
(_, Nonmono_Types _) => raise Same.SAME
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (Higher_Order THF_With_Choice, fool, syntax, Mangled_Monomorphic, level)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
- Native (Higher_Order THF_With_Choice, fool, syntax, poly, All_Types)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, poly, All_Types)
| _ => raise Same.SAME))
+ |> validate_syntax
end
fun nonnative_of_string core =
@@ -752,28 +769,28 @@
fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
| adjust_hologic _ type_enc = type_enc
-fun adjust_fool Without_FOOL _ = Without_FOOL
- | adjust_fool _ fool = fool
+fun adjust_syntax {with_ite = ite1, with_let = let1} {with_ite = ite2, with_let = let2} =
+ {with_ite = ite1 andalso ite2, with_let = let1 andalso let2}
+
+fun adjust_fool (With_FOOL syntax) (With_FOOL syntax') = With_FOOL (adjust_syntax syntax syntax')
+ | adjust_fool _ _ = Without_FOOL
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (fool, Polymorphic, hologic))
- (Native (order, fool', syntax, poly, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, no_type_classes poly,
- level)
- | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', syntax, _, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, Mangled_Monomorphic,
+fun adjust_type_enc (THF (poly, syntax, hologic)) (Native (order, fool, poly', level)) =
+ Native (adjust_hologic hologic order, adjust_fool (With_FOOL syntax) fool,
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
level)
- | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', syntax, _, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (DFG Polymorphic) (Native (_, _, syntax, poly, level)) =
- Native (First_Order, Without_FOOL, syntax, poly, level)
- | adjust_type_enc (DFG Monomorphic) (Native (_, _, syntax, _, level)) =
- Native (First_Order, Without_FOOL, syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (fool, _)) (Native (_, fool', syntax, poly, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, no_type_classes poly, level)
- | adjust_type_enc format (Native (_, _, _, poly, level)) =
+ | adjust_type_enc (TFF (poly, fool)) (Native (_, fool', poly', level)) =
+ Native (First_Order, adjust_fool fool fool',
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
+ level)
+ | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) =
+ Native (First_Order, Without_FOOL, poly, level)
+ | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) =
+ Native (First_Order, Without_FOOL, Mangled_Monomorphic, level)
+ | adjust_type_enc format (Native (_, _, poly, level)) =
adjust_type_enc format (Guards (no_type_classes poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_sound type_enc then Tags else Guards) stuff
@@ -949,8 +966,8 @@
T_args
else
(case type_enc of
- Native (_, _, _, Raw_Polymorphic _, _) => T_args
- | Native (_, _, _, Type_Class_Polymorphic, _) => T_args
+ Native (_, _, Raw_Polymorphic _, _) => T_args
+ | Native (_, _, Type_Class_Polymorphic, _) => T_args
| _ =>
let
fun gen_type_args _ _ [] = []
@@ -1086,7 +1103,7 @@
val tm_args =
tm_args @
(case type_enc of
- Native (_, _, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
@@ -1215,6 +1232,7 @@
let
val is_fool = is_type_enc_fool type_enc
val has_ite = has_type_enc_ite type_enc
+ val has_let = has_type_enc_let type_enc
fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
(* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
limitations. This works in conjunction with special code in "ATP_Problem" that uses the
@@ -1270,7 +1288,7 @@
let val argc = length args in
if has_ite andalso s = "c_If" andalso argc >= 3 then
IConst (`I tptp_ite, T, [])
- else if is_fool andalso s = "c_Let" andalso argc >= 2 then
+ else if has_let andalso s = "c_Let" andalso argc >= 2 then
IConst (`I tptp_let, T, [])
else
(case proxify_const s of
@@ -1881,10 +1899,10 @@
|> class_membs_of_types type_enc add_sorts_on_tvar
|> map (class_atom type_enc)))
#> (case type_enc of
- Native (_, _, _, Type_Class_Polymorphic, _) =>
+ Native (_, _, Type_Class_Polymorphic, _) =>
mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
(AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts)
- | Native (_, _, _, Raw_Polymorphic _, _) =>
+ | Native (_, _, Raw_Polymorphic _, _) =>
mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts)
| _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
@@ -1940,10 +1958,11 @@
in
fold (fn ((helper_s, needs_sound), ths) =>
let
- fun map_syntax_of_type_enc f (Native (order, fool, syntax, polymorphism, type_level)) =
- Native (order, fool, f syntax, polymorphism, type_level)
- | map_syntax_of_type_enc _ type_enc = type_enc
- val remove_ite_syntax = map_syntax_of_type_enc (K {with_ite = false})
+ fun map_syntax f (Native (order, With_FOOL syntax, polymorphism, type_level)) =
+ Native (order, With_FOOL (f syntax), polymorphism, type_level)
+ | map_syntax _ type_enc = type_enc
+ val remove_ite_syntax = map_syntax
+ (fn {with_let, ...} => {with_ite = false, with_let = with_let})
in
if (needs_sound andalso not sound) orelse
(helper_s <> unmangled_s andalso
@@ -2313,7 +2332,7 @@
fun decl_lines_of_classes type_enc =
(case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
+ Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
| _ => K [])
fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2375,7 +2394,7 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) =>
+ Native (_, _, Raw_Polymorphic phantoms, _) =>
phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
@@ -2815,9 +2834,8 @@
if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
else lam_trans
val simp_options =
- let val simp = not (is_type_enc_fool type_enc) in
- {if_simps = simp, let_simps = simp}
- end
+ {if_simps = not (has_type_enc_ite type_enc),
+ let_simps = not (has_type_enc_let type_enc)}
val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts
concl_t facts