--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Mar 30 15:46:50 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Mar 31 16:44:41 2010 +0200
@@ -469,10 +469,41 @@
val random_compilations = [Random, Depth_Limited_Random,
Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
-(* Different options for compiler *)
+(* datastructures and setup for generic compilation *)
+
+datatype compilation_funs = CompilationFuns of {
+ mk_predT : typ -> typ,
+ dest_predT : typ -> typ,
+ mk_bot : typ -> term,
+ mk_single : term -> term,
+ mk_bind : term * term -> term,
+ mk_sup : term * term -> term,
+ mk_if : term -> term,
+ mk_not : term -> term,
+ mk_map : typ -> typ -> term -> term -> term
+};
-(*datatype compilation_options =
- Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)
+fun mk_predT (CompilationFuns funs) = #mk_predT funs
+fun dest_predT (CompilationFuns funs) = #dest_predT funs
+fun mk_bot (CompilationFuns funs) = #mk_bot funs
+fun mk_single (CompilationFuns funs) = #mk_single funs
+fun mk_bind (CompilationFuns funs) = #mk_bind funs
+fun mk_sup (CompilationFuns funs) = #mk_sup funs
+fun mk_if (CompilationFuns funs) = #mk_if funs
+fun mk_not (CompilationFuns funs) = #mk_not funs
+fun mk_map (CompilationFuns funs) = #mk_map funs
+
+(** function types and names of different compilations **)
+
+fun funT_of compfuns mode T =
+ let
+ val Ts = binder_types T
+ val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
+ in
+ inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
+ end;
+
+(* Different options for compiler *)
datatype options = Options of {
expected_modes : (string * mode list) option,