# HG changeset patch # User blanchet # Date 1324476268 -3600 # Node ID 7eccf8147f5764a2ce69b7fce5e3a0b6483a1669 # Parent 428db0387f320486ca767574c9e63970cadbd278 treat polymorphic constructors specially in @? encodings diff -r 428db0387f32 -r 7eccf8147f57 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 21 15:04:28 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 21 15:04:28 2011 +0100 @@ -1317,26 +1317,33 @@ | is_maybe_universal_var (IVar _) = true | is_maybe_universal_var _ = false -datatype tag_site = +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)) sites u T = +fun should_tag_with_type _ _ _ _ [Top_Level _] _ _ = false + | should_tag_with_type ctxt polym_constrs mono (Tags (_, level)) sites u T = (case granularity_of_type_level level of All_Vars => should_encode_type ctxt mono level T | grain => - case (hd sites, is_maybe_universal_var u) of - (Eq_Arg _, true) => should_encode_type ctxt mono level T - | (Arg (s, j, ary), true) => - let val thy = Proof_Context.theory_of ctxt in - grain = Ghost_Type_Arg_Vars andalso - member (op =) (ghost_type_args thy s ary) j + case (sites, is_maybe_universal_var u) of + (Eq_Arg _ :: _, true) => should_encode_type ctxt mono level T + | (Arg (s, j, ary) :: site0 :: _, true) => + grain = Ghost_Type_Arg_Vars andalso + let + val thy = Proof_Context.theory_of ctxt + fun is_ghost_type_arg s j ary = + member (op =) (ghost_type_args thy s ary) j + fun is_ghost_site (Arg (s, j, ary)) = is_ghost_type_arg s j ary + | is_ghost_site _ = true + in + is_ghost_type_arg s j ary andalso + (not (member (op =) polym_constrs s) orelse is_ghost_site site0) end | _ => false) - | should_tag_with_type _ _ _ _ _ _ = false + | should_tag_with_type _ _ _ _ _ _ _ = false fun fused_type ctxt mono level = let @@ -1803,13 +1810,13 @@ fun mk_aterm format type_enc name T_args args = ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) -fun tag_with_type ctxt format mono type_enc pos T tm = +fun tag_with_type ctxt polym_constrs format mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) |> mangle_type_args_in_iterm format type_enc - |> ho_term_from_iterm ctxt format mono type_enc pos + |> ho_term_from_iterm ctxt polym_constrs format mono type_enc pos |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") -and ho_term_from_iterm ctxt format mono type_enc = +and ho_term_from_iterm ctxt polym_constrs format mono type_enc = let fun term sites u = let @@ -1839,17 +1846,18 @@ | IApp _ => raise Fail "impossible \"IApp\"" val T = ityp_of u in - t |> (if should_tag_with_type ctxt mono type_enc sites u T then - tag_with_type ctxt format mono type_enc pos T - else - I) + if should_tag_with_type ctxt polym_constrs mono type_enc sites u T then + tag_with_type ctxt polym_constrs format mono type_enc pos T t + else + t end in term o single o Top_Level end -and formula_from_iformula ctxt format mono type_enc should_guard_var = +and formula_from_iformula ctxt polym_constrs format mono type_enc + should_guard_var = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc - val do_term = ho_term_from_iterm ctxt format mono type_enc + val do_term = ho_term_from_iterm ctxt polym_constrs format mono type_enc val do_bound_type = case type_enc of Simple_Types _ => fused_type ctxt mono level 0 @@ -1864,7 +1872,7 @@ else if should_generate_tag_bound_decl ctxt mono type_enc universal T then let val var = ATerm (name, []) - val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T + val tagged_var = tag_with_type ctxt [] format mono type_enc pos T var in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end else NONE @@ -1890,13 +1898,12 @@ (* 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 format prefix encode freshen pos mono type_enc - (j, {name, locality, kind, iformula, atomic_types}) = +fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos + mono type_enc (j, {name, locality, kind, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, iformula - |> formula_from_iformula ctxt format mono type_enc - should_guard_var_in_formula - (if pos then SOME true else NONE) + |> formula_from_iformula ctxt polym_constrs format mono type_enc + should_guard_var_in_formula (if pos then SOME true else NONE) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, @@ -1932,11 +1939,11 @@ (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), isabelle_info format introN, NONE) -fun formula_line_for_conjecture ctxt format mono type_enc +fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, iformula - |> formula_from_iformula ctxt format mono type_enc + |> formula_from_iformula ctxt polym_constrs format mono type_enc should_guard_var_in_formula (SOME false) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, NONE) @@ -2133,7 +2140,7 @@ IConst (`make_bound_var "X", T, []) |> type_guard_iterm format type_enc T |> AAtom - |> formula_from_iformula ctxt format mono type_enc + |> formula_from_iformula ctxt [] format mono type_enc (K (K (K (K (K (K true)))))) (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), @@ -2145,8 +2152,8 @@ ascii_of (mangled_type format type_enc T), Axiom, eq_formula type_enc (atomic_types_of T) false - (tag_with_type ctxt format mono type_enc NONE T x_var) - x_var, + (tag_with_type ctxt [] format mono type_enc NONE T x_var) + x_var, isabelle_info format simpN, NONE) end @@ -2211,7 +2218,7 @@ |> fold (curry (IApp o swap)) bounds |> type_guard_iterm format type_enc res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_iformula ctxt format mono type_enc + |> formula_from_iformula ctxt [] format mono type_enc (K (K (K (K (K (K true)))))) (SOME true) |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) @@ -2237,7 +2244,7 @@ val cst = mk_aterm format type_enc (s, s') T_args val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym val should_encode = should_encode_type ctxt mono level - val tag_with = tag_with_type ctxt format mono type_enc NONE + val tag_with = tag_with_type ctxt [] format mono type_enc NONE val add_formula_for_res = if should_encode res_T then let @@ -2324,7 +2331,7 @@ problem_lines_for_mono_types ctxt format mono type_enc mono_Ts val decl_lines = fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind - mono type_enc) + mono type_enc) syms [] in mono_lines @ decl_lines end @@ -2407,14 +2414,14 @@ fun is_poly_constr (_, Us) = exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us -fun all_monomorphic_constrs_of_polymorphic_datatypes thy = +fun all_constrs_of_polymorphic_datatypes thy = Symtab.fold (snd #> #descr #> maps (snd #> #3) #> (fn cs => exists is_poly_constr cs ? append cs)) (Datatype.get_all thy) [] - |> filter_out is_poly_constr - |> map fst + |> List.partition is_poly_constr + |> pairself (map fst) (* Forcing explicit applications is expensive for polymorphic encodings, because it takes only one existential variable ranging over "'a => 'b" to ruin @@ -2446,7 +2453,9 @@ concl_t facts val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc - val monom_constrs = all_monomorphic_constrs_of_polymorphic_datatypes thy + val (polym_constrs, monom_constrs) = + all_constrs_of_polymorphic_datatypes thy + |>> map (make_fixed_const (SOME format)) val firstorderize = firstorderize_fact thy monom_constrs format type_enc sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize) @@ -2464,8 +2473,8 @@ type_enc mono_Ts val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt format helper_prefix I false true mono - type_enc) + |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I + false true mono type_enc) |> (if needs_type_tag_idempotence ctxt type_enc then cons (type_tag_idempotence_fact format type_enc) else @@ -2475,8 +2484,8 @@ val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), (factsN, - map (formula_line_for_fact ctxt format fact_prefix ascii_of - (not exporter) (not exporter) mono type_enc) + map (formula_line_for_fact ctxt polym_constrs format fact_prefix + ascii_of (not exporter) (not exporter) mono type_enc) (0 upto length facts - 1 ~~ facts)), (class_relsN, map (formula_line_for_class_rel_clause format type_enc) @@ -2485,7 +2494,8 @@ map (formula_line_for_arity_clause format type_enc) arity_clauses), (helpersN, helper_lines), (conjsN, - map (formula_line_for_conjecture ctxt format mono type_enc) conjs), + map (formula_line_for_conjecture ctxt polym_constrs format mono + type_enc) conjs), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))] val problem = problem