# HG changeset patch # User blanchet # Date 1340702335 -7200 # Node ID 14e31703380905e5bc520fe3b394485c1674b1b9 # Parent f7b31782e632553996a5353a998031f1a6477c32 reintroduced "t@" encoding, this time sound diff -r f7b31782e632 -r 14e317033809 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jun 26 11:18:55 2012 +0200 @@ -27,19 +27,21 @@ "poly_guards", "poly_guards?", "poly_guards??", - "poly_guards@?", + "poly_guards@", "poly_tags", "poly_tags?", "poly_tags??", + "poly_tags@", "poly_args", "poly_args?", "raw_mono_guards", "raw_mono_guards?", "raw_mono_guards??", - "raw_mono_guards@?", + "raw_mono_guards@", "raw_mono_tags", "raw_mono_tags?", "raw_mono_tags??", + "raw_mono_tags@", "raw_mono_args", "raw_mono_args?", "mono_guards", diff -r f7b31782e632 -r 14e317033809 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:18:55 2012 +0200 @@ -27,7 +27,7 @@ datatype type_level = All_Types | Nonmono_Types of strictness * granularity | - Const_Types of bool (* "?" *) | + Const_Types of bool | No_Types type type_enc @@ -609,11 +609,11 @@ SOME s => (case try_unsuffixes queries s of SOME s => (Nonmono_Types (strictness, Positively_Naked_Vars), s) - | NONE => - case try_unsuffixes ats s of - SOME s => (Nonmono_Types (strictness, Undercover_Vars), s) - | NONE => (Nonmono_Types (strictness, All_Vars), s)) - | NONE => (All_Types, s)) + | NONE => (Nonmono_Types (strictness, All_Vars), s)) + | NONE => + (case try_unsuffixes ats s of + SOME s => (Nonmono_Types (strictness, Undercover_Vars), s) + | NONE => (All_Types, s))) |> (fn (poly, (level, core)) => case (core, (poly, level)) of ("native", (SOME poly, _)) => @@ -645,7 +645,8 @@ else Guards (poly, level) | ("tags", (SOME poly, _)) => - if granularity_of_type_level level = Undercover_Vars orelse + if (poly = Mangled_Monomorphic andalso + granularity_of_type_level level = Undercover_Vars) orelse poly = Type_Class_Polymorphic then raise Same.SAME else @@ -830,8 +831,9 @@ datatype type_arg_policy = Mangled_Type_Args | All_Type_Args | - Noninferable_Type_Args | - Constr_Type_Args | + Not_Input_Type_Args | + Only_In_Or_Output_Type_Args | + Constr_Input_Type_Args | No_Type_Args fun type_arg_policy constrs type_enc s = @@ -849,11 +851,14 @@ No_Type_Args else if poly = Mangled_Monomorphic then Mangled_Type_Args - else if level = All_Types orelse - granularity_of_type_level level = Undercover_Vars then - Noninferable_Type_Args + else if level = All_Types then + Not_Input_Type_Args + else if granularity_of_type_level level = Undercover_Vars then + case type_enc of + Tags _ => Only_In_Or_Output_Type_Args + | _ => Not_Input_Type_Args else if member (op =) constrs s andalso level <> Const_Types false then - Constr_Type_Args + Constr_Input_Type_Args else All_Type_Args end @@ -1136,15 +1141,21 @@ chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ T = ([], T) -fun infer_type_args _ _ _ _ [] = [] - | infer_type_args maybe_not thy s binders_of T_args = +fun filter_type_args _ _ _ _ [] = [] + | filter_type_args keep thy s strip_ty T_args = let val U = robust_const_type thy s - val arg_U_vars = fold Term.add_tvarsT (binders_of U) [] - fun filt (U, T) = - if maybe_not (member (op =) arg_U_vars (dest_TVar U)) then dummyT else T + val (binder_Us, body_U) = strip_ty U + val in_U_vars = fold Term.add_tvarsT binder_Us [] + val out_U_vars = Term.add_tvarsT body_U [] + fun filt (U_var, T) = + if keep (member (op =) in_U_vars U_var, + member (op =) out_U_vars U_var) then + T + else + dummyT val U_args = (s, U) |> robust_const_typargs thy - in map filt (U_args ~~ T_args) end + in map (filt o apfst dest_TVar) (U_args ~~ T_args) end handle TYPE _ => T_args fun filter_type_args_in_const _ _ _ _ _ [] = [] @@ -1158,9 +1169,12 @@ case type_arg_policy constrs type_enc s'' of Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" | All_Type_Args => T_args - | Noninferable_Type_Args => - infer_type_args I thy s'' (fst o chop_fun ary) T_args - | Constr_Type_Args => infer_type_args not thy s'' binder_types T_args + | Not_Input_Type_Args => + filter_type_args (not o fst) thy s'' (chop_fun ary) T_args + | Only_In_Or_Output_Type_Args => + filter_type_args (op <>) thy s'' (chop_fun ary) T_args + | Constr_Input_Type_Args => + filter_type_args fst thy s'' strip_type T_args | No_Type_Args => [] end fun filter_type_args_in_iterm thy constrs type_enc = @@ -1398,16 +1412,22 @@ datatype site = Top_Level of bool option | Eq_Arg of bool option | + Arg of string * int * int | Elsewhere fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false | should_tag_with_type ctxt mono (Tags (_, level)) site u T = - if granularity_of_type_level level = All_Vars then - should_encode_type ctxt mono level T - else - (case (site, is_maybe_universal_var u) of - (Eq_Arg _, true) => should_encode_type ctxt mono level T - | _ => false) + let val thy = Proof_Context.theory_of ctxt in + case granularity_of_type_level level of + All_Vars => should_encode_type ctxt mono level T + | grain => + (case (site, is_maybe_universal_var u) of + (Eq_Arg _, true) => should_encode_type ctxt mono level T + | (Arg (s, j, ary), true) => + grain = Undercover_Vars andalso + member (op =) (type_arg_cover thy s ary) j + | _ => false) + end | should_tag_with_type _ _ _ _ _ _ = false fun fused_type ctxt mono level = @@ -2028,8 +2048,13 @@ case head of IConst (name as (s, _), _, T_args) => let - val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere - in map (term arg_site) args |> mk_aterm type_enc name T_args end + val ary = length args + fun arg_site j = + if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary) + in + map2 (fn j => term (arg_site j)) (0 upto ary - 1) args + |> mk_aterm type_enc name T_args + end | IVar (name, _) => map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => @@ -2091,8 +2116,8 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) -fun formula_line_for_fact ctxt prefix encode freshen pos mono type_enc rank - (j, {name, stature, role, iformula, atomic_types}) = +fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank + (j, {name, stature, role, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role, iformula |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula @@ -2111,21 +2136,21 @@ end) |> Formula -fun formula_lines_for_subclass type_enc sub super = +fun lines_for_subclass type_enc sub super = Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], NONE, isabelle_info inductiveN helper_rank) -fun formula_lines_for_subclass_pair type_enc (sub, supers) = +fun lines_for_subclass_pair type_enc (sub, supers) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)] else - map (formula_lines_for_subclass type_enc sub) supers + map (lines_for_subclass type_enc sub) supers -fun formula_line_for_tcon_clause type_enc (name, prems, (cl, T)) = +fun line_for_tcon_clause type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, map (fn (cls, T) => @@ -2139,8 +2164,8 @@ |> bound_tvars type_enc true (snd (dest_Type T)), NONE, isabelle_info inductiveN helper_rank) -fun formula_line_for_conjecture ctxt mono type_enc - ({name, role, iformula, atomic_types, ...} : ifact) = +fun line_for_conjecture ctxt mono type_enc + ({name, role, iformula, atomic_types, ...} : ifact) = Formula (conjecture_prefix ^ name, role, iformula |> formula_from_iformula ctxt mono type_enc @@ -2148,7 +2173,7 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) -fun formula_lines_for_free_types type_enc (facts : ifact list) = +fun lines_for_free_types type_enc (facts : ifact list) = let fun line j (cl, T) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then @@ -2316,7 +2341,7 @@ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end -fun formula_line_for_guards_mono_type ctxt mono type_enc T = +fun line_for_guards_mono_type ctxt mono type_enc T = Formula (guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), Axiom, @@ -2329,7 +2354,7 @@ |> bound_tvars type_enc true (atomic_types_of T), NONE, isabelle_info inductiveN helper_rank) -fun formula_line_for_tags_mono_type ctxt mono type_enc T = +fun line_for_tags_mono_type ctxt mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in Formula (tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), @@ -2342,8 +2367,8 @@ fun lines_for_mono_types ctxt mono type_enc Ts = case type_enc of Native _ => [] - | Guards _ => map (formula_line_for_guards_mono_type ctxt mono type_enc) Ts - | Tags _ => map (formula_line_for_tags_mono_type ctxt mono type_enc) Ts + | Guards _ => map (line_for_guards_mono_type ctxt mono type_enc) Ts + | Tags _ => map (line_for_tags_mono_type ctxt mono type_enc) Ts fun decl_line_for_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) = @@ -2370,8 +2395,8 @@ fun honor_conj_sym_role in_conj = if in_conj then (Hypothesis, I) else (Axiom, I) -fun formula_line_for_guards_sym_decl ctxt mono type_enc n s j - (s', T_args, T, _, ary, in_conj) = +fun line_for_guards_sym_decl ctxt mono type_enc n s j + (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt val (role, maybe_negate) = honor_conj_sym_role in_conj @@ -2402,8 +2427,8 @@ NONE, isabelle_info inductiveN helper_rank) end -fun formula_lines_for_tags_sym_decl ctxt mono type_enc n s - (j, (s', T_args, T, pred_sym, ary, in_conj)) = +fun lines_for_tags_sym_decl ctxt mono type_enc n s + (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc @@ -2466,7 +2491,7 @@ o result_type_of_decl) in (0 upto length decls - 1, decls) - |-> map2 (formula_line_for_guards_sym_decl ctxt mono type_enc n s) + |-> map2 (line_for_guards_sym_decl ctxt mono type_enc n s) end | Tags (_, level) => if granularity_of_type_level level = All_Vars then @@ -2474,7 +2499,7 @@ else let val n = length decls in (0 upto n - 1 ~~ decls) - |> maps (formula_lines_for_tags_sym_decl ctxt mono type_enc n s) + |> maps (lines_for_tags_sym_decl ctxt mono type_enc n s) end fun lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab = @@ -2703,17 +2728,17 @@ |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts val num_facts = length facts val fact_lines = - map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter) + map (line_for_fact ctxt fact_prefix ascii_of (not exporter) (not exporter) mono type_enc (rank_of_fact_num num_facts)) (0 upto num_facts - 1 ~~ facts) - val subclass_lines = - maps (formula_lines_for_subclass_pair type_enc) subclass_pairs - val tcon_lines = map (formula_line_for_tcon_clause type_enc) tcon_clauses - val free_type_lines = formula_lines_for_free_types type_enc (facts @ conjs) + val subclass_lines = maps (lines_for_subclass_pair type_enc) subclass_pairs + val tcon_lines = map (line_for_tcon_clause type_enc) tcon_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt helper_prefix I false true mono - type_enc (K default_rank)) + |> map (line_for_fact ctxt helper_prefix I false true mono type_enc + (K default_rank)) + val free_type_lines = lines_for_free_types type_enc (facts @ conjs) + val conj_lines = map (line_for_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), @@ -2723,7 +2748,7 @@ (tconsN, tcon_lines), (helpersN, helper_lines), (free_typesN, free_type_lines), - (conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)] + (conjsN, conj_lines)] val problem = problem |> (case format of CNF => ensure_cnf_problem