src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML

modernized setup;

(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
    Author:     Lukas Bulwahn, TU Muenchen

A quickcheck generator based on the predicate compiler.
*)

signature PREDICATE_COMPILE_QUICKCHECK =
sig
  type seed = Random_Engine.seed
  (*val quickcheck : Proof.context -> term -> int -> term list option*)
  val put_pred_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
      term list Predicate.pred) ->
    Proof.context -> Proof.context
  val put_dseq_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
      term list Limited_Sequence.dseq * seed) ->
    Proof.context -> Proof.context
  val put_lseq_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
      term list Lazy_Sequence.lazy_sequence) ->
    Proof.context -> Proof.context
  val put_new_dseq_result :
    (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
    Proof.context -> Proof.context
  val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) ->
    Proof.context -> Proof.context
  val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list ->
    Quickcheck.result list
  val nrandom : int Unsynchronized.ref
  val debug : bool Unsynchronized.ref
  val no_higher_order_predicate : string list Unsynchronized.ref
end;

structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
struct

open Predicate_Compile_Aux;

type seed = Random_Engine.seed;

(* FIXME just one data slot (record) per program unit *)

structure Pred_Result = Proof_Data
(
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
  (* FIXME avoid user error with non-user text *)
  fun init _ () = error "Pred_Result"
)
val put_pred_result = Pred_Result.put

structure Dseq_Result = Proof_Data
(
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
  (* FIXME avoid user error with non-user text *)
  fun init _ () = error "Dseq_Result"
)
val put_dseq_result = Dseq_Result.put

structure Lseq_Result = Proof_Data
(
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
  (* FIXME avoid user error with non-user text *)
  fun init _ () = error "Lseq_Result"
)
val put_lseq_result = Lseq_Result.put

structure New_Dseq_Result = Proof_Data
(
  type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
  (* FIXME avoid user error with non-user text *)
  fun init _ () = error "New_Dseq_Random_Result"
)
val put_new_dseq_result = New_Dseq_Result.put

structure CPS_Result = Proof_Data
(
  type T = unit -> Code_Numeral.natural -> (bool * term list) option
  (* FIXME avoid user error with non-user text *)
  fun init _ () = error "CPS_Result"
)
val put_cps_result = CPS_Result.put

val target = "Quickcheck"

val nrandom = Unsynchronized.ref 3

val debug = Unsynchronized.ref false

val no_higher_order_predicate = Unsynchronized.ref ([] : string list)

val options = Options {
  expected_modes = NONE,
  proposed_modes = [],
  proposed_names = [],
  show_steps = false,
  show_intermediate_results = false,
  show_proof_trace = false,
  show_modes = false,
  show_mode_inference = false,
  show_compilation = false,
  show_caught_failures = false,
  show_invalid_clauses = false,
  skip_proof = false,
  compilation = Random,
  inductify = true,
  specialise = true,
  detect_switches = false,
  function_flattening = true,
  fail_safe_function_flattening = false,
  no_higher_order_predicate = [],
  smart_depth_limiting = true,
  no_topmost_reordering = false
}

val debug_options = Options {
  expected_modes = NONE,
  proposed_modes = [],
  proposed_names = [],
  show_steps = true,
  show_intermediate_results = true,
  show_proof_trace = false,
  show_modes = true,
  show_mode_inference = true,
  show_compilation = false,
  show_caught_failures = true,
  show_invalid_clauses = false,
  skip_proof = false,
  compilation = Random,
  inductify = true,
  specialise = true,
  detect_switches = false,
  function_flattening = true,
  fail_safe_function_flattening = false,
  no_higher_order_predicate = [],
  smart_depth_limiting = true,
  no_topmost_reordering = true
}


fun set_function_flattening b
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _,
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})

fun set_fail_safe_function_flattening b
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    fail_safe_function_flattening = _, no_higher_order_predicate = no_ho,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})

fun set_no_higher_order_predicate ss
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = _,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    show_invalid_clauses = s_ic, skip_proof = s_p,
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss,
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})


fun get_options () =
  set_no_higher_order_predicate (!no_higher_order_predicate)
    (if !debug then debug_options else options)

val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns
val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns

val mk_randompredT = Predicate_Compile_Aux.mk_monadT 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 =
  Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
val mk_new_return =
  Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
val mk_new_bind =
  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns

val mk_new_dseqT =
  Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
val mk_gen_return =
  Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
val mk_gen_bind =
  Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns


val mk_cpsT =
  Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns

val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple

fun cpu_time description e =
  let val ({cpu, ...}, result) = Timing.timing e ()
  in (result, (description, Time.toMilliseconds cpu)) end

fun compile_term compilation options ctxt t =
  let
    val t' = fold_rev absfree (Term.add_frees t []) t
    val thy = Proof_Context.theory_of ctxt
    val ((((full_constname, constT), vs'), intro), thy1) =
      Predicate_Compile_Aux.define_quickcheck_predicate t' thy
    val thy2 =
      Context.theory_map (Named_Theorems.add_thm @{named_theorems code_pred_def} intro) thy1
    val (thy3, _) = cpu_time "predicate preprocessing"
        (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
    val (thy4, _) = cpu_time "random_dseq core compilation"
        (fn () =>
          case compilation of
            Pos_Random_DSeq =>
              Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3
          | New_Pos_Random_DSeq =>
              Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
          | Pos_Generator_DSeq =>
              Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
          | Pos_Generator_CPS =>
               Predicate_Compile_Core.add_generator_cps_equations options [full_constname] thy3
          (*| Depth_Limited_Random =>
              Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
    (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
    val ctxt4 = Proof_Context.init_global thy4
    val modes = Core_Data.modes_of compilation ctxt4 full_constname
    val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
    val prog =
      if member eq_mode modes output_mode then
        let
          val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
          val T =
            (case compilation of
              Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
            | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
            | Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
            | Depth_Limited_Random =>
                [@{typ natural}, @{typ natural}, @{typ natural},
                 @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs')))
        in
          Const (name, T)
        end
      else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
    fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
    val qc_term =
      (case compilation of
        Pos_Random_DSeq => mk_bind (prog,
          mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
      | New_Pos_Random_DSeq => mk_new_bind (prog,
          mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
      | Pos_Generator_DSeq => mk_gen_bind (prog,
          mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
      | Pos_Generator_CPS => prog $
          mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
          HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))
      | Depth_Limited_Random => fold_rev absdummy
          [@{typ natural}, @{typ natural}, @{typ natural},
           @{typ Random.seed}]
          (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
          mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))))
    val prog =
      case compilation of
        Pos_Random_DSeq =>
          let
            val compiled_term =
              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
                (Proof_Context.init_global thy4) (SOME target)
                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
                qc_term []
          in
            (fn size => fn nrandom => fn depth =>
              Option.map fst (Limited_Sequence.yield
                (compiled_term nrandom size |> Random_Engine.run) depth true))
          end
      | New_Pos_Random_DSeq =>
          let
            val compiled_term =
              Code_Runtime.dynamic_value_strict
                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
                (Proof_Context.init_global thy4) (SOME target)
                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
                  qc_term []
          in
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
               (
               let
                 val seed = Random_Engine.next_seed ()
               in compiled_term nrandom size seed depth end))
          end
      | Pos_Generator_DSeq =>
          let
            val compiled_term =
              Code_Runtime.dynamic_value_strict
                (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
                (Proof_Context.init_global thy4) (SOME target)
                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
                qc_term []
          in
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
          end
      | Pos_Generator_CPS =>
          let
            val compiled_term =
              Code_Runtime.dynamic_value_strict
                (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
                (Proof_Context.init_global thy4) (SOME target)
                (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
                qc_term []
          in
            fn _ => fn _ => Option.map snd o compiled_term
          end
       | Depth_Limited_Random =>
          let
            val compiled_term = Code_Runtime.dynamic_value_strict
              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
                (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
                  g depth nrandom size seed |> (Predicate.map o map) proc)
                qc_term []
          in
            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
              (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
          end
  in
    prog
  end

fun try_upto_depth ctxt f =
  let
    val max_depth = Config.get ctxt Quickcheck.depth
    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    fun try' i =
      if i <= max_depth then
        let
          val _ = message ("Depth: " ^ string_of_int i)
          val (result, time) =
            cpu_time ("Depth " ^ string_of_int i) (fn () =>
              f i handle Match => (if Config.get ctxt Quickcheck.quiet then ()
                    else warning "Exception Match raised during quickcheck"; NONE))
         val _ = if Config.get ctxt Quickcheck.timing then
           message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
        in
          (case result of NONE => try' (i + 1) | SOME q => SOME q)
        end
      else NONE
  in
    try' 0
  end


(* quickcheck interface functions *)

fun compile_term' compilation options ctxt (t, _) =
  let
    val size = Config.get ctxt Quickcheck.size
    val c = compile_term compilation options ctxt t
    val counterexample = try_upto_depth ctxt (c (Code_Numeral.natural_of_integer size)
      (Code_Numeral.natural_of_integer (!nrandom)) o Code_Numeral.natural_of_integer)
  in
    Quickcheck.Result
      {counterexample =
        Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
       evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
  end

fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening =
  let
     val options =
       set_fail_safe_function_flattening fail_safe_function_flattening
         (set_function_flattening function_flattening (get_options ()))
  in
    compile_term' compilation options
  end


fun test_goals options ctxt _ insts goals =
  let
    val (compilation, fail_safe_function_flattening) = options
    val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion)
    val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
    val test_term =
      quickcheck_compile_term compilation function_flattening fail_safe_function_flattening
  in
    Quickcheck_Common.collect_results (test_term ctxt)
      (maps (map snd) correct_inst_goals) []
  end

val smart_exhaustive_active =
  Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true)
val smart_slow_exhaustive_active =
  Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false)

val _ =
  Theory.setup
   (Exhaustive_Generators.setup_exhaustive_datatype_interpretation #>
    Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
      (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false)))) #>
    Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
      (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false)))))

end