# HG changeset patch # User blanchet # Date 1305637896 -7200 # Node ID 8794ec73ec1377f586c6c9ab0b626cfb24098d5a # Parent 8bfdcaf3055198ae6cb1718e96f0ed0ce3f2317f added syntax for "shallow" encodings diff -r 8bfdcaf30551 -r 8794ec73ec13 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 17 15:11:36 2011 +0200 @@ -16,11 +16,12 @@ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype type_level = All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types + datatype type_depth = Deep | Shallow datatype type_system = Simple_Types of type_level | - Preds of polymorphism * type_level | - Tags of polymorphism * type_level + Preds of polymorphism * type_level * type_depth | + Tags of polymorphism * type_level * type_depth type translated_formula @@ -89,11 +90,12 @@ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype type_level = All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types +datatype type_depth = Deep | Shallow datatype type_system = Simple_Types of type_level | - Preds of polymorphism * type_level | - Tags of polymorphism * type_level + Preds of polymorphism * type_level * type_depth | + Tags of polymorphism * type_level * type_depth fun try_unsuffixes ss s = fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE @@ -116,33 +118,42 @@ case try_unsuffixes ["!", "_bang"] s of SOME s => (Finite_Types, s) | NONE => (All_Types, s)) - |> (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) + ||> apsnd (fn s => + case try (unsuffix "_shallow") s of + SOME s => (Shallow, s) + | NONE => (Deep, s)) + |> (fn (poly, (level, (depth, core))) => + case (core, (poly, level, depth)) of + ("simple_types", (NONE, level, Deep (* naja *))) => + Simple_Types level + | ("preds", (SOME Polymorphic, level, depth)) => + if level = All_Types then Preds (Polymorphic, level, depth) else raise Same.SAME - | ("preds", (SOME poly, level)) => Preds (poly, level) - | ("tags", (SOME Polymorphic, level)) => + | ("preds", (SOME poly, level, depth)) => Preds (poly, level, depth) + | ("tags", (SOME Polymorphic, level, depth)) => if level = All_Types orelse level = Finite_Types then - Tags (Polymorphic, level) + Tags (Polymorphic, level, depth) 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) + | ("tags", (SOME poly, level, depth)) => Tags (poly, level, depth) + | ("args", (SOME poly, All_Types (* naja *), Deep (* naja *))) => + Preds (poly, Const_Arg_Types, Shallow) + | ("erased", (NONE, All_Types (* naja *), Deep (* naja *))) => + Preds (Polymorphic, No_Types, Shallow) | _ => 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 - | polymorphism_of_type_sys (Tags (poly, _)) = poly + | polymorphism_of_type_sys (Preds (poly, _, _)) = poly + | polymorphism_of_type_sys (Tags (poly, _, _)) = poly fun level_of_type_sys (Simple_Types level) = level - | level_of_type_sys (Preds (_, level)) = level - | level_of_type_sys (Tags (_, level)) = level + | level_of_type_sys (Preds (_, level, _)) = level + | level_of_type_sys (Tags (_, level, _)) = level + +fun depth_of_type_sys (Simple_Types _) = Shallow + | depth_of_type_sys (Preds (_, _, depth)) = depth + | depth_of_type_sys (Tags (_, _, depth)) = depth fun is_type_level_virtually_sound level = level = All_Types orelse level = Nonmonotonic_Types @@ -192,7 +203,7 @@ 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 + Tags (_, All_Types, _) => true | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso member (op =) boring_consts s)) @@ -486,11 +497,11 @@ exists (curry Type.raw_instance T) nonmono_Ts | should_encode_type _ _ _ _ = false -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T = +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, _)) T = should_encode_type ctxt nonmono_Ts level T | should_predicate_on_type _ _ _ _ = false -fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T = +fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level, _)) T = should_encode_type ctxt nonmono_Ts level T | should_tag_with_type _ _ _ _ = false @@ -1082,7 +1093,7 @@ type_sys) (0 upto length helpers - 1 ~~ helpers) |> (case type_sys of - Tags (Polymorphic, level) => + Tags (Polymorphic, level, _) => is_type_level_partial level ? cons (ti_ti_helper_fact ()) | _ => I)), diff -r 8bfdcaf30551 -r 8794ec73ec13 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 17 15:11:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 17 15:11:36 2011 +0200 @@ -404,12 +404,12 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Polymorphic, Const_Arg_Types), - Preds (Mangled_Monomorphic, Nonmonotonic_Types)] + [Preds (Polymorphic, Const_Arg_Types, Deep), + Preds (Mangled_Monomorphic, Nonmonotonic_Types, Deep)] fun adjust_dumb_type_sys formats (Simple_Types level) = if member (op =) formats Tff then (Tff, Simple_Types level) - else (Fof, Preds (Mangled_Monomorphic, level)) + else (Fof, Preds (Mangled_Monomorphic, level, Deep)) | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys diff -r 8bfdcaf30551 -r 8794ec73ec13 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Tue May 17 15:11:36 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Tue May 17 15:11:36 2011 +0200 @@ -93,15 +93,15 @@ val _ = File.write path "" val facts0 = facts_of thy val facts = - facts0 - |> map_filter (try (fn ((_, loc), (_, th)) => - Sledgehammer_ATP_Translate.translate_atp_fact ctxt true - ((Thm.get_name_hint th, loc), th))) + facts0 |> map_filter (try (fn ((_, loc), (_, th)) => + Sledgehammer_ATP_Translate.translate_atp_fact ctxt true + ((Thm.get_name_hint th, loc), th))) val type_sys = Sledgehammer_ATP_Translate.Preds (Sledgehammer_ATP_Translate.Polymorphic, if full_types then Sledgehammer_ATP_Translate.All_Types - else Sledgehammer_ATP_Translate.Const_Arg_Types) + else Sledgehammer_ATP_Translate.Const_Arg_Types, + Sledgehammer_ATP_Translate.Deep) val explicit_apply = false val (atp_problem, _, _, _, _, _) = Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom