corrected treatment of applications of built-in functions to higher-order terms
authorboehmes
Sat Feb 18 23:43:21 2012 +0100 (2012-02-18)
changeset 46529a018d542e0ae
parent 46528 1bbee2041321
child 46530 d5d14046686f
corrected treatment of applications of built-in functions to higher-order terms
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Feb 18 23:05:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sat Feb 18 23:43:21 2012 +0100
     1.3 @@ -228,6 +228,8 @@
     1.4                (case SMT_Builtin.dest_builtin ctxt c ts of
     1.5                  SOME (_, k, us, mk) =>
     1.6                    if k = length us then mk (map expand us)
     1.7 +                  else if k < length us then
     1.8 +                    chop k (map expand us) |>> mk |> Term.list_comb
     1.9                    else expf k (length ts) T (mk (map expand us))
    1.10                | NONE => exp_func u T (map expand ts))
    1.11            | (u as Free (_, T), ts) => exp_func u T (map expand ts)
    1.12 @@ -299,7 +301,11 @@
    1.13            q $ traverse Ts u1 $ traverse Ts u2
    1.14        | (u as Const (c as (_, T)), ts) =>
    1.15            (case SMT_Builtin.dest_builtin ctxt c ts of
    1.16 -            SOME (_, _, us, mk) => mk (map (traverse Ts) us)
    1.17 +            SOME (_, k, us, mk) =>
    1.18 +              let
    1.19 +                val (ts1, ts2) = chop k (map (traverse Ts) us)
    1.20 +                val U = Term.strip_type T |>> snd o chop k |> (op --->)
    1.21 +              in apply 0 (mk ts1) U ts2 end
    1.22            | NONE => app_func u T (map (traverse Ts) ts))
    1.23        | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
    1.24        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)