# HG changeset patch # User blanchet # Date 1304267845 -7200 # Node ID 9f7c484636456e712c786c42aa40649297fca461 # Parent 562d6415616a5631f829513ef4cb79ef5b2a8304 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" diff -r 562d6415616a -r 9f7c48463645 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:25 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:25 2011 +0200 @@ -578,57 +578,71 @@ Monomorphization can simplify reasoning but also leads to larger fact bases, which can slow down the ATPs. -\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names, -and predicates restrict the range of bound variables. The problem is -monomorphized. This corresponds to the traditional encoding of types in an -untyped logic without overloading (e.g., such as performed by the ToFoF-E -wrapper). +\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate +$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables. +Constants are annotated with their types, supplied as extra arguments, to +resolve overloading. -\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with their -types, which are supplied as extra arguments. +\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but +the problem is additionally monomorphized. This corresponds to the traditional +encoding of types in an untyped logic without overloading (e.g., such as +performed by the ToFoF-E wrapper). -\item[$\bullet$] \textbf{\textit{mono\_args}:} Similar to \textit{args}, but -the problem is additionally monomorphized. +\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to +\textit{mono\_preds}, but types are mangled in constant names instead of being +supplied as ground term arguments. The binary predicate +$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate +$\mathit{has\_type\_}\tau(t)$. -\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with -its type using a special uninterpreted function symbol. +\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with +its type using a function $\mathit{type\_info\/}(\tau, t)$. \item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but the problem is additionally monomorphized. -\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the -ATP. +\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to +\textit{mono\_tags}, but types are mangled in constant names instead of being +supplied as ground term arguments. The binary function +$\mathit{type\_info\/}(\tau, t)$ becomes a unary function +$\mathit{type\_info\_}\tau(t)$. + +\item[$\bullet$] +\textbf{% +\textit{preds}!, +\textit{mono\_preds}!, +\textit{mangled\_preds}!, \\ +\textit{tags}!, +\textit{mono\_tags}!, +\textit{mangled\_tags}!:} \\ +The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds}, +\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed +and virtually sound. For each of these, Sledgehammer also provides a mildly +unsound variant identified by an exclamation mark (!)\ that types only finite +(and hence especially dangerous) types. \item[$\bullet$] \textbf{% -\textit{many\_typed}!, -\textit{mangled}!, -\textit{args}!, -\textit{mono\_args}!, -\textit{tags}!, \\ %% TYPESETTING -\textit{mono\_tags}!:} -The type systems \textit{many\_typed}, \textit{mangled}, -(\textit{mono\_})\allowbreak\textit{args}, and -(\textit{mono\_})\allowbreak\textit{tags} are fully typed and (virtually) sound. -For each of these, Sledgehammer also provides a mildly unsound variant -identified by one exclamation mark suffix (!). +\textit{preds}?, +\textit{mono\_preds}?, +\textit{mangled\_preds}?, \\ +\textit{tags}?, +\textit{mono\_tags}?, +\textit{mangled\_tags}?:} \\ +If the exclamation mark (!) is replaced by an question mark (?), the type +systems type only nonmonotonic (and hence especially dangerous) types. Not +implemented yet. -\item[$\bullet$] -\textbf{% -\textit{many\_typed}!!, -\textit{mangled}!!, -\textit{args}!!, -\textit{mono\_args}!!, -\textit{tags}!!, \\ %% TYPESETTING -\textit{mono\_tags}!!:} -More strongly unsound variants of \textit{many\_typed}, \textit{mangled}, -(\textit{mono\_})\allowbreak\textit{args}, and -(\textit{mono\_})\allowbreak\textit{tags}, identified by two exclamation marks -(!!). +\item[$\bullet$] \textbf{\textit{const\_args}:} +Constants are annotated with their types, supplied as extra arguments, to +resolve overloading. Variables are unbounded. + +\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to +the ATP. Types are simply erased. \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, -uses a fully typed encoding; otherwise, uses a partially typed encoding. The -actual encoding used depends on the ATP. +uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The +actual encoding used depends on the ATP and should be the most efficient for +that ATP. \end{enum} For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}. diff -r 562d6415616a -r 9f7c48463645 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200 @@ -377,7 +377,8 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys + val fairly_sound = + Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val time_limit = (case hard_timeout of NONE => I @@ -387,7 +388,7 @@ time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val facts = - Sledgehammer_Filter.relevant_facts ctxt half_sound + Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r 562d6415616a -r 9f7c48463645 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 @@ -117,18 +117,18 @@ val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing prover - val is_built_in_const = - Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover + val is_built_in_const = + Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover val relevance_fudge = extract_relevance_fudge args (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal - val half_sound = - Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys + val fairly_sound = + Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt half_sound + Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override facts hyp_ts concl_t diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200 @@ -164,7 +164,7 @@ | keep (c :: cs) = c :: keep cs in String.explode #> rev #> keep #> rev #> String.implode end -val max_readable_name_length = 32 +val max_readable_name_length = 24 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure @@ -184,7 +184,7 @@ if size s > max_readable_name_length then String.substring (s, 0, max_readable_name_length div 2 - 4) ^ Word.toString (hashw_string (full_name, 0w0)) ^ - String.extract (s, max_readable_name_length div 2 - 4, NONE) + String.extract (s, max_readable_name_length div 2 + 4, NONE) else s) |> (fn s => if member (op =) reserved_nice_names s then full_name else s) diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 @@ -11,13 +11,14 @@ type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure - datatype type_level = Sound | Half_Sound | Unsound + datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic + datatype type_level = + All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types + datatype type_system = Many_Typed | - Mangled of type_level | - Args of bool * type_level | - Tags of bool * type_level | - No_Types + Preds of polymorphism * type_level | + Tags of polymorphism * type_level type atp_config = {exec : string * string, @@ -33,7 +34,10 @@ datatype e_weight_method = E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight + val polymorphism_of_type_sys : type_system -> polymorphism val level_of_type_sys : type_system -> type_level + val is_type_sys_virtually_sound : type_system -> bool + val is_type_sys_fairly_sound : type_system -> bool (* for experimentation purposes -- do not use in production code *) val e_weight_method : e_weight_method Unsynchronized.ref val e_default_fun_weight : real Unsynchronized.ref @@ -71,19 +75,31 @@ (* ATP configuration *) -datatype type_level = Sound | Half_Sound | Unsound +datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic +datatype type_level = + All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types + datatype type_system = Many_Typed | - Mangled of type_level | - Args of bool * type_level | - Tags of bool * type_level | - No_Types + Preds of polymorphism * type_level | + Tags of polymorphism * type_level + +fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic + | polymorphism_of_type_sys (Preds (poly, _)) = poly + | polymorphism_of_type_sys (Tags (poly, _)) = poly -fun level_of_type_sys Many_Typed = Sound - | level_of_type_sys (Mangled level) = level - | level_of_type_sys (Args (_, level)) = level +fun level_of_type_sys Many_Typed = All_Types + | level_of_type_sys (Preds (_, level)) = level | level_of_type_sys (Tags (_, level)) = level - | level_of_type_sys No_Types = Unsound + +val is_type_level_virtually_sound = + member (op =) [All_Types, Nonmonotonic_Types] +val is_type_sys_virtually_sound = + is_type_level_virtually_sound o level_of_type_sys + +fun is_type_level_fairly_sound level = + is_type_level_virtually_sound level orelse level = Finite_Types +val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys type atp_config = {exec : string * string, diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200 @@ -194,7 +194,7 @@ | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " fun metis_name type_sys = - if level_of_type_sys type_sys = Unsound then "metis" else "metisFT" + if is_type_sys_fairly_sound type_sys then "metisFT" else "metis" fun metis_call type_sys ss = command_call (metis_name type_sys) ss fun metis_command type_sys i n (ls, ss) = using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss @@ -342,12 +342,7 @@ fun aux opt_T extra_us u = case u of ATerm (a, us) => - if a = type_tag_name then - case us of - [typ_u, term_u] => - aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u - | _ => raise FO_TERM us - else if String.isPrefix tff_type_prefix a then + if String.isPrefix tff_type_prefix a then @{const True} (* ignore TFF type information *) else case strip_prefix_and_unascii const_prefix a of SOME "equal" => @@ -360,7 +355,12 @@ end | SOME b => let val (b, mangled_us) = b |> unmangled_const |>> invert_const in - if b = predicator_base then + if b = type_tag_name then + case mangled_us @ us of + [typ_u, term_u] => + aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u + | _ => raise FO_TERM us + else if b = predicator_base then aux (SOME @{typ bool}) [] (hd us) else if b = explicit_app_base then aux opt_T (nth us 1 :: extra_us) (hd us) diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 @@ -42,7 +42,9 @@ open Sledgehammer_Util (* Readable names are often much shorter, especially if types are mangled in - names. For that reason, they are on by default. *) + names. Also, the logic for generating legal SNARK sort names is only + implemented for readable names. Finally, readable names are, well, more + readable. For these reason, they are enabled by default. *) val readable_names = Unsynchronized.ref true val type_decl_prefix = "type_" @@ -91,29 +93,25 @@ fun fact_lift f ({combformula, ...} : translated_formula) = f combformula -fun type_sys_declares_sym_types Many_Typed = true - | type_sys_declares_sym_types (Mangled level) = level <> Unsound - | type_sys_declares_sym_types (Args (_, level)) = level <> Unsound - | type_sys_declares_sym_types _ = false - val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] fun should_omit_type_args type_sys s = - s <> type_pred_base andalso - (s = @{const_name HOL.eq} orelse - case type_sys of - Many_Typed => false - | Mangled _ => false - | Tags (_, Sound) => true - | No_Types => true - | _ => member (op =) boring_consts s) + s <> type_pred_base andalso s <> type_tag_name andalso + (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse + (case type_sys of + Tags (_, All_Types) => true + | _ => 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 -datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args - -fun general_type_arg_policy Many_Typed = Mangled_Types - | general_type_arg_policy (Mangled _) = Mangled_Types - | general_type_arg_policy No_Types = No_Type_Args - | general_type_arg_policy _ = Explicit_Type_Args +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 + else + Explicit_Type_Args fun type_arg_policy type_sys s = if should_omit_type_args type_sys s then No_Type_Args @@ -124,7 +122,7 @@ else 0 fun atp_type_literals_for_types type_sys kind Ts = - if type_sys = No_Types then + if level_of_type_sys type_sys = No_Types then [] else Ts |> type_literals_for_types @@ -486,8 +484,8 @@ let val s'' = invert_const s'' in case type_arg_policy type_sys s'' of No_Type_Args => (name, []) - | Mangled_Types => (mangled_const_name T_args name, []) | Explicit_Type_Args => (name, T_args) + | Mangled_Type_Args => (mangled_const_name T_args name, []) end) |> (fn (name, T_args) => CombConst (name, T, T_args)) | aux tm = tm @@ -504,7 +502,7 @@ fun ti_ti_helper_fact () = let fun var s = ATerm (`I s, []) - fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) + fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) in Formula (helper_prefix ^ ascii_of "ti_ti", Axiom, AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) @@ -521,7 +519,7 @@ ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), false), let val t = th |> prop_of in - t |> (general_type_arg_policy type_sys = Mangled_Types andalso + t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso not (null (Term.hidden_polymorphism t))) ? (case typ of SOME T => specialize_type thy (invert_const unmangled_s, T) @@ -529,12 +527,12 @@ end) fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false) + val has_some_types = is_type_sys_fairly_sound type_sys in metis_helpers |> maps (fn (metis_s, (needs_some_types, ths)) => if metis_s <> unmangled_s orelse - (needs_some_types andalso - level_of_type_sys type_sys = Unsound) then + (needs_some_types andalso not has_some_types) then [] else ths ~~ (1 upto length ths) @@ -567,15 +565,13 @@ val tycons = type_consts_of_terms thy all_ts val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) val (supers', arity_clauses) = - if type_sys = No_Types then ([], []) + if level_of_type_sys type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) end -fun tag_with_type ty tm = ATerm (`I type_tag_name, [ty, tm]) - fun fo_literal_from_type_literal (TyLitVar (class, name)) = (true, ATerm (class, [ATerm (name, [])])) | fo_literal_from_type_literal (TyLitFree (class, name)) = @@ -588,39 +584,39 @@ unsound ATP proofs. The checks below are an (unsound) approximation of finiteness. *) -fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true - | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = - is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us - | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false -and is_type_dangerous ctxt (Type (s, Ts)) = - is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts - | is_type_dangerous _ _ = false -and is_type_constr_dangerous ctxt s = +fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true + | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) = + is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us + | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false +and is_type_finite ctxt (Type (s, Ts)) = + is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts + | is_type_finite _ _ = false +and is_type_constr_finite ctxt s = let val thy = Proof_Context.theory_of ctxt in case Datatype_Data.get_info thy s of SOME {descr, ...} => forall (fn (_, (_, _, constrs)) => - forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr + forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr | NONE => case Typedef.get_info ctxt s of - ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type + ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type | [] => true end -fun should_encode_type _ Sound _ = true - | should_encode_type ctxt Half_Sound T = is_type_dangerous ctxt T - | should_encode_type _ Unsound _ = false +fun should_encode_type _ All_Types _ = true + | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T + | should_encode_type _ Nonmonotonic_Types _ = + error "Monotonicity inference not implemented yet." + | should_encode_type _ _ _ = false + +fun should_predicate_on_type ctxt (Preds (_, level)) T = + should_encode_type ctxt level T + | should_predicate_on_type _ _ _ = false fun should_tag_with_type ctxt (Tags (_, level)) T = should_encode_type ctxt level T | should_tag_with_type _ _ _ = false -fun should_predicate_on_type ctxt (Mangled level) T = - should_encode_type ctxt level T - | should_predicate_on_type ctxt (Args (_, level)) T = - should_encode_type ctxt level T - | should_predicate_on_type _ _ _ = false - fun type_pred_combatom type_sys T tm = CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), tm) @@ -629,7 +625,12 @@ fun formula_from_combformula ctxt type_sys = let - fun do_term top_level u = + fun tag_with_type type_sys T tm = + CombConst (`make_fixed_const type_tag_name, T --> T, [T]) + |> impose_type_arg_policy_in_combterm type_sys + |> do_term true + |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) + and do_term top_level u = let val (head, args) = strip_combterm_comb u val (x, T_args) = @@ -642,7 +643,7 @@ val T = combtyp_of u in t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then - tag_with_type (fo_term_from_typ T) + tag_with_type type_sys T else I) end @@ -735,7 +736,7 @@ let fun declare_sym (decl as (_, _, T, _, _)) decls = case type_sys of - Tags (false, Sound) => + Preds (Polymorphic, All_Types) => if exists (curry Type.raw_instance T o #3) decls then decls else @@ -760,7 +761,7 @@ fact_lift (formula_fold (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)) fun sym_decl_table_for_facts type_sys repaired_sym_tab facts = - Symtab.empty |> type_sys_declares_sym_types type_sys + Symtab.empty |> is_type_sys_fairly_sound type_sys ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab) facts @@ -787,10 +788,8 @@ bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) val bound_Ts = arg_Ts |> map (if n > 1 then SOME else K NONE) - val freshener = - case type_sys of Args _ => string_of_int j ^ "_" | _ => "" in - Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, + Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom, CombConst ((s, s'), T, T_args) |> fold (curry (CombApp o swap)) bound_tms |> type_pred_combatom type_sys res_T @@ -884,7 +883,9 @@ (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys) (0 upto length helpers - 1 ~~ helpers) |> (case type_sys of - Tags (_, Half_Sound) => cons (ti_ti_helper_fact ()) + Tags (Polymorphic, level) => + member (op =) [Finite_Types, Nonmonotonic_Types] level + ? cons (ti_ti_helper_fact ()) | _ => I)), (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs), (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200 @@ -777,17 +777,17 @@ (* Facts containing variables of type "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are omitted. *) -fun is_dangerous_term half_sound t = - not half_sound andalso +fun is_dangerous_term fairly_sound t = + not fairly_sound andalso let val t = transform_elim_term t in has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t end -fun is_theorem_bad_for_atps half_sound thm = +fun is_theorem_bad_for_atps fairly_sound thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - is_dangerous_term half_sound t orelse exists_sledgehammer_const t orelse + is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse exists_low_level_class_const t orelse is_metastrange_theorem thm orelse is_that_fact thm end @@ -800,7 +800,7 @@ val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end -fun all_facts ctxt reserved really_all half_sound +fun all_facts ctxt reserved really_all fairly_sound ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths chained_ths = let @@ -846,7 +846,7 @@ pair 1 #> fold (fn th => fn (j, rest) => (j + 1, - if is_theorem_bad_for_atps half_sound th andalso + if is_theorem_bad_for_atps fairly_sound th andalso not (member Thm.eq_thm add_ths th) then rest else @@ -890,7 +890,7 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -fun relevant_facts ctxt half_sound (threshold0, threshold1) max_relevant +fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant is_built_in_const fudge (override as {add, only, ...}) chained_ths hyp_ts concl_t = let @@ -908,7 +908,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved false half_sound fudge add_ths chained_ths) + all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths) |> instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> rearrange_facts ctxt (respect_no_atp andalso not only) diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200 @@ -235,22 +235,29 @@ |> auto ? single o hd val type_sys = lookup_string "type_sys" val type_sys = - (case try (unprefix "mono_") type_sys of - SOME s => (true, s) - | NONE => (false, type_sys)) - ||> (fn s => case try (unsuffix " !!") s of - SOME s => (Unsound, s) - | NONE => case try (unsuffix " !") s of - SOME s => (Half_Sound, s) - | NONE => (Sound, s)) - |> (fn (mono, (level, core)) => - case (core, (mono, level)) of - ("many_typed", (false, Sound)) => Dumb_Type_Sys Many_Typed - | ("mangled", (false, level)) => Dumb_Type_Sys (Mangled level) - | ("args", extra) => Dumb_Type_Sys (Args extra) + (case try (unprefix "mangled_") type_sys of + SOME s => (Mangled_Monomorphic, s) + | NONE => + case try (unprefix "mono_") type_sys of + SOME s => (Monomorphic, s) + | NONE => (Polymorphic, type_sys)) + ||> (fn s => case try (unsuffix " ?") s of + SOME s => (Nonmonotonic_Types, s) + | NONE => + case try (unsuffix " !") s of + SOME s => (Finite_Types, s) + | NONE => (All_Types, s)) + |> (fn (polymorphism, (level, core)) => + case (core, (polymorphism, level)) of + ("many_typed", (Polymorphic (* naja *), All_Types)) => + Dumb_Type_Sys Many_Typed + | ("preds", extra) => Dumb_Type_Sys (Preds extra) | ("tags", extra) => Dumb_Type_Sys (Tags extra) - | ("none", (false, Sound)) => Dumb_Type_Sys No_Types - | ("smart", (false, Sound)) => + | ("const_args", (_, All_Types (* naja *))) => + Dumb_Type_Sys (Preds (polymorphism, Const_Arg_Types)) + | ("erased", (Polymorphic, All_Types (* naja *))) => + Dumb_Type_Sys (Preds (polymorphism, No_Types)) + | ("smart", (Polymorphic, All_Types) (* naja *)) => Smart_Type_Sys (lookup_bool "full_types") | _ => error ("Unknown type system: " ^ quote type_sys ^ ".")) val relevance_thresholds = lookup_real_pair "relevance_thresholds" @@ -351,7 +358,7 @@ val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " val parse_value = - Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "!!" + Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?" || Parse.$$$ "!") val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 @@ -86,7 +86,7 @@ val weight_smt_fact : theory -> int -> ((string * locality) * thm) * int -> (string * locality) * (int option * thm) - val is_rich_type_sys_half_sound : rich_type_system -> bool + val is_rich_type_sys_fairly_sound : rich_type_system -> bool val untranslated_fact : prover_fact -> (string * locality) * thm val smt_weighted_fact : theory -> int -> prover_fact * int @@ -313,9 +313,9 @@ fun weight_smt_fact thy num_facts ((info, th), j) = (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy)) -fun is_rich_type_sys_half_sound (Dumb_Type_Sys type_sys) = - level_of_type_sys type_sys <> Unsound - | is_rich_type_sys_half_sound (Smart_Type_Sys full_types) = full_types +fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) = + is_type_sys_fairly_sound type_sys + | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types fun untranslated_fact (Untranslated_Fact p) = p | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) @@ -339,17 +339,12 @@ them each time. *) val atp_important_message_keep_factor = 0.1 -fun type_sys_monomorphizes Many_Typed = true - | type_sys_monomorphizes (Mangled _) = true - | type_sys_monomorphizes (Args (mono, _)) = mono - | type_sys_monomorphizes (Tags (mono, _)) = mono - | type_sys_monomorphizes No_Types = false - -val fallback_best_type_systems = [Args (false, Unsound), Many_Typed] +val fallback_best_type_systems = + [Preds (Polymorphic, Const_Arg_Types), Many_Typed] fun adjust_dumb_type_sys formats Many_Typed = if member (op =) formats Tff then (Tff, Many_Typed) - else (Fof, Mangled Sound) + else (Fof, Preds (Mangled_Monomorphic, All_Types)) | adjust_dumb_type_sys formats type_sys = if member (op =) formats Fof then (Fof, type_sys) else (Tff, Many_Typed) @@ -358,8 +353,8 @@ | determine_format_and_type_sys best_type_systems formats (Smart_Type_Sys full_types) = best_type_systems @ fallback_best_type_systems - |> full_types ? filter (curry (op =) Sound o level_of_type_sys) - |> hd |> adjust_dumb_type_sys formats + |> find_first (if full_types then is_type_sys_virtually_sound else K true) + |> the |> adjust_dumb_type_sys formats fun run_atp auto name ({exec, required_execs, arguments, proof_delims, known_failures, @@ -443,7 +438,8 @@ |> not (null blacklist) ? filter_out (member (op =) blacklist o fst o untranslated_fact) - |> type_sys_monomorphizes type_sys ? monomorphize_facts + |> polymorphism_of_type_sys type_sys <> Polymorphic + ? monomorphize_facts |> map (atp_translated_fact ctxt) val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = @@ -507,7 +503,7 @@ NONE => if is_unsound_proof conjecture_shape facts_offset fact_names atp_proof then - SOME (UnsoundProof (level_of_type_sys type_sys = Sound)) + SOME (UnsoundProof (is_type_sys_virtually_sound type_sys)) else NONE | SOME Unprovable => diff -r 562d6415616a -r 9f7c48463645 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200 @@ -183,7 +183,7 @@ val thy = Proof_Context.theory_of ctxt val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i - val half_sound = is_rich_type_sys_half_sound type_sys + val fairly_sound = is_rich_type_sys_fairly_sound type_sys val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -212,7 +212,7 @@ |> (if blocking then smart_par_list_map else map) (launch problem) |> exists fst |> rpair state end - fun get_facts label half_sound relevance_fudge provers = + fun get_facts label fairly_sound relevance_fudge provers = let val max_max_relevant = case max_relevant of @@ -225,7 +225,7 @@ val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) in - relevant_facts ctxt half_sound relevance_thresholds max_max_relevant + relevant_facts ctxt fairly_sound relevance_thresholds max_max_relevant is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t |> tap (fn facts => @@ -246,7 +246,7 @@ accum else launch_provers state - (get_facts "ATP" half_sound atp_relevance_fudge o K atps) + (get_facts "ATP" fairly_sound atp_relevance_fudge o K atps) (K (Untranslated_Fact o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then diff -r 562d6415616a -r 9f7c48463645 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200 @@ -32,9 +32,10 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys + val fairly_sound = + Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem =