# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID ea2a28b1938f161e039e392d285faaa7a6ee69ef # Parent b5eec0c9952874df1c19740c3534eba777d3a06f make sure the minimizer monomorphizes when it should diff -r b5eec0c99528 -r ea2a28b1938f src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -14,9 +14,9 @@ datatype type_system = Many_Typed | - Tags of bool | + Mangled of bool | Args of bool | - Mangled of bool | + Tags of bool | No_Types val fact_prefix : string @@ -81,15 +81,15 @@ datatype type_system = Many_Typed | - Tags of bool | + Mangled of bool | Args of bool | - Mangled of bool | + Tags of bool | No_Types fun is_type_system_sound Many_Typed = true - | is_type_system_sound (Tags full_types) = full_types + | is_type_system_sound (Mangled full_types) = full_types | is_type_system_sound (Args full_types) = full_types - | is_type_system_sound (Mangled full_types) = full_types + | is_type_system_sound (Tags full_types) = full_types | is_type_system_sound No_Types = false fun type_system_types_dangerous_types (Tags _) = true @@ -100,12 +100,12 @@ (member (op =) [@{const_name HOL.eq}] s orelse case type_sys of Many_Typed => false - | Tags full_types => full_types orelse s = explicit_app_base + | Mangled _ => false | Args _ => s = explicit_app_base - | Mangled _ => false + | Tags full_types => full_types orelse s = explicit_app_base | No_Types => true) -datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types +datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args fun type_arg_policy type_sys s = if dont_need_type_args type_sys s then @@ -501,8 +501,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 ty_args name, []) | Explicit_Type_Args => (name, ty_args) - | Mangled_Types => (mangled_const_name ty_args name, []) end) |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) | aux tm = tm @@ -551,7 +551,7 @@ val do_bound_type = if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE val do_out_of_bound_type = - if member (op =) [Args true, Mangled true] type_sys then + if member (op =) [Mangled true, Args true] type_sys then (fn (s, ty) => type_pred_combatom type_sys ty (CombVar (s, ty)) |> formula_for_combformula ctxt type_sys |> SOME) @@ -770,7 +770,7 @@ (* FIXME: needed? *) fun const_table_for_facts type_sys sym_tab facts = - Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys + Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys ? fold (consider_fact_consts type_sys sym_tab) facts fun strip_and_map_combtyp 0 f ty = ([], f ty) diff -r b5eec0c99528 -r ea2a28b1938f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:24 2011 +0200 @@ -235,21 +235,21 @@ val blocking = auto orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd - val (type_sys, must_monomorphize) = + val type_sys = case (lookup_string "type_sys", lookup_bool "full_types") of - ("many_typed", _) => (Many_Typed, true) - | ("tags", full_types) => (Tags full_types, false) - | ("args", full_types) => (Args full_types, false) - | ("mangled", full_types) => (Mangled full_types, true) - | ("none", false) => (No_Types, false) + ("many_typed", _) => Many_Typed + | ("mangled", full_types) => Mangled full_types + | ("args", full_types) => Args full_types + | ("tags", full_types) => Tags full_types + | ("none", false) => No_Types | (type_sys, full_types) => if member (op =) ["none", "smart"] type_sys then - (if full_types then Tags true else Args false, false) + if full_types then Tags true else Args false else error ("Unknown type system: " ^ quote type_sys ^ ".") val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" - val monomorphize = must_monomorphize orelse lookup_bool "monomorphize" + val monomorphize = lookup_bool "monomorphize" val monomorphize_limit = lookup_int "monomorphize_limit" val explicit_apply = lookup_bool "explicit_apply" val isar_proof = lookup_bool "isar_proof" diff -r b5eec0c99528 -r ea2a28b1938f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 @@ -334,6 +334,10 @@ them each time. *) val atp_important_message_keep_factor = 0.1 +fun must_monomorphize Many_Typed = true + | must_monomorphize (Mangled _) = true + | must_monomorphize _ = false + fun run_atp auto name ({exec, required_execs, arguments, slices, proof_delims, known_failures, use_conjecture_for_hypotheses, ...} : atp_config) @@ -414,7 +418,8 @@ |> not (null blacklist) ? filter_out (member (op =) blacklist o fst o untranslated_fact) - |> monomorphize ? monomorphize_facts + |> (monomorphize orelse must_monomorphize type_sys) + ? monomorphize_facts |> map (atp_translated_fact ctxt) val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout =