<commit_before>(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
    Author:     <NAME> and <NAME>, TU Munich
*)

structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct

fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "

fun init _ = I
fun done _ _ = ()

fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
  let
    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
  in
    (case TimeLimit.timeLimit timeout quickcheck pre of
      NONE => log (qc_tag id ^ "no counterexample")
    | SOME _ => log (qc_tag id ^ "counterexample found"))
  end
  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)

fun invoke args =
  Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)

end<commit_msg>fixing quickcheck invocation in HOL-Mirabelle<commit_after>(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
    Author:     <NAME> and <NAME>, TU Munich
*)

structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct

fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "

fun init _ = I
fun done _ _ = ()

fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
  let
    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
  in
    (case TimeLimit.timeLimit timeout quickcheck pre of
      NONE => log (qc_tag id ^ "no counterexample")
    | SOME _ => log (qc_tag id ^ "counterexample found"))
  end
  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)

fun invoke args =
  Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)

end
{'fraction_non_alphanumeric': 0.12099837221920781, 'fraction_numerical': 0.0010851871947911015, 'mean_word_length': 3.5530864197530865, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7312961', 'n_tokens_mistral': 650, 'n_tokens_neox': 640, 'n_words': 192}