src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML
changeset 32469 1ad7d4fc0954
parent 32385 594890623c46
equal deleted inserted replaced
32468:3e6f5365971e 32469:1ad7d4fc0954
     3 *)
     3 *)
     4 
     4 
     5 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     5 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     6 struct
     6 struct
     7 
     7 
     8 fun quickcheck_action args {pre=st, ...} =
     8 fun quickcheck_action limit args {pre=st, ...} =
     9   let
     9   let
    10     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    10     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
       
    11     val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
    11   in
    12   in
    12     (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
    13     (case TimeLimit.timeLimit limit quickcheck st of
    13       NONE => SOME "no counterexample"
    14       NONE => SOME "no counterexample"
    14     | SOME _ => SOME "counterexample found")
    15     | SOME _ => SOME "counterexample found")
    15   end
    16   end
    16 
    17 
    17 fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
    18 fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)