adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
authorbulwahn
Thu Oct 21 19:13:07 2010 +0200 (2010-10-21)
changeset 4004975d9f57123d6
parent 40048 f3a46d524101
child 40050 638ce4dabe53
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/New_DSequence.thy	Thu Oct 21 19:13:06 2010 +0200
     1.2 +++ b/src/HOL/New_DSequence.thy	Thu Oct 21 19:13:07 2010 +0200
     1.3 @@ -21,7 +21,11 @@
     1.4  
     1.5  definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
     1.6  where
     1.7 -  "pos_bind x f = (%i. 
     1.8 +  "pos_bind x f = (%i. Lazy_Sequence.bind (x i) (%a. f a i))"
     1.9 +
    1.10 +definition pos_decr_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
    1.11 +where
    1.12 +  "pos_decr_bind x f = (%i. 
    1.13       if i = 0 then
    1.14         Lazy_Sequence.empty
    1.15       else
    1.16 @@ -57,7 +61,11 @@
    1.17  
    1.18  definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
    1.19  where
    1.20 -  "neg_bind x f = (%i. 
    1.21 +  "neg_bind x f = (%i. hb_bind (x i) (%a. f a i))"
    1.22 +
    1.23 +definition neg_decr_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
    1.24 +where
    1.25 +  "neg_decr_bind x f = (%i. 
    1.26       if i = 0 then
    1.27         Lazy_Sequence.hit_bound
    1.28       else
    1.29 @@ -94,8 +102,8 @@
    1.30  hide_type (open) pos_dseq neg_dseq
    1.31  
    1.32  hide_const (open)
    1.33 -  pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
    1.34 -  neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
    1.35 +  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
    1.36 +  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
    1.37  hide_fact (open)
    1.38    pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
    1.39    neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
     2.1 --- a/src/HOL/New_Random_Sequence.thy	Thu Oct 21 19:13:06 2010 +0200
     2.2 +++ b/src/HOL/New_Random_Sequence.thy	Thu Oct 21 19:13:07 2010 +0200
     2.3 @@ -20,6 +20,10 @@
     2.4  where
     2.5    "pos_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
     2.6  
     2.7 +definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
     2.8 +where
     2.9 +  "pos_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    2.10 +
    2.11  definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
    2.12  where
    2.13    "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
    2.14 @@ -62,6 +66,10 @@
    2.15  where
    2.16    "neg_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    2.17  
    2.18 +definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
    2.19 +where
    2.20 +  "neg_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    2.21 +
    2.22  definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
    2.23  where
    2.24    "neg_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
    2.25 @@ -97,8 +105,8 @@
    2.26  *)
    2.27  
    2.28  hide_const (open)
    2.29 -  pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
    2.30 -  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
    2.31 +  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
    2.32 +  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
    2.33  hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
    2.34  (* FIXME: hide facts *)
    2.35  (*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:06 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:07 2010 +0200
     3.3 @@ -92,6 +92,7 @@
     3.4      | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     3.5    val negative_compilation_of : compilation -> compilation
     3.6    val compilation_for_polarity : bool -> compilation -> compilation
     3.7 +  val is_depth_limited_compilation : compilation -> bool 
     3.8    val string_of_compilation : compilation -> string
     3.9    val compilation_names : (string * compilation) list
    3.10    val non_random_compilations : compilation list
    3.11 @@ -646,6 +647,9 @@
    3.12    | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
    3.13    | compilation_for_polarity _ c = c
    3.14  
    3.15 +fun is_depth_limited_compilation c =
    3.16 +  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq)
    3.17 +
    3.18  fun string_of_compilation c =
    3.19    case c of
    3.20      Pred => ""
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:06 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:07 2010 +0200
     4.3 @@ -182,6 +182,13 @@
     4.4    in
     4.5      Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
     4.6    end;
     4.7 +  
     4.8 +fun mk_decr_bind (x, f) =
     4.9 +  let
    4.10 +    val T as Type ("fun", [_, U]) = fastype_of f
    4.11 +  in
    4.12 +    Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
    4.13 +  end;
    4.14  
    4.15  val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
    4.16  
    4.17 @@ -206,7 +213,12 @@
    4.18  fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
    4.19    (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
    4.20  
    4.21 -val compfuns = Predicate_Compile_Aux.CompilationFuns
    4.22 +val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
    4.23 +    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
    4.24 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
    4.25 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    4.26 +
    4.27 +val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
    4.28      {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
    4.29      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    4.30      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    4.31 @@ -241,6 +253,13 @@
    4.32      Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
    4.33    end;
    4.34  
    4.35 +fun mk_decr_bind (x, f) =
    4.36 +  let
    4.37 +    val T as Type ("fun", [_, U]) = fastype_of f
    4.38 +  in
    4.39 +    Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
    4.40 +  end;
    4.41 +
    4.42  val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
    4.43  
    4.44  fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
    4.45 @@ -262,7 +281,12 @@
    4.46  fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
    4.47    (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
    4.48  
    4.49 -val compfuns = Predicate_Compile_Aux.CompilationFuns
    4.50 +val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
    4.51 +    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
    4.52 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
    4.53 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    4.54 +
    4.55 +val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
    4.56      {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
    4.57      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    4.58      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:06 2010 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:07 2010 +0200
     5.3 @@ -839,8 +839,26 @@
     5.4  val wrap_compilation = #wrap_compilation o dest_comp_modifiers
     5.5  val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
     5.6  
     5.7 +fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random,
     5.8 +    modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) =
     5.9 +    (Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix,
    5.10 +    compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT,
    5.11 +    additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
    5.12 +    transform_additional_arguments = transform_additional_arguments})
    5.13 +
    5.14  end;
    5.15  
    5.16 +fun unlimited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
    5.17 +    New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.18 +  | unlimited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
    5.19 +    New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.20 +  
    5.21 +fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
    5.22 +    New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    5.23 +  | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
    5.24 +    New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
    5.25 +
    5.26 +
    5.27  val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
    5.28    {
    5.29    compilation = Depth_Limited,
    5.30 @@ -1028,7 +1046,7 @@
    5.31    {
    5.32    compilation = New_Pos_Random_DSeq,
    5.33    function_name_prefix = "new_random_dseq_",
    5.34 -  compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
    5.35 +  compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
    5.36    mk_random = (fn T => fn additional_arguments =>
    5.37    let
    5.38      val random = Const ("Quickcheck.random_class.random",
    5.39 @@ -1050,7 +1068,7 @@
    5.40    {
    5.41    compilation = New_Neg_Random_DSeq,
    5.42    function_name_prefix = "new_random_dseq_neg_",
    5.43 -  compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
    5.44 +  compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns,
    5.45    mk_random = (fn _ => error "no random generation"),
    5.46    modify_funT = I,
    5.47    additional_arguments = K [],
    5.48 @@ -1964,8 +1982,16 @@
    5.49  
    5.50  fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
    5.51    let
    5.52 -    val compilation_modifiers = if pol then compilation_modifiers else
    5.53 -      negative_comp_modifiers_of compilation_modifiers
    5.54 +    val is_terminating = true (* FIXME: requires an termination analysis *)  
    5.55 +    val compilation_modifiers =
    5.56 +      (if pol then compilation_modifiers else
    5.57 +        negative_comp_modifiers_of compilation_modifiers)
    5.58 +      |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
    5.59 +           (if is_terminating then
    5.60 +             (Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
    5.61 +           else
    5.62 +             (Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
    5.63 +         else I)
    5.64      val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
    5.65        (all_vs @ param_vs)
    5.66      val compfuns = Comp_Mod.compfuns compilation_modifiers
    5.67 @@ -3062,9 +3088,9 @@
    5.68      let
    5.69        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
    5.70        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
    5.71 -    in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.compfuns
    5.72 +    in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    5.73        options preds (s, pos_modes)
    5.74 -      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.compfuns
    5.75 +      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
    5.76        options preds (s, neg_modes)
    5.77      end,
    5.78    prove = prove_by_skip,
    5.79 @@ -3292,7 +3318,7 @@
    5.80          Random => PredicateCompFuns.compfuns
    5.81        | DSeq => DSequence_CompFuns.compfuns
    5.82        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
    5.83 -      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
    5.84 +      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.85        | _ => PredicateCompFuns.compfuns
    5.86      val t = analyze_compr ctxt compfuns param_user_modes options t_compr;
    5.87      val T = dest_predT compfuns (fastype_of t);