1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:38 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:38 2011 +0200
1.3 @@ -632,28 +632,28 @@
1.4 level_of_type_enc type_enc = All_Types andalso
1.5 heaviness_of_type_enc type_enc = Heavyweight
1.6
1.7 -fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
1.8 - | general_type_arg_policy type_enc =
1.9 - if level_of_type_enc type_enc = No_Types then
1.10 - No_Type_Args
1.11 - else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.12 - Mangled_Type_Args (should_drop_arg_type_args type_enc)
1.13 - else
1.14 - Explicit_Type_Args (should_drop_arg_type_args type_enc)
1.15 -
1.16 fun type_arg_policy type_enc s =
1.17 - if s = @{const_name HOL.eq} orelse
1.18 - (s = app_op_name andalso level_of_type_enc type_enc = Const_Arg_Types) then
1.19 - No_Type_Args
1.20 - else if s = type_tag_name then
1.21 + if s = type_tag_name then
1.22 (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.23 Mangled_Type_Args
1.24 else
1.25 Explicit_Type_Args) false
1.26 - else
1.27 - general_type_arg_policy type_enc
1.28 + else case type_enc of
1.29 + Tags (_, All_Types, Heavyweight) => No_Type_Args
1.30 + | _ =>
1.31 + if level_of_type_enc type_enc = No_Types orelse
1.32 + s = @{const_name HOL.eq} orelse
1.33 + (s = app_op_name andalso
1.34 + level_of_type_enc type_enc = Const_Arg_Types) then
1.35 + No_Type_Args
1.36 + else
1.37 + should_drop_arg_type_args type_enc
1.38 + |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.39 + Mangled_Type_Args
1.40 + else
1.41 + Explicit_Type_Args)
1.42
1.43 -(*Make literals for sorted type variables*)
1.44 +(* Make literals for sorted type variables. *)
1.45 fun generic_add_sorts_on_type (_, []) = I
1.46 | generic_add_sorts_on_type ((x, i), s :: ss) =
1.47 generic_add_sorts_on_type ((x, i), ss)
1.48 @@ -1314,9 +1314,9 @@
1.49 end
1.50
1.51 fun should_specialize_helper type_enc t =
1.52 - case general_type_arg_policy type_enc of
1.53 - Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1.54 - | _ => false
1.55 + polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
1.56 + level_of_type_enc type_enc <> No_Types andalso
1.57 + not (null (Term.hidden_polymorphism t))
1.58
1.59 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1.60 case strip_prefix_and_unascii const_prefix s of
1.61 @@ -1324,18 +1324,21 @@
1.62 let
1.63 val thy = Proof_Context.theory_of ctxt
1.64 val unmangled_s = mangled_s |> unmangled_const_name
1.65 + fun dub needs_fairly_sound j k =
1.66 + (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1.67 + (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1.68 + (if needs_fairly_sound then typed_helper_suffix
1.69 + else untyped_helper_suffix),
1.70 + Helper)
1.71 fun dub_and_inst needs_fairly_sound (th, j) =
1.72 - ((unmangled_s ^ "_" ^ string_of_int j ^
1.73 - (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1.74 - (if needs_fairly_sound then typed_helper_suffix
1.75 - else untyped_helper_suffix),
1.76 - Helper),
1.77 - let val t = th |> prop_of in
1.78 - t |> should_specialize_helper type_enc t
1.79 - ? (case types of
1.80 - [T] => specialize_type thy (invert_const unmangled_s, T)
1.81 - | _ => I)
1.82 - end)
1.83 + let val t = prop_of th in
1.84 + if should_specialize_helper type_enc t then
1.85 + map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1.86 + types
1.87 + else
1.88 + [t]
1.89 + end
1.90 + |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1.91 val make_facts =
1.92 map_filter (make_fact ctxt format type_enc false false [])
1.93 val fairly_sound = is_type_enc_fairly_sound type_enc
1.94 @@ -1347,7 +1350,7 @@
1.95 []
1.96 else
1.97 ths ~~ (1 upto length ths)
1.98 - |> map (dub_and_inst needs_fairly_sound)
1.99 + |> maps (dub_and_inst needs_fairly_sound)
1.100 |> make_facts)
1.101 end
1.102 | NONE => []