--- a/src/HOL/IsaMakefile Tue Mar 30 15:46:50 2010 -0700
+++ b/src/HOL/IsaMakefile Wed Mar 31 16:44:41 2010 +0200
@@ -297,6 +297,7 @@
Tools/numeral_syntax.ML \
Tools/polyhash.ML \
Tools/Predicate_Compile/predicate_compile_aux.ML \
+ Tools/Predicate_Compile/predicate_compile_compilations.ML \
Tools/Predicate_Compile/predicate_compile_core.ML \
Tools/Predicate_Compile/predicate_compile_data.ML \
Tools/Predicate_Compile/predicate_compile_fun.ML \
--- a/src/HOL/Predicate_Compile.thy Tue Mar 30 15:46:50 2010 -0700
+++ b/src/HOL/Predicate_Compile.thy Wed Mar 31 16:44:41 2010 +0200
@@ -8,6 +8,7 @@
imports New_Random_Sequence
uses
"Tools/Predicate_Compile/predicate_compile_aux.ML"
+ "Tools/Predicate_Compile/predicate_compile_compilations.ML"
"Tools/Predicate_Compile/predicate_compile_core.ML"
"Tools/Predicate_Compile/predicate_compile_data.ML"
"Tools/Predicate_Compile/predicate_compile_fun.ML"
--- 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,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Wed Mar 31 16:44:41 2010 +0200
@@ -0,0 +1,293 @@
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Structures for different compilations of the predicate compiler
+*)
+
+structure PredicateCompFuns =
+struct
+
+fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
+
+fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
+ | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
+
+fun mk_single t =
+ let val T = fastype_of t
+ in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+ let val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name sup};
+
+fun mk_if cond = Const (@{const_name Predicate.if_pred},
+ HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+ let
+ val T = mk_predT HOLogic.unitT
+ in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+
+fun mk_Enum f =
+ let val T as Type ("fun", [T', _]) = fastype_of f
+ in
+ Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f
+ end;
+
+fun mk_Eval (f, x) =
+ let
+ val T = fastype_of x
+ in
+ Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
+ end;
+
+fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+ (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+ mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
+ mk_map = mk_map};
+
+end;
+
+structure RandomPredCompFuns =
+struct
+
+fun mk_randompredT T =
+ @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
+
+fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
+ [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
+ | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
+
+fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in
+ Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
+ end;
+
+fun mk_bind (x, f) =
+ let
+ val T as (Type ("fun", [_, U])) = fastype_of f
+ in
+ Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
+ end
+
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
+
+fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
+ HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+ let
+ val T = mk_randompredT HOLogic.unitT
+ in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
+ (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+structure DSequence_CompFuns =
+struct
+
+fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
+
+fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
+ | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
+
+fun mk_single t =
+ let val T = fastype_of t
+ in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
+
+fun mk_if cond = Const (@{const_name DSequence.if_seq},
+ HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t = let val T = mk_dseqT HOLogic.unitT
+ in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
+ (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure New_Pos_Random_Sequence_CompFuns =
+struct
+
+fun mk_pos_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+
+fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+ | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
+ HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+ let
+ val pT = mk_pos_random_dseqT HOLogic.unitT
+ val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+ [Type (@{type_name Option.option}, [@{typ unit}])])
+
+ in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
+ (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure New_Neg_Random_Sequence_CompFuns =
+struct
+
+fun mk_neg_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} -->
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+
+fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+ Type (@{type_name Lazy_Sequence.lazy_sequence},
+ [Type (@{type_name Option.option}, [T])])])])])])) = T
+ | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
+ HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+ let
+ val nT = mk_neg_random_dseqT HOLogic.unitT
+ val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
+ in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
+ (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure Random_Sequence_CompFuns =
+struct
+
+fun mk_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
+
+fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed},
+ Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
+ | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
+
+fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
+ HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+ let
+ val T = mk_random_dseqT HOLogic.unitT
+ in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
+ (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map}
+
+end;
+
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 30 15:46:50 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Mar 31 16:44:41 2010 +0200
@@ -66,9 +66,6 @@
val code_pred_intro_attrib : attribute
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
- val pred_compfuns : compilation_funs
- val randompred_compfuns : compilation_funs
- val new_randompred_compfuns : compilation_funs
val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
val add_depth_limited_random_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
@@ -724,30 +721,6 @@
PredData.map (Graph.map_node name (map_pred_data set))
end
-(* 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
-};
-
-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
-
(* registration of alternative function names *)
structure Alt_Compilations_Data = Theory_Data
@@ -796,306 +769,8 @@
(map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
fun_names)
-(* structures for different compilations *)
-
-structure PredicateCompFuns =
-struct
-
-fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
-
-fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
- | dest_predT T = raise TYPE ("dest_predT", [T], []);
-
-fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
-
-fun mk_single t =
- let val T = fastype_of t
- in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
-
-fun mk_bind (x, f) =
- let val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name sup};
-
-fun mk_if cond = Const (@{const_name Predicate.if_pred},
- HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
-
-fun mk_not t =
- let
- val T = mk_predT HOLogic.unitT
- in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
-
-fun mk_Enum f =
- let val T as Type ("fun", [T', _]) = fastype_of f
- in
- Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f
- end;
-
-fun mk_Eval (f, x) =
- let
- val T = fastype_of x
- in
- Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
- end;
-
-fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
- (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
-
-val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
- mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- mk_map = mk_map};
-
-end;
-
-structure RandomPredCompFuns =
-struct
-
-fun mk_randompredT T =
- @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
-
-fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
- [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
- | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
-
-fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
-
-fun mk_single t =
- let
- val T = fastype_of t
- in
- Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
- end;
-
-fun mk_bind (x, f) =
- let
- val T as (Type ("fun", [_, U])) = fastype_of f
- in
- Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
- end
-
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
-
-fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
- HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
-
-fun mk_not t =
- let
- val T = mk_randompredT HOLogic.unitT
- in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
- (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map};
-
-end;
-
-structure DSequence_CompFuns =
-struct
-
-fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
-
-fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
- | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
-
-fun mk_single t =
- let val T = fastype_of t
- in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
- let val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
-
-fun mk_if cond = Const (@{const_name DSequence.if_seq},
- HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
-
-fun mk_not t = let val T = mk_dseqT HOLogic.unitT
- in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
- (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-structure New_Pos_Random_Sequence_CompFuns =
-struct
-
-fun mk_pos_random_dseqT T =
- @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
-
-fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
- Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
- Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
- | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
-
-fun mk_single t =
- let
- val T = fastype_of t
- in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
- let
- val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
-
-fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
- HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
-
-fun mk_not t =
- let
- val pT = mk_pos_random_dseqT HOLogic.unitT
- val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
- [Type (@{type_name Option.option}, [@{typ unit}])])
-
- in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
- (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-structure New_Neg_Random_Sequence_CompFuns =
-struct
-
-fun mk_neg_random_dseqT T =
- @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- @{typ code_numeral} -->
- Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
-
-fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
- Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
- Type (@{type_name Lazy_Sequence.lazy_sequence},
- [Type (@{type_name Option.option}, [T])])])])])])) = T
- | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
-
-fun mk_single t =
- let
- val T = fastype_of t
- in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
- let
- val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
- HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
-
-fun mk_not t =
- let
- val nT = mk_neg_random_dseqT HOLogic.unitT
- val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
- in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
- (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-structure Random_Sequence_CompFuns =
-struct
-
-fun mk_random_dseqT T =
- @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
-
-fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
- Type ("fun", [@{typ Random.seed},
- Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
- | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
-
-fun mk_single t =
- let
- val T = fastype_of t
- in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
- let
- val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
-
-fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
- HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
-
-fun mk_not t =
- let
- val T = mk_random_dseqT HOLogic.unitT
- in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
- (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-(* for external use with interactive mode *)
-val pred_compfuns = PredicateCompFuns.compfuns
-val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
-val new_randompred_compfuns = New_Pos_Random_Sequence_CompFuns.compfuns
-
(* compilation modifiers *)
-(* 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;
-
structure Comp_Mod =
struct
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Mar 30 15:46:50 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Mar 31 16:44:41 2010 +0200
@@ -142,19 +142,17 @@
(set_function_flattening (!function_flattening)
(if !debug then debug_options else options))
-fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
-val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
-val mk_return' = #mk_single (dest_compfuns Predicate_Compile_Core.pred_compfuns)
-val mk_bind' = #mk_bind (dest_compfuns Predicate_Compile_Core.pred_compfuns)
+val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
+val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
+val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
-val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
-val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
-val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
+val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
+val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
+val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
-val mk_new_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
-val mk_new_return = #mk_single (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
-val mk_new_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
-
+val mk_new_randompredT = Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.compfuns
+val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
+val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
| mk_split_lambda [x] t = lambda x t