src/HOL/Tools/ATP/atp_translate.ML
changeset 44591 0b107d11f634
parent 44589 0a1dfc6365e9
child 44593 ccf40af26ae9
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    datatype type_uniformity = Uniform | Nonuniform
     1.5  
     1.6    datatype type_enc =
     1.7 -    Simple_Types of order * type_level |
     1.8 +    Simple_Types of order * polymorphism * type_level |
     1.9      Guards of polymorphism * type_level * type_uniformity |
    1.10      Tags of polymorphism * type_level * type_uniformity
    1.11  
    1.12 @@ -547,7 +547,7 @@
    1.13  datatype type_uniformity = Uniform | Nonuniform
    1.14  
    1.15  datatype type_enc =
    1.16 -  Simple_Types of order * type_level |
    1.17 +  Simple_Types of order * polymorphism * type_level |
    1.18    Guards of polymorphism * type_level * type_uniformity |
    1.19    Tags of polymorphism * type_level * type_uniformity
    1.20  
    1.21 @@ -579,12 +579,15 @@
    1.22                  | NONE => (Nonuniform, s))
    1.23    |> (fn (poly, (level, (uniformity, core))) =>
    1.24           case (core, (poly, level, uniformity)) of
    1.25 -           ("simple", (NONE, _, Nonuniform)) =>
    1.26 -           Simple_Types (First_Order, level)
    1.27 -         | ("simple_higher", (NONE, _, Nonuniform)) =>
    1.28 -           (case level of
    1.29 -              Noninf_Nonmono_Types _ => raise Same.SAME
    1.30 -            | _ => Simple_Types (Higher_Order, level))
    1.31 +           ("simple", (SOME poly, _, Nonuniform)) =>
    1.32 +           (case poly of
    1.33 +              Raw_Monomorphic => raise Same.SAME
    1.34 +            | _ => Simple_Types (First_Order, poly, level))
    1.35 +         | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    1.36 +           (case (poly, level) of
    1.37 +              (Raw_Monomorphic, _) => raise Same.SAME
    1.38 +            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.39 +            | _ => Simple_Types (Higher_Order, poly, level))
    1.40           | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    1.41           | ("tags", (SOME Polymorphic, _, _)) =>
    1.42             Tags (Polymorphic, level, uniformity)
    1.43 @@ -596,14 +599,14 @@
    1.44           | _ => raise Same.SAME)
    1.45    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    1.46  
    1.47 -fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
    1.48 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
    1.49    | is_type_enc_higher_order _ = false
    1.50  
    1.51 -fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
    1.52 +fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
    1.53    | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
    1.54    | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
    1.55  
    1.56 -fun level_of_type_enc (Simple_Types (_, level)) = level
    1.57 +fun level_of_type_enc (Simple_Types (_, _, level)) = level
    1.58    | level_of_type_enc (Guards (_, level, _)) = level
    1.59    | level_of_type_enc (Tags (_, level, _)) = level
    1.60  
    1.61 @@ -625,11 +628,15 @@
    1.62    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    1.63    | is_type_level_monotonicity_based _ = false
    1.64  
    1.65 -fun adjust_type_enc (THF0 _) type_enc = type_enc
    1.66 -  | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
    1.67 -    Simple_Types (First_Order, level)
    1.68 -  | adjust_type_enc format (Simple_Types (_, level)) =
    1.69 -    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
    1.70 +fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
    1.71 +    Simple_Types (order, Mangled_Monomorphic, level)
    1.72 +  | adjust_type_enc (THF0 _) type_enc = type_enc
    1.73 +  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
    1.74 +    Simple_Types (First_Order, Mangled_Monomorphic, level)
    1.75 +  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
    1.76 +    Simple_Types (First_Order, poly, level)
    1.77 +  | adjust_type_enc format (Simple_Types (_, poly, level)) =
    1.78 +    adjust_type_enc format (Guards (poly, level, Uniform))
    1.79    | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
    1.80      (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
    1.81    | adjust_type_enc _ type_enc = type_enc
    1.82 @@ -1662,7 +1669,7 @@
    1.83      val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
    1.84      val do_bound_type =
    1.85        case type_enc of
    1.86 -        Simple_Types (_, level) =>
    1.87 +        Simple_Types (_, _, level) =>
    1.88          homogenized_type ctxt mono level 0
    1.89          #> ho_type_from_typ format type_enc false 0 #> SOME
    1.90        | _ => K NONE
    1.91 @@ -1940,7 +1947,7 @@
    1.92    let
    1.93      val (T_arg_Ts, level) =
    1.94        case type_enc of
    1.95 -        Simple_Types (_, level) => ([], level)
    1.96 +        Simple_Types (_, _, level) => ([], level)
    1.97        | _ => (replicate (length T_args) homo_infinite_type, No_Types)
    1.98    in
    1.99      Decl (sym_decl_prefix ^ s, (s, s'),