# HG changeset patch
# User bulwahn
# Date 1249367696 -7200
# Node ID 26a9d0c69b8b1262fd6916ac0564084406fc03e5
# Parent  50f95314063635fde60ad683a2aa8024e7e9dd97
refactoring predicate compiler; added type synonyms and functions split_smode and split_mode

diff -r 50f953140636 -r 26a9d0c69b8b src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 04 08:34:56 2009 +0200
@@ -68,10 +68,10 @@
     -> (string * (term list * indprem list) list) list
     -> (moded_clause list) pred_mode_table  
   (*val compile_preds : theory -> compilation_funs -> string list -> string list
-    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table*)
-  val rpred_create_definitions :(string * typ) list -> int -> string * mode list
+    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table
+  val rpred_create_definitions :(string * typ) list -> string * mode list
     -> theory -> theory 
-  val split_mode : int list -> term list -> (term list * term list)
+  val split_smode : int list -> term list -> (term list * term list) *)
   val print_moded_clauses :
     theory -> (moded_clause list) pred_mode_table -> unit
   val print_compiled_terms : theory -> term pred_mode_table -> unit
@@ -92,6 +92,7 @@
   val all_generator_modes_of : theory -> (string * mode list) list
   val compile_clause : compilation_funs -> term option -> (term list -> term) ->
     theory -> string list -> string list -> mode -> term -> moded_clause -> term
+  val preprocess_intro : theory -> thm -> thm
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
@@ -164,8 +165,8 @@
     Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
   end;
 
-fun dest_randomT (Type ("fun", [@{typ Random.seed}, T])) =
-  fst (HOLogic.dest_prodT (fst (HOLogic.dest_prodT T)))  
+fun dest_randomT (Type ("fun", [@{typ Random.seed},
+  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
 (* destruction of intro rules *)
@@ -177,12 +178,28 @@
   val (params, args) = chop nparams all_args
 in (pred, (params, args)) end
 
-(* data structures *)
+(** data structures **)
 
-type mode = int list option list * int list; (*pmode FIMXE*)
+type smode = int list;
+type mode = smode option list * smode;
 datatype tmode = Mode of mode * int list * tmode option list;
 
-(* short names for nested types *)
+fun split_smode is ts =
+  let
+    fun split_smode' _ _ [] = ([], [])
+      | split_smode' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
+          (split_smode' is (i+1) ts)
+  in split_smode' is 1 ts end
+
+fun split_mode (iss, is) ts =
+  let
+    val (t1, t2) = chop (length iss) ts 
+  in (t1, split_smode is t2) end
+
+fun string_of_mode (iss, is) = space_implode " -> " (map
+  (fn NONE => "X"
+    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
+       (iss @ [SOME is]));
 
 datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
   GeneratorPrem of term list * term | Generator of (string * typ);
@@ -190,16 +207,6 @@
 type moded_clause = term list * (indprem * tmode) list
 type 'a pred_mode_table = (string * (mode * 'a) list) list
 
-
-fun string_of_mode (iss, is) = space_implode " -> " (map
-  (fn NONE => "X"
-    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
-       (iss @ [SOME is]));
-
-fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
-  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-    string_of_mode ms)) modes));
-
 datatype predfun_data = PredfunData of {
   name : string,
   definition : thm,
@@ -260,7 +267,7 @@
   Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
 
 fun the_pred_data thy name = case lookup_pred_data thy name
- of NONE => error ("No such   predicate " ^ quote name)  
+ of NONE => error ("No such predicate " ^ quote name)  
   | SOME data => data;
 
 val is_registered = is_some oo lookup_pred_data 
@@ -326,20 +333,49 @@
 val sizelim_function_name_of = #name ooo the_sizelim_function_data
 
 (*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
-
-   
-(* further functions *)
-
-(* TODO: maybe join chop nparams and split_mode is
-to some function split_mode mode and rename split_mode to split_smode *)
-fun split_mode is ts = let
-  fun split_mode' _ _ [] = ([], [])
-    | split_mode' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
-        (split_mode' is (i+1) ts)
-in split_mode' is 1 ts end
-
+     
 (* diagnostic display functions *)
 
+fun print_modes modes = Output.tracing ("Inferred modes:\n" ^
+  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+    string_of_mode ms)) modes));
+
+fun print_pred_mode_table string_of_entry thy pred_mode_table =
+  let
+    fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
+      ^ (string_of_entry pred mode entry)  
+    fun print_pred (pred, modes) =
+      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
+    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
+  in () end;
+
+fun string_of_moded_prem thy (Prem (ts, p), Mode (_, is, _)) =
+    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
+    "(mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
+  | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (_, is, _)) =
+    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
+    "(generator_mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
+  | string_of_moded_prem thy (Generator (v, T), _) =
+    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
+  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
+    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
+    "(negative mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
+  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
+    (Syntax.string_of_term_global thy t) ^
+    "(sidecond mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"    
+  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
+     
+fun print_moded_clauses thy =
+  let        
+    fun string_of_clause pred mode clauses =
+      cat_lines (map (fn (ts, prems) => (space_implode " --> "
+        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
+        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
+  in print_pred_mode_table string_of_clause thy end;
+
+fun print_compiled_terms thy =
+  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
+    
 fun print_stored_rules thy =
   let
     val preds = (Graph.keys o PredData.get) thy
@@ -370,7 +406,7 @@
   in
     fold print (all_modes_of thy) ()
   end
-
+  
 (** preprocessing rules **)  
 
 fun imp_prems_conv cv ct =
@@ -393,7 +429,8 @@
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
     | replace_eqs t = t
-   fun preprocess_case t = let
+   fun preprocess_case t =
+   let
      val params = Logic.strip_params t
      val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
      val assums_hyp' = assums1 @ (map replace_eqs assums2)
@@ -459,6 +496,7 @@
     |> filter (fn c => is_inductive_predicate thy c orelse is_registered thy c)
 
 (* code dependency graph *)    
+
 fun dependencies_of thy name =
   let
     val (intros, elim, nparams) = fetch_pred_data thy name 
@@ -547,9 +585,8 @@
 fun funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
-    val (paramTs, argTs) = chop (length iss) Ts
+    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
     val paramTs' = map2 (fn SOME is => funT_of compfuns ([], is) | NONE => I) iss paramTs 
-    val (inargTs, outargTs) = split_mode is argTs
   in
     (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
   end;
@@ -557,9 +594,8 @@
 fun sizelim_funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
-    val (paramTs, argTs) = chop (length iss) Ts
+    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
     val paramTs' = map2 (fn SOME is => sizelim_funT_of compfuns ([], is) | NONE => I) iss paramTs 
-    val (inargTs, outargTs) = split_mode is argTs
   in
     (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
   end;  
@@ -702,9 +738,9 @@
 canonical order? *)
 (* maybe remove param_funT_of completely - by using funT_of *)
 fun param_funT_of compfuns T NONE = T
-  | param_funT_of compfuns T (SOME mode) = let
-     val Ts = binder_types T;
-     val (Us1, Us2) = split_mode mode Ts
+  | param_funT_of compfuns T (SOME mode) =
+   let
+     val (Us1, Us2) = split_smode mode (binder_types T)
    in Us1 ---> (mk_predT compfuns (mk_tupleT Us2)) end;
 
 (* Mode analysis *)
@@ -822,53 +858,12 @@
     | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)
     | _ => default
   end
-
-fun print_pred_mode_table string_of_entry thy pred_mode_table =
-  let
-    fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
-      ^ (string_of_entry pred mode entry)  
-    fun print_pred (pred, modes) =
-      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
-    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
-  in () end;
-
-fun string_of_moded_prem thy (Prem (ts, p), Mode (_, is, _)) =
-    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
-    "(mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
-  | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (_, is, _)) =
-    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
-    "(generator_mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
-  | string_of_moded_prem thy (Generator (v, T), _) =
-    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
-  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
-    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
-    "(negative mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
-  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
-    (Syntax.string_of_term_global thy t) ^
-    "(sidecond mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"    
-  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
-   
-  
-fun print_moded_clauses thy =
-  let        
-    fun string_of_clause pred mode clauses =
-      cat_lines (map (fn (ts, prems) => (space_implode " --> "
-        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
-        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
-  in print_pred_mode_table string_of_clause thy end;
-
-fun print_compiled_terms thy =
-  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
-
-fun print_raw_compiled_terms thy =
-  print_pred_mode_table (fn _ => fn _ => (PolyML.makestring : term -> string)) thy
-
   
 fun select_mode_prem thy modes vs ps =
   find_first (is_some o snd) (ps ~~ map
     (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
           let
-            val (in_ts, out_ts) = split_mode is us;
+            val (in_ts, out_ts) = split_smode is us;
             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
             val vTs = maps term_vTs out_ts';
             val dupTs = map snd (duplicates (op =) vTs) @
@@ -938,7 +933,7 @@
         | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
             (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
             (filter_out (equal p) ps))
-    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_mode is ts));
+    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
     val in_vs = terms_vs in_ts;
     val concl_vs = terms_vs ts
   in
@@ -1152,7 +1147,7 @@
           val v = Free (s, fastype_of t)
         in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 
-    val (in_ts, out_ts) = split_mode is ts;
+    val (in_ts, out_ts) = split_smode is ts;
     val (in_ts', (all_vs', eqs)) =
       fold_map check_constrt in_ts (all_vs, []);
 
@@ -1168,7 +1163,6 @@
               (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts)))
            *)
             compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
-              (* (mk_single compfuns (mk_tuple out_ts)) *)
               (final_term out_ts)
           end
       | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) =
@@ -1181,8 +1175,7 @@
             val (compiled_clause, rest) = case p of
                Prem (us, t) =>
                  let
-                   val (in_ts, out_ts''') = split_mode is us;
-                   (* compfuns seems wrong in compile_expr! *)
+                   val (in_ts, out_ts''') = split_smode is us;
                    val args = case size of
                      NONE => in_ts
                    | SOME size_t => in_ts @ [size_t]
@@ -1194,7 +1187,7 @@
                  end
              | Negprem (us, t) =>
                  let
-                   val (in_ts, out_ts''') = split_mode is us
+                   val (in_ts, out_ts''') = split_smode is us
                    val u = lift_pred compfuns
                      (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr NONE thy (mode, t), in_ts)))
                    val rest = compile_prems out_ts''' vs' names'' ps
@@ -1209,7 +1202,7 @@
                  end
              | GeneratorPrem (us, t) =>
                  let
-                   val (in_ts, out_ts''') = split_mode is us;
+                   val (in_ts, out_ts''') = split_smode is us;
                    val args = case size of
                      NONE => in_ts
                    | SOME size_t => in_ts @ [size_t]
@@ -1236,10 +1229,8 @@
 
 fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
   let
-    val Ts = binder_types T;
-    val (Ts1, Ts2) = chop (length param_vs) Ts;
+    val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T)
     val Ts1' = map2 (param_funT_of compfuns) Ts1 (fst mode)
-    val (Us1, Us2) = split_mode (snd mode) Ts2;
     val xnames = Name.variant_list (all_vs @ param_vs)
       (map (fn i => "x" ^ string_of_int i) (snd mode));
     val size_name = Name.variant (all_vs @ param_vs @ xnames) "size"
@@ -1288,30 +1279,29 @@
   val argnames = Name.variant_list names
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   val args = map Free (argnames ~~ Ts)
-  val (inargs, outargs) = split_mode mode args
+  val (inargs, outargs) = split_smode mode args
   val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs)
   val t = fold_rev lambda args r 
 in
   (t, argnames @ names)
 end;
 
-fun create_intro_elim_rule nparams mode defthm mode_id funT pred thy =
+fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy =
 let
   val Ts = binder_types (fastype_of pred)
   val funtrm = Const (mode_id, funT)
   val argnames = Name.variant_list []
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
-  val (Ts1, Ts2) = chop nparams Ts;
-  val Ts1' = map2 (param_funT_of (PredicateCompFuns.compfuns)) Ts1 (fst mode)
+  val (Ts1, Ts2) = chop (length iss) Ts;
+  val Ts1' = map2 (param_funT_of (PredicateCompFuns.compfuns)) Ts1 iss
   val args = map Free (argnames ~~ (Ts1' @ Ts2))
-  val (params, io_args) = chop nparams args
-  val (inargs, outargs) = split_mode (snd mode) io_args
+  val (params, (inargs, outargs)) = split_mode mode args 
   val param_names = Name.variant_list argnames
-    (map (fn i => "p" ^ string_of_int i) (1 upto nparams))
+    (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
   val param_vs = map Free (param_names ~~ Ts1)
-  val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ (fst mode)) []
-  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ io_args))
-  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args))
+  val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ iss) []
+  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ inargs @ outargs))
+  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ inargs @ outargs))
   val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
   val funargs = params @ inargs
   val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
@@ -1322,7 +1312,7 @@
   val _ = tracing (Syntax.string_of_term_global thy introtrm) 
   val simprules = [defthm, @{thm eval_pred},
                    @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
-  val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1)
+  val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
@@ -1335,45 +1325,49 @@
   let
     fun string_of_mode mode = if null mode then "0"
       else space_implode "_" (map string_of_int mode)
-    fun string_of_HOmode m s = case m of NONE => s | SOME mode => s ^ "__" ^ (string_of_mode mode)
+    fun string_of_HOmode m s =
+      case m of NONE => s | SOME mode => s ^ "_and_" ^ (string_of_mode mode)
     val HOmode = fold string_of_HOmode (fst mode) ""
   in
     (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
-      (if HOmode = "" then "_" else HOmode ^ "___") ^ (string_of_mode (snd mode))
+      (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
   end;
   
-fun create_definitions preds nparams (name, modes) thy =
+fun create_definitions preds (name, modes) thy =
   let
     val _ = tracing "create definitions"
     val compfuns = PredicateCompFuns.compfuns
     val T = AList.lookup (op =) preds name |> the
-    fun create_definition mode thy = let
+    fun create_definition (mode as (iss, is)) thy = let
       val mode_cname = create_constname_of_mode thy "" name mode
       val mode_cbasename = Long_Name.base_name mode_cname
       val Ts = binder_types T;
-      val (Ts1, Ts2) = chop nparams Ts;
-      val Ts1' = map2 (param_funT_of compfuns) Ts1 (fst mode)
-      val (Us1, Us2) = split_mode (snd mode) Ts2;
+      val (Ts1, (Us1, Us2)) = split_mode mode Ts;
+      val Ts1' = map2 (param_funT_of compfuns) Ts1 iss
       val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2))
       val names = Name.variant_list []
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
-      val xs = map Free (names ~~ (Ts1' @ Ts2));
-      val (xparams, xargs) = chop nparams xs;
-      val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ (fst mode)) names
-      val (xins, xouts) = split_mode (snd mode) xargs;
+      val xs = map Free (names ~~ (Ts1' @ Us1 @ Us2));
+      val (xparams, (xins, xouts)) = split_mode mode xs;
+      val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
       fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
-       | mk_split_lambda [x] t = lambda x t
-       | mk_split_lambda xs t = let
-         fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
-           | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
-         in mk_split_lambda' xs t end;
-      val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
+        | mk_split_lambda [x] t = lambda x t
+        | mk_split_lambda xs t =
+        let
+          fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+            | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+        in
+          mk_split_lambda' xs t
+        end;
+      val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
+        (list_comb (Const (name, T), xparams' @ xins @ xouts)))
       val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
       val def = Logic.mk_equals (lhs, predterm)
       val ([definition], thy') = thy |>
         Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
         PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
-      val (intro, elim) = create_intro_elim_rule nparams mode definition mode_cname funT (Const (name, T)) thy'
+      val (intro, elim) =
+        create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
       in thy' |> add_predfun name mode (mode_cname, definition, intro, elim)
         |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
         |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
@@ -1383,17 +1377,14 @@
     fold create_definition modes thy
   end;
 
-fun sizelim_create_definitions preds nparams (name, modes) thy =
+fun sizelim_create_definitions preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
         val mode_cname = create_constname_of_mode thy "sizelim_" name mode
-        val Ts = binder_types T;
-        (* termify code: val Ts = map termifyT Ts *)
-        val (Ts1, Ts2) = chop nparams Ts;
+        val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T)
         val Ts1' = map2 (param_funT_of PredicateCompFuns.compfuns) Ts1 (fst mode)
-        val (Us1, Us2) = split_mode (snd mode) Ts2;
         val funT = (Ts1' @ Us1 @ [@{typ "code_numeral"}]) ---> (PredicateCompFuns.mk_predT (mk_tupleT Us2)) 
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
@@ -1402,20 +1393,15 @@
   in
     fold create_definition modes thy
   end;
-  
-  
-(* MAYBE use own theory datastructure for rpred *)
-fun rpred_create_definitions preds nparams (name, modes) thy =
+    
+fun rpred_create_definitions preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
         val mode_cname = create_constname_of_mode thy "gen_" name mode
-        val Ts = binder_types T;
-        (* termify code: val Ts = map termifyT Ts *)
-        val (Ts1, Ts2) = chop nparams Ts;
+        val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T);
         val Ts1' = map2 (param_funT_of RPredCompFuns.compfuns) Ts1 (fst mode)
-        val (Us1, Us2) = split_mode (snd mode) Ts2;
         val funT = (Ts1' @ Us1 @ [@{typ "code_numeral"}]) ---> (RPredCompFuns.mk_rpredT (mk_tupleT Us2)) 
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
@@ -1548,7 +1534,7 @@
 
 fun prove_clause thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) =
   let
-    val (in_ts, clause_out_ts) = split_mode is ts;
+    val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems out_ts [] =
       (prove_match thy out_ts)
       THEN asm_simp_tac HOL_basic_ss' 1
@@ -1558,7 +1544,7 @@
         val premposition = (find_index (equal p) clauses) + nargs
         val rest_tac = (case p of Prem (us, t) =>
             let
-              val (_, out_ts''') = split_mode is us
+              val (_, out_ts''') = split_smode is us
               val rec_tac = prove_prems out_ts''' ps
             in
               print_tac "before clause:"
@@ -1570,7 +1556,7 @@
             end
           | Negprem (us, t) =>
             let
-              val (_, out_ts''') = split_mode is us
+              val (_, out_ts''') = split_smode is us
               val rec_tac = prove_prems out_ts''' ps
               val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
               val (_, params) = strip_comb t
@@ -1714,7 +1700,7 @@
       |> preprocess_intro thy
       |> (fn thm => hd (ind_set_codegen_preproc thy [thm]))
       (* FIXME preprocess |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]) *)
-    val (in_ts, clause_out_ts) = split_mode is ts;
+    val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems2 out_ts [] =
       print_tac "before prove_match2 - last call:"
       THEN prove_match2 thy out_ts
@@ -1736,14 +1722,14 @@
         val rest_tac = (case p of
           Prem (us, t) =>
           let
-            val (_, out_ts''') = split_mode is us
+            val (_, out_ts''') = split_smode is us
             val rec_tac = prove_prems2 out_ts''' ps
           in
             (prove_expr2 thy (mode, t)) THEN rec_tac
           end
         | Negprem (us, t) =>
           let
-            val (_, out_ts''') = split_mode is us
+            val (_, out_ts''') = split_smode is us
             val rec_tac = prove_prems2 out_ts''' ps
             val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
             val (_, params) = strip_comb t
@@ -1882,7 +1868,7 @@
     val (clauses, arities) = fold add_clause intrs ([], []);
   in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
 
-(** main function **)
+(** main function of predicate compiler **)
 
 fun add_equations_of steps prednames thy =
 let
@@ -1893,7 +1879,7 @@
   val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses 
   val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
   val _ = Output.tracing "Defining executable functions..."
-  val thy' = fold (#create_definitions steps preds nparams) modes thy
+  val thy' = fold (#create_definitions steps preds) modes thy
     |> Theory.checkpoint
   val _ = Output.tracing "Compiling equations..."
   val compiled_terms =
@@ -1915,6 +1901,47 @@
   thy''
 end
 
+fun gen_add_equations steps names thy =
+  let
+    val thy' = PredData.map (fold (Graph.extend (dependencies_of thy)) names) thy |> Theory.checkpoint;
+    fun strong_conn_of gr keys =
+      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
+    val scc = strong_conn_of (PredData.get thy') names
+    val thy'' = fold_rev
+      (fn preds => fn thy =>
+        if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy)
+      scc thy' |> Theory.checkpoint
+  in thy'' end
+
+(* different instantiantions of the predicate compiler *)
+
+val add_equations = gen_add_equations
+  {infer_modes = infer_modes false,
+  create_definitions = create_definitions,
+  compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
+  prove = prove,
+  are_not_defined = (fn thy => forall (null o modes_of thy)),
+  qname = "equation"}
+
+val add_sizelim_equations = gen_add_equations
+  {infer_modes = infer_modes false,
+  create_definitions = sizelim_create_definitions,
+  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
+  prove = prove_by_skip,
+  are_not_defined = (fn thy => fn preds => true), (* TODO *)
+  qname = "sizelim_equation"
+  }
+  
+val add_quickcheck_equations = gen_add_equations
+  {infer_modes = infer_modes_with_generator,
+  create_definitions = rpred_create_definitions,
+  compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true,
+  prove = prove_by_skip,
+  are_not_defined = (fn thy => fn preds => true), (* TODO *)
+  qname = "rpred_equation"}
+
+(** user interface **)
+
 (* generation of case rules from user-given introduction rules *)
 
 fun mk_casesrule ctxt nparams introrules =
@@ -1940,50 +1967,12 @@
     val cases = map mk_case intros
   in Logic.list_implies (assm :: cases, prop) end;
 
-fun gen_add_equations steps names thy =
-  let
-    val thy' = PredData.map (fold (Graph.extend (dependencies_of thy)) names) thy |> Theory.checkpoint;
-    fun strong_conn_of gr keys =
-      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
-    val scc = strong_conn_of (PredData.get thy') names
-    val thy'' = fold_rev
-      (fn preds => fn thy =>
-        if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy)
-      scc thy' |> Theory.checkpoint
-  in thy'' end
-
+(* code_pred_intro attribute *)
 
-val add_equations = gen_add_equations
-  {infer_modes = infer_modes false,
-  create_definitions = create_definitions,
-  compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
-  prove = prove,
-  are_not_defined = (fn thy => forall (null o modes_of thy)),
-  qname = "equation"}
-
-val add_sizelim_equations = gen_add_equations
-  {infer_modes = infer_modes false,
-  create_definitions = sizelim_create_definitions,
-  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
-  prove = prove_by_skip,
-  are_not_defined = (fn thy => fn preds => true), (* TODO *)
-  qname = "sizelim_equation"
-  }
-  
-val add_quickcheck_equations = gen_add_equations
-  {infer_modes = infer_modes_with_generator,
-  create_definitions = rpred_create_definitions,
-  compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true,
-  prove = prove_by_skip,
-  are_not_defined = (fn thy => fn preds => true), (* TODO *)
-  qname = "rpred_equation"}
-    
 fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
 
 val code_pred_intros_attrib = attrib add_intro;
 
-(** user interface **)
-
 local
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
@@ -2061,7 +2050,7 @@
     val user_mode = map_filter I (map_index
       (fn (i, t) => case t of Bound j => if j < length Ts then NONE
         else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
-    val (inargs, _) = split_mode user_mode args;
+    val (inargs, _) = split_smode user_mode args;
     val modes = filter (fn Mode (_, is, _) => is = user_mode)
       (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes