added syntax for "shallow" encodings
authorblanchet
Tue May 17 15:11:36 2011 +0200 (2011-05-17)
changeset 428288794ec73ec13
parent 42827 8bfdcaf30551
child 42829 1558741f8a72
added syntax for "shallow" encodings
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/tptp_export.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 17 15:11:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 17 15:11:36 2011 +0200
     1.3 @@ -16,11 +16,12 @@
     1.4    datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     1.5    datatype type_level =
     1.6      All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
     1.7 +  datatype type_depth = Deep | Shallow
     1.8  
     1.9    datatype type_system =
    1.10      Simple_Types of type_level |
    1.11 -    Preds of polymorphism * type_level |
    1.12 -    Tags of polymorphism * type_level
    1.13 +    Preds of polymorphism * type_level * type_depth |
    1.14 +    Tags of polymorphism * type_level * type_depth
    1.15  
    1.16    type translated_formula
    1.17  
    1.18 @@ -89,11 +90,12 @@
    1.19  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    1.20  datatype type_level =
    1.21    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    1.22 +datatype type_depth = Deep | Shallow
    1.23  
    1.24  datatype type_system =
    1.25    Simple_Types of type_level |
    1.26 -  Preds of polymorphism * type_level |
    1.27 -  Tags of polymorphism * type_level
    1.28 +  Preds of polymorphism * type_level * type_depth |
    1.29 +  Tags of polymorphism * type_level * type_depth
    1.30  
    1.31  fun try_unsuffixes ss s =
    1.32    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    1.33 @@ -116,33 +118,42 @@
    1.34              case try_unsuffixes ["!", "_bang"] s of
    1.35                SOME s => (Finite_Types, s)
    1.36              | NONE => (All_Types, s))
    1.37 -  |> (fn (poly, (level, core)) =>
    1.38 -         case (core, (poly, level)) of
    1.39 -           ("simple_types", (NONE, level)) => Simple_Types level
    1.40 -         | ("preds", (SOME Polymorphic, level)) =>
    1.41 -           if level = All_Types then Preds (Polymorphic, level)
    1.42 +  ||> apsnd (fn s =>
    1.43 +                case try (unsuffix "_shallow") s of
    1.44 +                  SOME s => (Shallow, s)
    1.45 +                | NONE => (Deep, s))
    1.46 +  |> (fn (poly, (level, (depth, core))) =>
    1.47 +         case (core, (poly, level, depth)) of
    1.48 +           ("simple_types", (NONE, level, Deep (* naja *))) =>
    1.49 +           Simple_Types level
    1.50 +         | ("preds", (SOME Polymorphic, level, depth)) =>
    1.51 +           if level = All_Types then Preds (Polymorphic, level, depth)
    1.52             else raise Same.SAME
    1.53 -         | ("preds", (SOME poly, level)) => Preds (poly, level)
    1.54 -         | ("tags", (SOME Polymorphic, level)) =>
    1.55 +         | ("preds", (SOME poly, level, depth)) => Preds (poly, level, depth)
    1.56 +         | ("tags", (SOME Polymorphic, level, depth)) =>
    1.57             if level = All_Types orelse level = Finite_Types then
    1.58 -             Tags (Polymorphic, level)
    1.59 +             Tags (Polymorphic, level, depth)
    1.60             else
    1.61               raise Same.SAME
    1.62 -         | ("tags", (SOME poly, level)) => Tags (poly, level)
    1.63 -         | ("args", (SOME poly, All_Types (* naja *))) =>
    1.64 -           Preds (poly, Const_Arg_Types)
    1.65 -         | ("erased", (NONE, All_Types (* naja *))) =>
    1.66 -           Preds (Polymorphic, No_Types)
    1.67 +         | ("tags", (SOME poly, level, depth)) => Tags (poly, level, depth)
    1.68 +         | ("args", (SOME poly, All_Types (* naja *), Deep (* naja *))) =>
    1.69 +           Preds (poly, Const_Arg_Types, Shallow)
    1.70 +         | ("erased", (NONE, All_Types (* naja *), Deep (* naja *))) =>
    1.71 +           Preds (Polymorphic, No_Types, Shallow)
    1.72           | _ => raise Same.SAME)
    1.73    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    1.74  
    1.75  fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
    1.76 -  | polymorphism_of_type_sys (Preds (poly, _)) = poly
    1.77 -  | polymorphism_of_type_sys (Tags (poly, _)) = poly
    1.78 +  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
    1.79 +  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
    1.80  
    1.81  fun level_of_type_sys (Simple_Types level) = level
    1.82 -  | level_of_type_sys (Preds (_, level)) = level
    1.83 -  | level_of_type_sys (Tags (_, level)) = level
    1.84 +  | level_of_type_sys (Preds (_, level, _)) = level
    1.85 +  | level_of_type_sys (Tags (_, level, _)) = level
    1.86 +
    1.87 +fun depth_of_type_sys (Simple_Types _) = Shallow
    1.88 +  | depth_of_type_sys (Preds (_, _, depth)) = depth
    1.89 +  | depth_of_type_sys (Tags (_, _, depth)) = depth
    1.90  
    1.91  fun is_type_level_virtually_sound level =
    1.92    level = All_Types orelse level = Nonmonotonic_Types
    1.93 @@ -192,7 +203,7 @@
    1.94    s <> type_pred_base andalso s <> type_tag_name andalso
    1.95    (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
    1.96     (case type_sys of
    1.97 -      Tags (_, All_Types) => true
    1.98 +      Tags (_, All_Types, _) => true
    1.99      | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
   1.100             member (op =) boring_consts s))
   1.101  
   1.102 @@ -486,11 +497,11 @@
   1.103      exists (curry Type.raw_instance T) nonmono_Ts
   1.104    | should_encode_type _ _ _ _ = false
   1.105  
   1.106 -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
   1.107 +fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, _)) T =
   1.108      should_encode_type ctxt nonmono_Ts level T
   1.109    | should_predicate_on_type _ _ _ _ = false
   1.110  
   1.111 -fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
   1.112 +fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level, _)) T =
   1.113      should_encode_type ctxt nonmono_Ts level T
   1.114    | should_tag_with_type _ _ _ _ = false
   1.115  
   1.116 @@ -1082,7 +1093,7 @@
   1.117                                               type_sys)
   1.118                        (0 upto length helpers - 1 ~~ helpers)
   1.119                    |> (case type_sys of
   1.120 -                        Tags (Polymorphic, level) =>
   1.121 +                        Tags (Polymorphic, level, _) =>
   1.122                          is_type_level_partial level
   1.123                          ? cons (ti_ti_helper_fact ())
   1.124                        | _ => I)),
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
     2.3 @@ -404,12 +404,12 @@
     2.4  val atp_important_message_keep_quotient = 10
     2.5  
     2.6  val fallback_best_type_systems =
     2.7 -  [Preds (Polymorphic, Const_Arg_Types),
     2.8 -   Preds (Mangled_Monomorphic, Nonmonotonic_Types)]
     2.9 +  [Preds (Polymorphic, Const_Arg_Types, Deep),
    2.10 +   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Deep)]
    2.11  
    2.12  fun adjust_dumb_type_sys formats (Simple_Types level) =
    2.13      if member (op =) formats Tff then (Tff, Simple_Types level)
    2.14 -    else (Fof, Preds (Mangled_Monomorphic, level))
    2.15 +    else (Fof, Preds (Mangled_Monomorphic, level, Deep))
    2.16    | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
    2.17  fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
    2.18      adjust_dumb_type_sys formats type_sys
     3.1 --- a/src/HOL/ex/tptp_export.ML	Tue May 17 15:11:36 2011 +0200
     3.2 +++ b/src/HOL/ex/tptp_export.ML	Tue May 17 15:11:36 2011 +0200
     3.3 @@ -93,15 +93,15 @@
     3.4      val _ = File.write path ""
     3.5      val facts0 = facts_of thy
     3.6      val facts =
     3.7 -      facts0
     3.8 -      |> map_filter (try (fn ((_, loc), (_, th)) =>
     3.9 -             Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
    3.10 -             ((Thm.get_name_hint th, loc), th)))
    3.11 +      facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
    3.12 +                    Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
    3.13 +                    ((Thm.get_name_hint th, loc), th)))
    3.14      val type_sys =
    3.15        Sledgehammer_ATP_Translate.Preds
    3.16            (Sledgehammer_ATP_Translate.Polymorphic,
    3.17             if full_types then Sledgehammer_ATP_Translate.All_Types
    3.18 -           else Sledgehammer_ATP_Translate.Const_Arg_Types)
    3.19 +           else Sledgehammer_ATP_Translate.Const_Arg_Types,
    3.20 +           Sledgehammer_ATP_Translate.Deep)
    3.21      val explicit_apply = false
    3.22      val (atp_problem, _, _, _, _, _) =
    3.23        Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom