# HG changeset patch # User blanchet # Date 1304340057 -7200 # Node ID 23b13b1bd565afbac545accbc4067753a623c872 # Parent bb9143d7e2174e52974729197adc59c0892f73fb use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 02 14:40:57 2011 +0200 @@ -11,15 +11,6 @@ type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure - 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 | - Preds of polymorphism * type_level | - Tags of polymorphism * type_level - type atp_config = {exec : string * string, required_execs : (string * string) list, @@ -29,15 +20,11 @@ hypothesis_kind : formula_kind, formats : format list, best_slices : unit -> (real * (bool * int)) list, - best_type_systems : type_system list} + best_type_systems : string list} 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 @@ -58,7 +45,7 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> format list -> (unit -> int) - -> type_system list -> string * atp_config + -> string list -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -75,35 +62,6 @@ (* ATP configuration *) -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 | - Preds of polymorphism * type_level | - Tags of polymorphism * type_level - -val mangled_preds = Preds (Mangled_Monomorphic, All_Types) -val const_args = Preds (Polymorphic, Const_Arg_Types) - -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 = All_Types - | level_of_type_sys (Preds (_, level)) = level - | level_of_type_sys (Tags (_, level)) = level - -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, required_execs : (string * string) list, @@ -113,7 +71,7 @@ hypothesis_kind : formula_kind, formats : format list, best_slices : unit -> (real * (bool * int)) list, - best_type_systems : type_system list} + best_type_systems : string list} val known_perl_failures = [(CantConnect, "HTTP error"), @@ -240,7 +198,7 @@ (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)] else [(1.0, (true, 250 (* FUDGE *)))], - best_type_systems = [const_args, mangled_preds]} + best_type_systems = ["const_args", "mangled_preds"]} val e = (eN, e_config) @@ -271,7 +229,7 @@ best_slices = K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *), (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)], - best_type_systems = [mangled_preds]} + best_type_systems = ["mangled_preds"]} val spass = (spassN, spass_config) @@ -307,7 +265,7 @@ best_slices = K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *), (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)], - best_type_systems = [mangled_preds]} + best_type_systems = ["mangled_preds"]} val vampire = (vampireN, vampire_config) diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 14:40:57 2011 +0200 @@ -46,7 +46,6 @@ open ATP_Problem open ATP_Proof -open ATP_Systems open Metis_Translate open Sledgehammer_Util open Sledgehammer_Filter diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 14:40:57 2011 +0200 @@ -10,7 +10,16 @@ sig type 'a fo_term = 'a ATP_Problem.fo_term type 'a problem = 'a ATP_Problem.problem - type type_system = ATP_Systems.type_system + + 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 | + Preds of polymorphism * type_level | + Tags of polymorphism * type_level + type translated_formula val readable_names : bool Unsynchronized.ref @@ -20,6 +29,11 @@ val explicit_app_base : string val type_pred_base : string val tff_type_prefix : string + val type_sys_from_string : string -> type_system + 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 val num_atp_type_args : theory -> type_system -> string -> int val unmangled_const : string -> string * string fo_term list val translate_atp_fact : @@ -37,7 +51,6 @@ struct open ATP_Problem -open ATP_Systems open Metis_Translate open Sledgehammer_Util @@ -72,6 +85,58 @@ (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" +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 | + Preds of polymorphism * type_level | + Tags of polymorphism * type_level + +fun type_sys_from_string s = + (case try (unprefix "mangled_") s of + SOME s => (Mangled_Monomorphic, s) + | NONE => + case try (unprefix "mono_") s of + SOME s => (Monomorphic, s) + | NONE => (Polymorphic, s)) + ||> (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)) => + Many_Typed + | ("preds", extra) => Preds extra + | ("tags", extra) => Tags extra + | ("const_args", (_, All_Types (* naja *))) => + Preds (polymorphism, Const_Arg_Types) + | ("erased", (Polymorphic, All_Types (* naja *))) => + Preds (polymorphism, No_Types) + | _ => error ("Unknown type system: " ^ quote s ^ ".")) + +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 = All_Types + | level_of_type_sys (Preds (_, level)) = level + | level_of_type_sys (Tags (_, level)) = level + +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 + fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 02 14:40:57 2011 +0200 @@ -233,33 +233,10 @@ val blocking = auto orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd - val type_sys = lookup_string "type_sys" val type_sys = - (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) - | ("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 ^ ".")) + case lookup_string "type_sys" of + "smart" => Smart_Type_Sys (lookup_bool "full_types") + | s => Dumb_Type_Sys (type_sys_from_string s) val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" val monomorphize_limit = lookup_int "monomorphize_limit" diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 14:40:57 2011 +0200 @@ -352,7 +352,7 @@ adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats (Smart_Type_Sys full_types) = - best_type_systems @ fallback_best_type_systems + map type_sys_from_string best_type_systems @ fallback_best_type_systems |> find_first (if full_types then is_type_sys_virtually_sound else K true) |> the |> adjust_dumb_type_sys formats diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 14:40:57 2011 +0200 @@ -23,7 +23,6 @@ structure Sledgehammer_Run : SLEDGEHAMMER_RUN = struct -open ATP_Systems open Sledgehammer_Util open Sledgehammer_Filter open Sledgehammer_ATP_Translate diff -r bb9143d7e217 -r 23b13b1bd565 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Mon May 02 14:28:28 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Mon May 02 14:40:57 2011 +0200 @@ -98,9 +98,10 @@ Sledgehammer_ATP_Translate.translate_atp_fact ctxt true ((Thm.get_name_hint th, loc), th))) val type_sys = - ATP_Systems.Preds (ATP_Systems.Polymorphic, - if full_types then ATP_Systems.All_Types - else ATP_Systems.Const_Arg_Types) + Sledgehammer_ATP_Translate.Preds + (Sledgehammer_ATP_Translate.Polymorphic, + if full_types then Sledgehammer_ATP_Translate.All_Types + else Sledgehammer_ATP_Translate.Const_Arg_Types) val explicit_apply = false val (atp_problem, _, _, _, _) = Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys