diff -r 4f1c1c7eb95f -r 11e34ffc65e4 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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>\HOL.eq\ = 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