1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 21 15:04:28 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 21 15:04:28 2011 +0100
1.3 @@ -608,10 +608,6 @@
1.4 | NONE => (constr All_Vars, s))
1.5 | NONE => fallback s
1.6
1.7 -fun is_incompatible_type_level poly level =
1.8 - poly = Mangled_Monomorphic andalso
1.9 - granularity_of_type_level level = Ghost_Type_Arg_Vars
1.10 -
1.11 fun type_enc_from_string soundness s =
1.12 (case try (unprefix "poly_") s of
1.13 SOME s => (SOME Polymorphic, s)
1.14 @@ -649,11 +645,16 @@
1.15 raise Same.SAME
1.16 | _ => raise Same.SAME)
1.17 | ("guards", (SOME poly, _)) =>
1.18 - if is_incompatible_type_level poly level then raise Same.SAME
1.19 - else Guards (poly, level)
1.20 + if poly = Mangled_Monomorphic andalso
1.21 + granularity_of_type_level level = Ghost_Type_Arg_Vars then
1.22 + raise Same.SAME
1.23 + else
1.24 + Guards (poly, level)
1.25 | ("tags", (SOME poly, _)) =>
1.26 - if is_incompatible_type_level poly level then raise Same.SAME
1.27 - else Tags (poly, level)
1.28 + if granularity_of_type_level level = Ghost_Type_Arg_Vars then
1.29 + raise Same.SAME
1.30 + else
1.31 + Tags (poly, level)
1.32 | ("args", (SOME poly, All_Types (* naja *))) =>
1.33 Guards (poly, Const_Arg_Types)
1.34 | ("erased", (NONE, All_Types (* naja *))) =>
1.35 @@ -1323,30 +1324,17 @@
1.36 datatype site =
1.37 Top_Level of bool option |
1.38 Eq_Arg of bool option |
1.39 - Arg of string * int * int |
1.40 Elsewhere
1.41
1.42 -fun should_tag_with_type _ _ _ _ [Top_Level _] _ _ = false
1.43 - | should_tag_with_type ctxt polym_constrs mono (Tags (_, level)) sites u T =
1.44 - (case granularity_of_type_level level of
1.45 - All_Vars => should_encode_type ctxt mono level T
1.46 - | grain =>
1.47 - case (sites, is_maybe_universal_var u) of
1.48 - (Eq_Arg _ :: _, true) => should_encode_type ctxt mono level T
1.49 - | (Arg (s, j, ary) :: site0 :: _, true) =>
1.50 - grain = Ghost_Type_Arg_Vars andalso
1.51 - let
1.52 - val thy = Proof_Context.theory_of ctxt
1.53 - fun is_ghost_type_arg s j ary =
1.54 - member (op =) (ghost_type_args thy s ary) j
1.55 - fun is_ghost_site (Arg (s, j, ary)) = is_ghost_type_arg s j ary
1.56 - | is_ghost_site _ = true
1.57 - in
1.58 - is_ghost_type_arg s j ary andalso
1.59 - (not (member (op =) polym_constrs s) orelse is_ghost_site site0)
1.60 - end
1.61 +fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1.62 + | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1.63 + if granularity_of_type_level level = All_Vars then
1.64 + should_encode_type ctxt mono level T
1.65 + else
1.66 + (case (site, is_maybe_universal_var u) of
1.67 + (Eq_Arg _, true) => should_encode_type ctxt mono level T
1.68 | _ => false)
1.69 - | should_tag_with_type _ _ _ _ _ _ _ = false
1.70 + | should_tag_with_type _ _ _ _ _ _ = false
1.71
1.72 fun fused_type ctxt mono level =
1.73 let
1.74 @@ -1822,19 +1810,19 @@
1.75 fun mk_aterm format type_enc name T_args args =
1.76 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1.77
1.78 -fun tag_with_type ctxt polym_constrs format mono type_enc pos T tm =
1.79 +fun tag_with_type ctxt format mono type_enc pos T tm =
1.80 IConst (type_tag, T --> T, [T])
1.81 |> mangle_type_args_in_iterm format type_enc
1.82 - |> ho_term_from_iterm ctxt polym_constrs format mono type_enc pos
1.83 + |> ho_term_from_iterm ctxt format mono type_enc pos
1.84 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1.85 | _ => raise Fail "unexpected lambda-abstraction")
1.86 -and ho_term_from_iterm ctxt polym_constrs format mono type_enc =
1.87 +and ho_term_from_iterm ctxt format mono type_enc =
1.88 let
1.89 - fun term sites u =
1.90 + fun term site u =
1.91 let
1.92 val (head, args) = strip_iterm_comb u
1.93 val pos =
1.94 - case hd sites of
1.95 + case site of
1.96 Top_Level pos => pos
1.97 | Eq_Arg pos => pos
1.98 | _ => NONE
1.99 @@ -1842,34 +1830,30 @@
1.100 case head of
1.101 IConst (name as (s, _), _, T_args) =>
1.102 let
1.103 - val ary = length args
1.104 - fun arg_site j =
1.105 - if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
1.106 + val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1.107 in
1.108 - map2 (fn j => term (arg_site j :: sites)) (0 upto ary - 1) args
1.109 - |> mk_aterm format type_enc name T_args
1.110 + map (term arg_site) args |> mk_aterm format type_enc name T_args
1.111 end
1.112 | IVar (name, _) =>
1.113 - map (term (Elsewhere :: sites)) args
1.114 - |> mk_aterm format type_enc name []
1.115 + map (term Elsewhere) args |> mk_aterm format type_enc name []
1.116 | IAbs ((name, T), tm) =>
1.117 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1.118 - term (Elsewhere :: sites) tm)
1.119 + term Elsewhere tm)
1.120 | IApp _ => raise Fail "impossible \"IApp\""
1.121 val T = ityp_of u
1.122 in
1.123 - if should_tag_with_type ctxt polym_constrs mono type_enc sites u T then
1.124 - tag_with_type ctxt polym_constrs format mono type_enc pos T t
1.125 + if should_tag_with_type ctxt mono type_enc site u T then
1.126 + tag_with_type ctxt format mono type_enc pos T t
1.127 else
1.128 t
1.129 end
1.130 - in term o single o Top_Level end
1.131 + in term o Top_Level end
1.132 and formula_from_iformula ctxt polym_constrs format mono type_enc
1.133 should_guard_var =
1.134 let
1.135 val thy = Proof_Context.theory_of ctxt
1.136 val level = level_of_type_enc type_enc
1.137 - val do_term = ho_term_from_iterm ctxt polym_constrs format mono type_enc
1.138 + val do_term = ho_term_from_iterm ctxt format mono type_enc
1.139 val do_bound_type =
1.140 case type_enc of
1.141 Simple_Types _ => fused_type ctxt mono level 0
1.142 @@ -1885,7 +1869,7 @@
1.143 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1.144 let
1.145 val var = ATerm (name, [])
1.146 - val tagged_var = tag_with_type ctxt [] format mono type_enc pos T var
1.147 + val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1.148 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1.149 else
1.150 NONE
1.151 @@ -2165,8 +2149,7 @@
1.152 ascii_of (mangled_type format type_enc T),
1.153 Axiom,
1.154 eq_formula type_enc (atomic_types_of T) false
1.155 - (tag_with_type ctxt [] format mono type_enc NONE T x_var)
1.156 - x_var,
1.157 + (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
1.158 isabelle_info format simpN, NONE)
1.159 end
1.160
1.161 @@ -2257,7 +2240,7 @@
1.162 val cst = mk_aterm format type_enc (s, s') T_args
1.163 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
1.164 val should_encode = should_encode_type ctxt mono level
1.165 - val tag_with = tag_with_type ctxt [] format mono type_enc NONE
1.166 + val tag_with = tag_with_type ctxt format mono type_enc NONE
1.167 val add_formula_for_res =
1.168 if should_encode res_T then
1.169 let