src/HOL/Tools/SMT/smt_translate.ML
changeset 43385 9cd4b4ecb4dd
parent 43154 72e4753a6677
child 43507 d566714a9ce1
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 14 08:33:51 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 14 13:50:54 2011 +0200
     1.3 @@ -160,7 +160,6 @@
     1.4        Termtab.update (constr, length selects) #>
     1.5        fold (Termtab.update o rpair 1) selects
     1.6      val funcs = fold (fold (fold add o snd)) declss Termtab.empty
     1.7 -
     1.8    in ((funcs, declss', tr_context', ctxt'), ts) end
     1.9      (* FIXME: also return necessary datatype and record theorems *)
    1.10  
    1.11 @@ -344,11 +343,14 @@
    1.12      in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
    1.13  in
    1.14  
    1.15 -fun intro_explicit_application ctxt ts =
    1.16 +fun intro_explicit_application ctxt funcs ts =
    1.17    let
    1.18      val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
    1.19      val arities' = Termtab.map (minimize types) arities
    1.20 -    fun apply' t = apply (the (Termtab.lookup arities' t)) t
    1.21 +
    1.22 +    fun app_func t T ts =
    1.23 +      if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
    1.24 +      else apply (the (Termtab.lookup arities' t)) t T ts
    1.25  
    1.26      fun traverse Ts t =
    1.27        (case Term.strip_comb t of
    1.28 @@ -359,8 +361,8 @@
    1.29        | (u as Const (c as (_, T)), ts) =>
    1.30            (case SMT_Builtin.dest_builtin ctxt c ts of
    1.31              SOME (_, _, us, mk) => mk (map (traverse Ts) us)
    1.32 -          | NONE => apply' u T (map (traverse Ts) ts))
    1.33 -      | (u as Free (_, T), ts) => apply' u T (map (traverse Ts) ts)
    1.34 +          | NONE => app_func u T (map (traverse Ts) ts))
    1.35 +      | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
    1.36        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
    1.37        | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
    1.38        | (u, ts) => traverses Ts u ts)
    1.39 @@ -586,7 +588,7 @@
    1.40        ts2
    1.41        |> eta_expand ctxt1 is_fol funcs
    1.42        |> lift_lambdas ctxt1
    1.43 -      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1)
    1.44 +      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
    1.45  
    1.46      val ((rewrite_rules, extra_thms, builtin), ts4) =
    1.47        (if is_fol then folify ctxt2 else pair ([], [], I)) ts3