src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 35881 aa412e08bfee
parent 35880 2623b23e41fc
child 35884 362bfc2ca0ee
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -2586,6 +2586,50 @@
     1.4    transform_additional_arguments = K I : (indprem -> term list -> term list)
     1.5    }
     1.6  
     1.7 +val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
     1.8 +  {
     1.9 +  compilation = Depth_Limited_Random,
    1.10 +  function_name_prefix = "depth_limited_random_",
    1.11 +  compfuns = PredicateCompFuns.compfuns,
    1.12 +  mk_random = (fn T => fn additional_arguments =>
    1.13 +  list_comb (Const(@{const_name Quickcheck.iter},
    1.14 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    1.15 +    PredicateCompFuns.mk_predT T), tl additional_arguments)),
    1.16 +  modify_funT = (fn T =>
    1.17 +    let
    1.18 +      val (Ts, U) = strip_type T
    1.19 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    1.20 +        @{typ "code_numeral * code_numeral"}]
    1.21 +    in (Ts @ Ts') ---> U end),
    1.22 +  additional_arguments = (fn names =>
    1.23 +    let
    1.24 +      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
    1.25 +    in
    1.26 +      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
    1.27 +        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
    1.28 +    end),
    1.29 +  wrap_compilation =
    1.30 +  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    1.31 +    let
    1.32 +      val depth = hd (additional_arguments)
    1.33 +      val (_, Ts) = split_modeT' mode (binder_types T)
    1.34 +      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    1.35 +      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    1.36 +    in
    1.37 +      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
    1.38 +        $ mk_bot compfuns (dest_predT compfuns T')
    1.39 +        $ compilation
    1.40 +    end,
    1.41 +  transform_additional_arguments =
    1.42 +    fn prem => fn additional_arguments =>
    1.43 +    let
    1.44 +      val [depth, nrandom, size, seed] = additional_arguments
    1.45 +      val depth' =
    1.46 +        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
    1.47 +          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
    1.48 +    in [depth', nrandom, size, seed] end
    1.49 +}
    1.50 +
    1.51  (* different instantiantions of the predicate compiler *)
    1.52  
    1.53  val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
    1.54 @@ -2713,6 +2757,18 @@
    1.55    use_random = true,
    1.56    qname = "random_equation"})
    1.57  
    1.58 +val add_depth_limited_random_equations = gen_add_equations
    1.59 +  (Steps {
    1.60 +  define_functions =
    1.61 +    fn options => fn preds => fn (s, modes) =>
    1.62 +      define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
    1.63 +      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
    1.64 +  comp_modifiers = depth_limited_random_comp_modifiers,
    1.65 +  prove = prove_by_skip,
    1.66 +  add_code_equations = K (K I),
    1.67 +  use_random = true,
    1.68 +  qname = "depth_limited_random_equation"})
    1.69 +
    1.70  val add_dseq_equations = gen_add_equations
    1.71    (Steps {
    1.72    define_functions =
    1.73 @@ -2798,6 +2854,7 @@
    1.74             | Pos_Random_DSeq => add_random_dseq_equations
    1.75             | Depth_Limited => add_depth_limited_equations
    1.76             | Random => add_random_equations
    1.77 +           | Depth_Limited_Random => add_depth_limited_random_equations
    1.78             | compilation => error ("Compilation not supported")
    1.79             ) options [const]))
    1.80        end
    1.81 @@ -2881,6 +2938,8 @@
    1.82              [@{term "(1, 1) :: code_numeral * code_numeral"}]
    1.83            | Annotated => []
    1.84            | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
    1.85 +          | Depth_Limited_Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
    1.86 +            [@{term "(1, 1) :: code_numeral * code_numeral"}]
    1.87            | DSeq => []
    1.88            | Pos_Random_DSeq => []
    1.89          val comp_modifiers =
    1.90 @@ -2888,6 +2947,7 @@
    1.91              Pred => predicate_comp_modifiers
    1.92            | Random => random_comp_modifiers
    1.93            | Depth_Limited => depth_limited_comp_modifiers
    1.94 +          | Depth_Limited_Random => depth_limited_random_comp_modifiers
    1.95            (*| Annotated => annotated_comp_modifiers*)
    1.96            | DSeq => dseq_comp_modifiers
    1.97            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers