# HG changeset patch # User blanchet # Date 1304542593 -7200 # Node ID 2123b2608b14def059da993d63dc6c5ee7433bce # Parent e60326e7ee95dee1c108487e51f80fd36e56876c renamed "many_typed" to "simple" (as in simple types) diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 04 22:54:10 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed May 04 22:56:33 2011 +0200 @@ -378,14 +378,14 @@ val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] val remote_tofof_e = remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) - Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"] + Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"] val remote_sine_e = remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *)) (#best_type_systems e_config) val remote_snark = remote_atp snarkN "SNARK" ["20080805r024"] [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof] - (K 250 (* FUDGE *)) ["many_typed"] + (K 250 (* FUDGE *)) ["simple"] (* Setup *) diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 22:54:10 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 22:56:33 2011 +0200 @@ -17,7 +17,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Many_Typed of type_level | + Simple of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -96,7 +96,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Many_Typed of type_level | + Simple of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -116,7 +116,7 @@ | NONE => (All_Types, s)) |> (fn (polymorphism, (level, core)) => case (core, (polymorphism, level)) of - ("many_typed", (Polymorphic (* naja *), level)) => Many_Typed level + ("simple", (Polymorphic (* naja *), level)) => Simple level | ("preds", extra) => Preds extra | ("tags", extra) => Tags extra | ("args", (_, All_Types (* naja *))) => @@ -125,11 +125,11 @@ Preds (polymorphism, No_Types) | _ => error ("Unknown type system: " ^ quote s ^ ".")) -fun polymorphism_of_type_sys (Many_Typed _) = Mangled_Monomorphic +fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic | polymorphism_of_type_sys (Preds (poly, _)) = poly | polymorphism_of_type_sys (Tags (poly, _)) = poly -fun level_of_type_sys (Many_Typed level) = level +fun level_of_type_sys (Simple level) = level | level_of_type_sys (Preds (_, level)) = level | level_of_type_sys (Tags (_, level)) = level @@ -783,7 +783,7 @@ end val do_bound_type = case type_sys of - Many_Typed level => + Simple level => SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level | _ => K NONE fun do_out_of_bound_type (s, T) = @@ -886,7 +886,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 - ((case type_sys of Many_Typed _ => true | _ => false) orelse not pred_sym) + ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym) fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab = let @@ -980,7 +980,7 @@ fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) = case type_sys of - Many_Typed _ => map (decl_line_for_sym s) decls + Simple _ => map (decl_line_for_sym s) decls | _ => let val decls = @@ -1077,7 +1077,7 @@ val problem = problem |> (case type_sys of - Many_Typed _ => + Simple _ => cons (type_declsN, map decl_line_for_tff_type (tff_types_in_problem problem)) | _ => I) diff -r e60326e7ee95 -r 2123b2608b14 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 04 22:54:10 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 04 22:56:33 2011 +0200 @@ -346,14 +346,14 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Polymorphic, Const_Arg_Types), Many_Typed All_Types] + [Preds (Polymorphic, Const_Arg_Types), Simple All_Types] -fun adjust_dumb_type_sys formats (Many_Typed level) = - if member (op =) formats Tff then (Tff, Many_Typed level) +fun adjust_dumb_type_sys formats (Simple level) = + if member (op =) formats Tff then (Tff, Simple level) else (Fof, Preds (Mangled_Monomorphic, level)) | adjust_dumb_type_sys formats type_sys = if member (op =) formats Fof then (Fof, type_sys) - else (Tff, Many_Typed (level_of_type_sys type_sys)) + else (Tff, Simple (level_of_type_sys type_sys)) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats