src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42828 8794ec73ec13
parent 42781 4b7a988a0213
child 42829 1558741f8a72
     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)),