Mercurial Mercurial > repos > isabelle / annotate
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/Mirabelle/Tools/mirabelle_quickcheck.ML
author nipkow
Wed, 10 Jan 2018 15:25:09 +0100
changeset 67399 eab6ce8368fa
parent 62519 a564458f94db
child 67405 e9ab4ad7bd15
permissions -rw-r--r--
ran isabelle update_op on all sources
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47847
7cddb6c8f93c updated headers;
wenzelm
parents: 47730
diff changeset 
     1
 
(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
32564
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32521
diff changeset 
     2
 
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset 
     3
 
*)
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset 
     4
 












594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




     5


structure Mirabelle_Quickcheck : MIRABELLE_ACTION =













594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




     6


struct













594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




     7









32521






f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




     8


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













f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




     9














f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    10


fun init _ = I













f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    11


fun done _ _ = ()













f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    12









32567






de411627a985
explicitly export type abbreviations (as usual in SML97);



wenzelm


parents: 
32564

diff
changeset




    13


fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =








32385






594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    14


  let








67399






eab6ce8368fa
ran isabelle update_op on all sources



nipkow


parents: 
62519

diff
changeset




    15


    val has_valid_key = member (=) ["iterations", "size", "generator"] o fst








37920






581c1e5f53e0
fixing quickcheck invocation in HOL-Mirabelle



bulwahn


parents: 
32567

diff
changeset




    16


    val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1








32385






594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    17


  in








62519






a564458f94db
tuned signature -- clarified modules;



wenzelm


parents: 
47847

diff
changeset




    18


    (case Timeout.apply timeout quickcheck pre of








32521






f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    19


      NONE => log (qc_tag id ^ "no counterexample")













f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    20


    | SOME _ => log (qc_tag id ^ "counterexample found"))








32385






594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    21


  end








62519






a564458f94db
tuned signature -- clarified modules;



wenzelm


parents: 
47847

diff
changeset




    22


  handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout")








32521






f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    23


       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)








32385






594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    24









32515






e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),



boehmes


parents: 
32498

diff
changeset




    25


fun invoke args =








32521






f20cc66b2c74
added initialization and cleanup of actions,



boehmes


parents: 
32518

diff
changeset




    26


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








32385






594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    27














594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)



boehmes


parents: 

diff
changeset




    28


end















isabelle