adding depth_limited_random compilation to predicate compiler
authorbulwahn
Mon Mar 22 08:30:13 2010 +0100 (2010-03-22)
changeset 35881aa412e08bfee
parent 35880 2623b23e41fc
child 35882 9bb2c5b0c297
adding depth_limited_random compilation to predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -478,7 +478,7 @@
     1.4  
     1.5  (* Different options for compiler *)
     1.6  
     1.7 -datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated
     1.8 +datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
     1.9    | Pos_Random_DSeq | Neg_Random_DSeq
    1.10  
    1.11  
    1.12 @@ -493,6 +493,7 @@
    1.13      Pred => ""
    1.14    | Random => "random"
    1.15    | Depth_Limited => "depth limited"
    1.16 +  | Depth_Limited_Random => "depth limited random"
    1.17    | DSeq => "dseq"
    1.18    | Annotated => "annotated"
    1.19    | Pos_Random_DSeq => "pos_random dseq"
    1.20 @@ -571,7 +572,9 @@
    1.21  
    1.22  val compilation_names = [("pred", Pred),
    1.23    ("random", Random),
    1.24 -  ("depth_limited", Depth_Limited), (*("annotated", Annotated),*)
    1.25 +  ("depth_limited", Depth_Limited),
    1.26 +  ("depth_limited_random", Depth_Limited_Random),
    1.27 +  (*("annotated", Annotated),*)
    1.28    ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
    1.29  
    1.30  fun print_step options s =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     2.3 @@ -2586,6 +2586,50 @@
     2.4    transform_additional_arguments = K I : (indprem -> term list -> term list)
     2.5    }
     2.6  
     2.7 +val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
     2.8 +  {
     2.9 +  compilation = Depth_Limited_Random,
    2.10 +  function_name_prefix = "depth_limited_random_",
    2.11 +  compfuns = PredicateCompFuns.compfuns,
    2.12 +  mk_random = (fn T => fn additional_arguments =>
    2.13 +  list_comb (Const(@{const_name Quickcheck.iter},
    2.14 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    2.15 +    PredicateCompFuns.mk_predT T), tl additional_arguments)),
    2.16 +  modify_funT = (fn T =>
    2.17 +    let
    2.18 +      val (Ts, U) = strip_type T
    2.19 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    2.20 +        @{typ "code_numeral * code_numeral"}]
    2.21 +    in (Ts @ Ts') ---> U end),
    2.22 +  additional_arguments = (fn names =>
    2.23 +    let
    2.24 +      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
    2.25 +    in
    2.26 +      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
    2.27 +        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
    2.28 +    end),
    2.29 +  wrap_compilation =
    2.30 +  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    2.31 +    let
    2.32 +      val depth = hd (additional_arguments)
    2.33 +      val (_, Ts) = split_modeT' mode (binder_types T)
    2.34 +      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    2.35 +      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    2.36 +    in
    2.37 +      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
    2.38 +        $ mk_bot compfuns (dest_predT compfuns T')
    2.39 +        $ compilation
    2.40 +    end,
    2.41 +  transform_additional_arguments =
    2.42 +    fn prem => fn additional_arguments =>
    2.43 +    let
    2.44 +      val [depth, nrandom, size, seed] = additional_arguments
    2.45 +      val depth' =
    2.46 +        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
    2.47 +          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
    2.48 +    in [depth', nrandom, size, seed] end
    2.49 +}
    2.50 +
    2.51  (* different instantiantions of the predicate compiler *)
    2.52  
    2.53  val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
    2.54 @@ -2713,6 +2757,18 @@
    2.55    use_random = true,
    2.56    qname = "random_equation"})
    2.57  
    2.58 +val add_depth_limited_random_equations = gen_add_equations
    2.59 +  (Steps {
    2.60 +  define_functions =
    2.61 +    fn options => fn preds => fn (s, modes) =>
    2.62 +      define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
    2.63 +      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
    2.64 +  comp_modifiers = depth_limited_random_comp_modifiers,
    2.65 +  prove = prove_by_skip,
    2.66 +  add_code_equations = K (K I),
    2.67 +  use_random = true,
    2.68 +  qname = "depth_limited_random_equation"})
    2.69 +
    2.70  val add_dseq_equations = gen_add_equations
    2.71    (Steps {
    2.72    define_functions =
    2.73 @@ -2798,6 +2854,7 @@
    2.74             | Pos_Random_DSeq => add_random_dseq_equations
    2.75             | Depth_Limited => add_depth_limited_equations
    2.76             | Random => add_random_equations
    2.77 +           | Depth_Limited_Random => add_depth_limited_random_equations
    2.78             | compilation => error ("Compilation not supported")
    2.79             ) options [const]))
    2.80        end
    2.81 @@ -2881,6 +2938,8 @@
    2.82              [@{term "(1, 1) :: code_numeral * code_numeral"}]
    2.83            | Annotated => []
    2.84            | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
    2.85 +          | Depth_Limited_Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
    2.86 +            [@{term "(1, 1) :: code_numeral * code_numeral"}]
    2.87            | DSeq => []
    2.88            | Pos_Random_DSeq => []
    2.89          val comp_modifiers =
    2.90 @@ -2888,6 +2947,7 @@
    2.91              Pred => predicate_comp_modifiers
    2.92            | Random => random_comp_modifiers
    2.93            | Depth_Limited => depth_limited_comp_modifiers
    2.94 +          | Depth_Limited_Random => depth_limited_random_comp_modifiers
    2.95            (*| Annotated => annotated_comp_modifiers*)
    2.96            | DSeq => dseq_comp_modifiers
    2.97            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers