# HG changeset patch
# User bulwahn
# Date 1242394174 -7200
# Node ID f4c61cbea49d107be94cfba15db0279c2403a885
# Parent  657386d94f14efd61203cf6fde21071e07aa8830
added predicate transformation function for code generation

diff -r 657386d94f14 -r f4c61cbea49d src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon May 11 09:39:53 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Fri May 15 15:29:34 2009 +0200
@@ -20,6 +20,7 @@
   val do_proofs: bool ref
   val pred_intros : theory -> string -> thm list
   val get_nparams : theory -> string -> int
+  val pred_term_of : theory -> term -> term option
 end;
 
 structure Predicate_Compile: PREDICATE_COMPILE =
@@ -1395,7 +1396,30 @@
   val code_pred = generic_code_pred (K I);
   val code_pred_cmd = generic_code_pred Code_Unit.read_const
 
+(* transformation for code generation *)
+
+fun pred_term_of thy t = let
+   val (vars, body) = strip_abs t
+   val (pred, all_args) = strip_comb body
+   val (name, T) = dest_Const pred 
+   val (params, args) = chop (get_nparams thy name) all_args
+   val user_mode = flat (map_index
+      (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1])
+        args)
+  val (inargs, _) = get_args user_mode args
+  val all_modes = Symtab.dest (#modes (IndCodegenData.get thy))
+  val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of all_modes (list_comb (pred, params)))
+  fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs)
+  in
+    case modes of
+      []  => (let val _ = error "No mode possible for this term" in NONE end)
+    | [m] => SOME (compile m)
+    | ms  => (let val _ = warning "Multiple modes possible for this term"
+        in SOME (compile (hd ms)) end)
+  end;
+
 end;
 
 fun pred_compile name thy = Predicate_Compile.create_def_equation
   (Sign.intern_const thy name) thy;
+