# HG changeset patch
# User bulwahn
# Date 1284134005 -7200
# Node ID e98a061455300864751b620e0095d4919d0a3b4a
# Parent  7c69964c6d741e235f1dde20008fc36cf9d598aa
directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory

diff -r 7c69964c6d74 -r e98a06145530 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 10 15:48:43 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 10 17:53:25 2010 +0200
@@ -27,6 +27,8 @@
   val ho_arg_modes_of : mode -> mode list
   val ho_argsT_of : mode -> typ list -> typ list
   val ho_args_of : mode -> term list -> term list
+  val ho_args_of_typ : typ -> term list -> term list
+  val ho_argsT_of_typ : typ list -> typ list
   val split_map_mode : (mode -> term -> term option * term option)
     -> mode -> term list -> term list * term list
   val split_map_modeT : (mode -> typ -> typ option * typ option)
@@ -262,6 +264,31 @@
     flat (map2_optional ho_arg (strip_fun_mode mode) ts)
   end
 
+fun ho_args_of_typ T ts =
+  let
+    fun ho_arg (Type("fun", [_,_])) (SOME t) = [t]
+      | ho_arg (Type("fun", [_,_])) NONE = raise Fail "mode and term do not match"
+      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2]))
+         (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
+          ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2)
+      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) NONE =
+          ho_arg T1 NONE @ ho_arg T2 NONE
+      | ho_arg _ _ = []
+  in
+    flat (map2_optional ho_arg (binder_types T) ts)
+  end
+
+fun ho_argsT_of_typ Ts =
+  let
+    fun ho_arg (T as Type("fun", [_,_])) = [T]
+      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) =
+          ho_arg T1 @ ho_arg T2
+      | ho_arg _ = []
+  in
+    maps ho_arg Ts
+  end
+  
+
 (* temporary function should be replaced by unsplit_input or so? *)
 fun replace_ho_args mode hoargs ts =
   let
diff -r 7c69964c6d74 -r e98a06145530 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 15:48:43 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 17:53:25 2010 +0200
@@ -446,8 +446,7 @@
   let
     val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
     val T = fastype_of outp_pred
-    (* TODO: put in a function for this next line! *)
-    val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T)
+    val paramTs = ho_argsT_of_typ (binder_types T)
     val (param_names, ctxt'') = Variable.variant_fixes
       (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
     val params = map2 (curry Free) param_names paramTs
@@ -460,7 +459,7 @@
       val thy = ProofContext.theory_of ctxt'
       val (pred, args) = strip_intro_concl th'
       val T = fastype_of pred
-      val ho_args = ho_args_of (hd (all_modes_of_typ T)) args
+      val ho_args = ho_args_of_typ T args
       fun subst_of (pred', pred) =
         let
           val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
@@ -474,7 +473,7 @@
       fun instantiate_ho_args th =
         let
           val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
-          val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args')
+          val ho_args' = map dest_Var (ho_args_of_typ T args')
         in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
       val outp_pred =
         Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
@@ -2710,7 +2709,7 @@
           let
             val T = snd (hd preds)
             val paramTs =
-              ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T)
+              ho_argsT_of_typ (binder_types T)
             val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
               (1 upto length paramTs))
           in
@@ -3067,7 +3066,7 @@
     val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
     fun mk_cases const =
       let
-        val T = Sign.the_const_type thy const
+        val T = Sign.the_const_type thy' const
         val pred = Const (const, T)
         val intros = intros_of ctxt' const
       in mk_casesrule lthy' pred intros end