# HG changeset patch # User bulwahn # Date 1270046681 -7200 # Node ID c3946372f5563d0e4187ee2629ce062857e6d5da # Parent b846881928ea8d3eb894fefefe0d5d0b40ca057f putting compilation setup of predicate compiler in a separate file diff -r b846881928ea -r c3946372f556 src/HOL/IsaMakefile --- 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 \ diff -r b846881928ea -r c3946372f556 src/HOL/Predicate_Compile.thy --- 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" diff -r b846881928ea -r c3946372f556 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.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, diff -r b846881928ea -r c3946372f556 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- /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; + diff -r b846881928ea -r c3946372f556 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r b846881928ea -r c3946372f556 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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