# HG changeset patch # User bulwahn # Date 1269876636 -7200 # Node ID 096ec83348f36bce0bda52c9ca751c2668dc4f19 # Parent 7516568bebeb4260b8c35796a4273a3fb9f60767 added new compilation to predicate_compiler diff -r 7516568bebeb -r 096ec83348f3 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:34 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 29 17:30:36 2010 +0200 @@ -465,14 +465,17 @@ (* Different options for compiler *) datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated - | Pos_Random_DSeq | Neg_Random_DSeq + | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq + | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq + | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq | negative_compilation_of c = c fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq + | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq | compilation_for_polarity _ c = c fun string_of_compilation c = @@ -485,6 +488,16 @@ | Annotated => "annotated" | Pos_Random_DSeq => "pos_random dseq" | Neg_Random_DSeq => "neg_random_dseq" + | New_Pos_Random_DSeq => "new_pos_random dseq" + | New_Neg_Random_DSeq => "new_neg_random_dseq" + +val compilation_names = [("pred", Pred), + ("random", Random), + ("depth_limited", Depth_Limited), + ("depth_limited_random", Depth_Limited_Random), + (*("annotated", Annotated),*) + ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq), + ("new_random_dseq", New_Pos_Random_DSeq)] (*datatype compilation_options = Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*) @@ -557,13 +570,6 @@ "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening", "no_topmost_reordering"] -val compilation_names = [("pred", Pred), - ("random", Random), - ("depth_limited", Depth_Limited), - ("depth_limited_random", Depth_Limited_Random), - (*("annotated", Annotated),*) - ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)] - fun print_step options s = if show_steps options then tracing s else () diff -r 7516568bebeb -r 096ec83348f3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:34 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:36 2010 +0200 @@ -873,6 +873,105 @@ 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 Option.option}, + [Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{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 Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [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 Option.option}, + [Type (@{type_name Lazy_Sequence.lazy_sequence}, [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 @@ -1638,6 +1737,7 @@ end | Negprem t => let + val u = mk_not compfuns (compile_expr compilation_modifiers compfuns ctxt (not pol) (t, deriv) additional_arguments') @@ -1686,7 +1786,7 @@ val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod) (fn T => fn (param_vs, names) => - if is_param_type T then + if is_param_type T then (Free (hd param_vs, T), (tl param_vs, names)) else let @@ -2809,6 +2909,42 @@ transform_additional_arguments = K I : (indprem -> term list -> term list) } + +val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = New_Pos_Random_DSeq, + function_name_prefix = "new_random_dseq_", + compfuns = New_Pos_Random_Sequence_CompFuns.compfuns, + mk_random = (fn T => fn additional_arguments => + let + val random = Const ("Quickcheck.random_class.random", + @{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) + in + Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> + New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random + end), + modify_funT = I, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + +val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers + { + compilation = New_Neg_Random_DSeq, + function_name_prefix = "new_random_dseq_neg_", + compfuns = New_Neg_Random_Sequence_CompFuns.compfuns, + mk_random = (fn _ => error "no random generation"), + modify_funT = I, + additional_arguments = K [], + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) + } + val add_depth_limited_equations = gen_add_equations (Steps { define_functions = @@ -2887,6 +3023,23 @@ use_random = true, qname = "random_dseq_equation"}) +val add_new_random_dseq_equations = gen_add_equations + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + let + val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes + val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes + in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.compfuns + options preds (s, pos_modes) + #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.compfuns + options preds (s, neg_modes) + end, + prove = prove_by_skip, + add_code_equations = K (K I), + comp_modifiers = new_pos_random_dseq_comp_modifiers, + use_random = true, + qname = "new_random_dseq_equation"}) (** user interface **) @@ -2942,6 +3095,7 @@ | Depth_Limited => add_depth_limited_equations | Random => add_random_equations | Depth_Limited_Random => add_depth_limited_random_equations + | New_Pos_Random_DSeq => add_new_random_dseq_equations | compilation => error ("Compilation not supported") ) options [const])) end