# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID c9552e617accbec28ca31d761fcbe811cada4168 # Parent 887789ed4b492180cf21030b9d7ade19da19287f drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation diff -r 887789ed4b49 -r c9552e617acc doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 15:29:19 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 15:29:19 2011 +0200 @@ -566,10 +566,6 @@ following values: \begin{enum} -%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for -%polymorphic first-order logic if available; otherwise, fall back on -%\textit{poly\_preds}. - \item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate $\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables. Constants are annotated with their types, supplied as extra arguments, to @@ -615,8 +611,8 @@ \item[$\bullet$] \textbf{% -\textit{simple\_types}?, -\{\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\ +\textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple\_types}?, \\ +\textit{mangled\_preds}?, \textit{mangled\_tags}?:} \\ The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types}, \textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and virtually sound---except for pathological cases, all found proofs are @@ -628,8 +624,8 @@ \item[$\bullet$] \textbf{% -\textit{simple\_types}!, -\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\ +\textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\ +\textit{simple\_types}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\ The type systems \textit{poly\_preds}, \textit{poly\_tags}, \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types}, \textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat diff -r 887789ed4b49 -r c9552e617acc src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 @@ -120,13 +120,22 @@ |> (fn (poly, (level, core)) => case (core, (poly, level)) of ("simple_types", (NONE, level)) => Simple_Types level + | ("preds", (SOME Polymorphic, level)) => + if level = All_Types then Preds (Polymorphic, level) + else raise Same.SAME | ("preds", (SOME poly, level)) => Preds (poly, level) + | ("tags", (SOME Polymorphic, level)) => + if level = All_Types orelse level = Finite_Types then + Tags (Polymorphic, level) + else + raise Same.SAME | ("tags", (SOME poly, level)) => Tags (poly, level) | ("args", (SOME poly, All_Types (* naja *))) => Preds (poly, Const_Arg_Types) | ("erased", (NONE, All_Types (* naja *))) => Preds (Polymorphic, No_Types) - | _ => error ("Unknown type system: " ^ quote s ^ ".")) + | _ => raise Same.SAME) + handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic | polymorphism_of_type_sys (Preds (poly, _)) = poly @@ -188,23 +197,32 @@ | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso member (op =) boring_consts s)) -datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args +(* The Booleans indicate whether all type arguments should be kept. *) +datatype type_arg_policy = + Explicit_Type_Args of bool | + Mangled_Type_Args of bool | + No_Type_Args +(* FIXME: Find out whether and when erasing the non-result type arguments is + sound. *) fun general_type_arg_policy type_sys = if level_of_type_sys type_sys = No_Types then No_Type_Args else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then - Mangled_Type_Args + Mangled_Type_Args (is_type_sys_virtually_sound type_sys) else - Explicit_Type_Args + Explicit_Type_Args (is_type_sys_virtually_sound type_sys) fun type_arg_policy type_sys s = if should_omit_type_args type_sys s then No_Type_Args else general_type_arg_policy type_sys fun num_atp_type_args thy type_sys s = - if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s - else 0 + case type_arg_policy type_sys s of + Explicit_Type_Args keep_all => + if keep_all then num_type_args thy s + else error "not implemented yet" (* FIXME *) + | _ => 0 fun atp_type_literals_for_types type_sys kind Ts = if level_of_type_sys type_sys = No_Types then @@ -589,10 +607,31 @@ | (head, args) => list_explicit_app head (map aux args) in aux end -fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = +fun chop_fun 0 T = ([], T) + | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = + chop_fun (n - 1) ran_T |>> cons dom_T + | chop_fun _ _ = raise Fail "unexpected non-function" + +fun filter_type_args thy s arity T_args = let - fun aux (CombApp tmp) = CombApp (pairself aux tmp) - | aux (CombConst (name as (s, _), T, T_args)) = + val U = s |> Sign.the_const_type thy (* may throw "TYPE" *) + val res_U = U |> chop_fun arity |> snd + val res_U_vars = Term.add_tvarsT res_U [] + val U_args = (s, U) |> Sign.const_typargs thy + in + U_args ~~ T_args + |> map_filter (fn (U, T) => + if member (op =) res_U_vars (dest_TVar U) then SOME T + else NONE) + end + handle TYPE _ => T_args + +fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = + let + val thy = Proof_Context.theory_of ctxt + fun aux arity (CombApp (tm1, tm2)) = + CombApp (aux (arity + 1) tm1, aux 0 tm2) + | aux arity (CombConst (name as (s, _), T, T_args)) = let val level = level_of_type_sys type_sys val (T, T_args) = @@ -604,7 +643,7 @@ not (is_type_sys_virtually_sound type_sys) then T_args |> map (homogenized_type ctxt nonmono_Ts level) |> (fn Ts => let val T = hd Ts --> nth Ts 1 in - (T --> T, tl Ts) + (T --> T, tl Ts) (* ### FIXME: need tl? *) end) else (T, T_args) @@ -612,21 +651,26 @@ (case strip_prefix_and_unascii const_prefix s of NONE => (name, T_args) | SOME s'' => - let val s'' = invert_const s'' in + let + val s'' = invert_const s'' + fun filtered_T_args true = T_args + | filtered_T_args false = filter_type_args thy s'' arity T_args + in case type_arg_policy type_sys s'' of - No_Type_Args => (name, []) - | Explicit_Type_Args => (name, T_args) - | Mangled_Type_Args => (mangled_const_name T_args name, []) + Explicit_Type_Args keep_all => (name, filtered_T_args keep_all) + | Mangled_Type_Args keep_all => + (mangled_const_name (filtered_T_args keep_all) name, []) + | No_Type_Args => (name, []) end) |> (fn (name, T_args) => CombConst (name, T, T_args)) end - | aux tm = tm - in aux end + | aux _ tm = tm + in aux 0 end fun repair_combterm ctxt nonmono_Ts type_sys sym_tab = introduce_explicit_apps_in_combterm sym_tab #> introduce_predicators_in_combterm sym_tab - #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys + #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys fun repair_fact ctxt nonmono_Ts type_sys sym_tab = update_combformula (formula_map (repair_combterm ctxt nonmono_Ts type_sys sym_tab)) @@ -653,7 +697,9 @@ ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), Chained), let val t = th |> prop_of in - t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso + t |> ((case general_type_arg_policy type_sys of + Mangled_Type_Args _ => true + | _ => false) andalso not (null (Term.hidden_polymorphism t))) ? (case typ of SOME T => specialize_type thy (invert_const unmangled_s, T) @@ -716,14 +762,14 @@ fun type_pred_combatom ctxt nonmono_Ts type_sys T tm = CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), tm) - |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys + |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |> AAtom fun formula_from_combformula ctxt nonmono_Ts type_sys = let fun tag_with_type type_sys T tm = CombConst (`make_fixed_const type_tag_name, T --> T, [T]) - |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys + |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |> do_term true |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) and do_term top_level u = @@ -852,7 +898,7 @@ fun should_declare_sym type_sys pred_sym s = not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso - not (String.isPrefix "$" s) andalso + not (String.isPrefix tptp_special_prefix s) andalso ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym) fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) = @@ -904,15 +950,10 @@ (* in case helper "True_or_False" is included *) #> insert_type I @{typ bool}) -fun n_ary_strip_type 0 T = ([], T) - | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) = - n_ary_strip_type (n - 1) ran_T |>> cons dom_T - | n_ary_strip_type _ _ = raise Fail "unexpected non-function" - -fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd +fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) = - let val (arg_Ts, res_T) = n_ary_strip_type ary T in + let val (arg_Ts, res_T) = chop_fun ary T in Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts, if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) end @@ -925,7 +966,7 @@ val (kind, maybe_negate) = if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) else (Axiom, I) - val (arg_Ts, res_T) = n_ary_strip_type ary T + val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) val bound_tms = @@ -1073,7 +1114,7 @@ fun add_term_weights weight (ATerm (s, tms)) = (not (is_atp_variable s) andalso s <> "equal" andalso - not (String.isPrefix "$" s)) ? Symtab.default (s, weight) + not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = formula_fold true (K (add_term_weights weight)) phi