Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
author wenzelm
Mon, 20 May 2024 15:43:51 +0200
changeset 80182 29f2b8ff84f3
parent 76183 8089593a364a
permissions -rw-r--r--
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f);

(*  Title:      HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
    Author:     Jasmin Blanchette, TU Munich
    Author:     Sascha Boehme, TU Munich
    Author:     Martin Desharnais, UniBw Munich

Mirabelle action: "quickcheck".
*)

structure Mirabelle_Quickcheck: MIRABELLE_ACTION =
struct

fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) =
  let
    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    val quickcheck =
      Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1

    fun run ({pre, ...} : Mirabelle.command) =
      (case Timeout.apply timeout quickcheck pre of
        NONE => "no counterexample"
      | SOME _ => "counterexample found")
  in ("", {run = run, finalize = K ""}) end

val () = Mirabelle.register_action "quickcheck" make_action

end
isabelle