# HG changeset patch
# User boehmes
# Date 1308052254 -7200
# Node ID 9cd4b4ecb4dd2d72ffc4cfa991a5101ce6b9fb9f
# Parent  809de915155ff9d61c4eac2e57670ca965c20e5f
slightly more general treatment of mutually recursive datatypes;
treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)

diff -r 809de915155f -r 9cd4b4ecb4dd src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Tue Jun 14 08:33:51 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Tue Jun 14 13:50:54 2011 +0200
@@ -32,12 +32,11 @@
     val vars = the (get_first get_vars descr) ~~ Ts
     val lookup_var = the o AList.lookup (op =) vars
 
-    val dTs = map (apsnd (fn (m, vs, _) => Type (m, map lookup_var vs))) descr
-    val lookup_typ = the o AList.lookup (op =) dTs
-
     fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
-      | typ_of (Datatype.DtType (n, dts)) = Type (n, map typ_of dts)
-      | typ_of (Datatype.DtRec i) = lookup_typ i
+      | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
+      | typ_of (Datatype.DtRec i) =
+          the (AList.lookup (op =) descr i)
+          |> (fn (m, dts, _) => Type (m, map typ_of dts))
 
     fun mk_constr T (m, dts) ctxt =
       let
@@ -48,7 +47,7 @@
 
     fun mk_decl (i, (_, _, constrs)) ctxt =
       let
-        val T = lookup_typ i
+        val T = typ_of (Datatype.DtRec i)
         val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
       in ((T, css), ctxt') end
 
@@ -87,6 +86,7 @@
 (* collection of declarations *)
 
 fun declared declss T = exists (exists (equal T o fst)) declss
+fun declared' dss T = exists (exists (equal T o fst) o snd) dss
 
 fun get_decls T n Ts ctxt =
   let val thy = Proof_Context.theory_of ctxt
@@ -104,13 +104,15 @@
 
 fun add_decls T (declss, ctxt) =
   let
+    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
+
     fun add (TFree _) = I
       | add (TVar _) = I
       | add (T as Type (@{type_name fun}, _)) =
           fold add (Term.body_type T :: Term.binder_types T)
       | add @{typ bool} = I
       | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
-          if declared declss T orelse declared dss T then (dss, ctxt1)
+          if declared declss T orelse declared' dss T then (dss, ctxt1)
           else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
           else
             (case get_decls T n Ts ctxt1 of
@@ -120,7 +122,13 @@
                   val constrTs =
                     maps (map (snd o Term.dest_Const o fst) o snd) ds
                   val Us = fold (union (op =) o Term.binder_types) constrTs []
-            in fold add Us (ds :: dss, ctxt2) end))
-  in add T ([], ctxt) |>> append declss end
+
+                  fun ins [] = [(Us, ds)]
+                    | ins ((Uds as (Us', _)) :: Udss) =
+                        if depends Us' ds then (Us, ds) :: Uds :: Udss
+                        else Uds :: ins Udss
+            in fold add Us (ins dss, ctxt2) end))
+  in add T ([], ctxt) |>> append declss o map snd end
+
 
 end
diff -r 809de915155f -r 9cd4b4ecb4dd src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 14 08:33:51 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 14 13:50:54 2011 +0200
@@ -160,7 +160,6 @@
       Termtab.update (constr, length selects) #>
       fold (Termtab.update o rpair 1) selects
     val funcs = fold (fold (fold add o snd)) declss Termtab.empty
-
   in ((funcs, declss', tr_context', ctxt'), ts) end
     (* FIXME: also return necessary datatype and record theorems *)
 
@@ -344,11 +343,14 @@
     in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
 in
 
-fun intro_explicit_application ctxt ts =
+fun intro_explicit_application ctxt funcs ts =
   let
     val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
     val arities' = Termtab.map (minimize types) arities
-    fun apply' t = apply (the (Termtab.lookup arities' t)) t
+
+    fun app_func t T ts =
+      if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
+      else apply (the (Termtab.lookup arities' t)) t T ts
 
     fun traverse Ts t =
       (case Term.strip_comb t of
@@ -359,8 +361,8 @@
       | (u as Const (c as (_, T)), ts) =>
           (case SMT_Builtin.dest_builtin ctxt c ts of
             SOME (_, _, us, mk) => mk (map (traverse Ts) us)
-          | NONE => apply' u T (map (traverse Ts) ts))
-      | (u as Free (_, T), ts) => apply' u T (map (traverse Ts) ts)
+          | NONE => app_func u T (map (traverse Ts) ts))
+      | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
       | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
       | (u, ts) => traverses Ts u ts)
@@ -586,7 +588,7 @@
       ts2
       |> eta_expand ctxt1 is_fol funcs
       |> lift_lambdas ctxt1
-      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1)
+      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
 
     val ((rewrite_rules, extra_thms, builtin), ts4) =
       (if is_fol then folify ctxt2 else pair ([], [], I)) ts3