diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,607 +1,608 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations BTree Banach_Steinhaus Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpreter_Optimizations Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regression_Test_Selection Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem +SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/SpecCheck/README.md b/thys/SpecCheck/README.md new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/README.md @@ -0,0 +1,61 @@ +# SpecCheck + +SpecCheck is a [QuickCheck](https://en.wikipedia.org/wiki/QuickCheck)-like testing framework for Isabelle/ML. +You can use it to write specifications for ML functions. +SpecCheck then checks whether your specification holds by testing your function against a given number of generated inputs. +It helps you to identify bugs by printing counterexamples on failure and provides you timing information. + +SpecCheck is customisable and allows you to specify your own input generators, +test output formats, as well as pretty printers and shrinking functions for counterexamples +among other things. + +## Quick Usage +1. Import `SpecCheck.SpecCheck` into your environment. +2. Write specifications using the ML invocation: `check show gen name prop ctxt seed` where + * `show` converts values into `Pretty.T` types to show the failing inputs. See `show/`. + * `gen` is the value generator used for the test. See `generators/`. + * `name` is the name of the test case + * `prop` is the property to be tested. See `property.ML` + * `seed` is the initial seed for the generator. + +You can also choose to omit the show method for rapid testing or add a shrinking method à la +QuickCheck to get better counterexamples. See `speccheck.ML`. + +An experimental alternative allows you to specify tests using strings: +1. Import `SpecCheck_Dynamic.Dynamic` into your environment. +2. `check_property "ALL x. P x"` where `P x` is some ML code evaluating to a boolean + +Examples can be found in `examples/`. + +## Notes + +SpecCheck is based on [QCheck](https://github.com/league/qcheck), a testing framework for Standard ML by +[Christopher League](https://contrapunctus.net/league/). +As Isabelle/ML provides a rich and uniform ML platform, some features where removed or adapted, in particular: + +1. Isabelle/ML provides common data structures, which we can use in the +tool's implementation for storing data and printing output. + +2. Implementations in Isabelle/ML checked with this tool commonly use Isabelle/ML's `int` type +(which corresponds ML's `IntInf.int`), but do not use other integer types in ML such as ML's `Int.int`, +`Word.word`, and others. + +3. As Isabelle makes heavy use of parallelism, we avoid reference types. + +## Next Steps + +* Implement more shrinking methods for commonly used types +* Implement sizing methods (cf. QuickCheck's `sized`) + +## License + +The source code originated from Christopher League's QCheck, which is +licensed under the 2-clause BSD license. The current source code is +licensed under the compatible 3-clause BSD license of Isabelle. + +## Authors + +* Lukas Bulwahn +* Nicolai Schaffroth +* Sebastian Willenbrink +* Kevin Kappelmann diff --git a/thys/SpecCheck/ROOT b/thys/SpecCheck/ROOT new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/ROOT @@ -0,0 +1,30 @@ +chapter AFP + +session SpecCheck (AFP) = "Pure" + + description + \SpecCheck is a specification-based testing environment for ML programs. It is based on QCheck + (\<^url>\https://github.com/league/qcheck/\) by Christopher League (\<^url>\https://contrapunctus.net/\). + It got adapted and extended to fit into the Isabelle/ML framework and resemble the very + successful QuickCheck (\<^url>\https://en.wikipedia.org/wiki/QuickCheck\) more closely.\ + options [timeout = 300] + + directories + dynamic + examples + generators + output_styles + "show" + shrink + + theories + SpecCheck_Generators + SpecCheck_Output_Style + SpecCheck_Show + SpecCheck_Shrink + SpecCheck + SpecCheck_Dynamic + theories [document = false] + SpecCheck_Examples + + document_files + "root.tex" diff --git a/thys/SpecCheck/SpecCheck.thy b/thys/SpecCheck/SpecCheck.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/SpecCheck.thy @@ -0,0 +1,17 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \SpecCheck\ +theory SpecCheck +imports + SpecCheck_Generators + SpecCheck_Show + SpecCheck_Shrink + SpecCheck_Output_Style +begin + +paragraph \Summary\ +text \The SpecCheck (specification based) testing environment and Lecker testing framework.\ + +ML_file \speccheck.ML\ +ML_file \lecker.ML\ + +end diff --git a/thys/SpecCheck/SpecCheck_Base.thy b/thys/SpecCheck/SpecCheck_Base.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/SpecCheck_Base.thy @@ -0,0 +1,18 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \SpecCheck Base\ +theory SpecCheck_Base +imports Pure +begin + +paragraph \Summary\ +text \Basic setup for SpecCheck.\ + +ML_file \util.ML\ + +ML_file \speccheck_base.ML\ +ML_file \property.ML\ +ML_file \configuration.ML\ + +ML_file \random.ML\ + +end diff --git a/thys/SpecCheck/configuration.ML b/thys/SpecCheck/configuration.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/configuration.ML @@ -0,0 +1,41 @@ +(* Title: SpecCheck/configuration.ML + Author: Kevin Kappelmann + +Configuration options for SpecCheck. +*) + +signature SPECCHECK_CONFIGURATION = +sig + + (*maximum number of successful tests before succeeding*) + val max_success : int Config.T + (*maximum number of discarded tests per successful test before giving up*) + val max_discard_ratio : int Config.T + (*maximum number of shrinks per counterexample*) + val max_shrinks : int Config.T + (*number of counterexamples shown*) + val num_counterexamples : int Config.T + (*sort counterexamples by size*) + val sort_counterexamples : bool Config.T + (*print timing etc. depending on style*) + val show_stats : bool Config.T + +end + +structure SpecCheck_Configuration : SPECCHECK_CONFIGURATION = +struct + +val max_success = Attrib.setup_config_int \<^binding>\speccheck_max_success\ (K 100) + +val max_discard_ratio = Attrib.setup_config_int \<^binding>\speccheck_max_discard_ratio\ (K 10) + +val max_shrinks = Attrib.setup_config_int \<^binding>\speccheck_max_shrinks\ (K 10000) + +val num_counterexamples = Attrib.setup_config_int \<^binding>\speccheck_num_counterexamples\ (K 1) + +val sort_counterexamples = + Attrib.setup_config_bool \<^binding>\speccheck_sort_counterexamples\ (K true) + +val show_stats = Attrib.setup_config_bool \<^binding>\speccheck_show_stats\ (K true) + +end diff --git a/thys/SpecCheck/document/root.tex b/thys/SpecCheck/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/document/root.tex @@ -0,0 +1,39 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{SpecCheck -- Specification-Based Testing for Isabelle/ML} +\author{Kevin Kappelmann, Lukas Bulwahn, and Sebastian Willenbrink} +\maketitle + +\begin{abstract} +SpecCheck is a \href{https://en.wikipedia.org/wiki/QuickCheck}{QuickCheck}-like testing framework +for Isabelle/ML. +You can use it to write specifications for ML functions. +SpecCheck then checks whether your specification holds by testing your function against a given number of generated inputs. +It helps you to identify bugs by printing counterexamples on failure and provides you timing information. + +SpecCheck is customisable and allows you to specify your own input generators, +test output formats, as well as pretty printers and shrinking functions for counterexamples +among other things. +\end{abstract} + +\tableofcontents + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy b/thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy @@ -0,0 +1,16 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Dynamic Generators\ +theory SpecCheck_Dynamic +imports SpecCheck +begin + +paragraph \Summary\ +text \Generators and show functions for SpecCheck that are dynamically derived from a given ML input +string. This approach can be handy to quickly test a function during development, but it lacks +customisability and is very brittle. See @{file "../examples/SpecCheck_Examples.thy"} for some +examples contrasting this approach to the standard one (specifying generators as ML code).\ + +ML_file \dynamic_construct.ML\ +ML_file \speccheck_dynamic.ML\ + +end diff --git a/thys/SpecCheck/dynamic/dynamic_construct.ML b/thys/SpecCheck/dynamic/dynamic_construct.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/dynamic/dynamic_construct.ML @@ -0,0 +1,188 @@ +(* Title: SpecCheck/dynamic/dynamic_construct.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + +Dynamic construction of generators and show functions (returned as strings that need to be compiled) +from a given string representing ML code to be tested as a SpecCheck test. +*) + +signature SPECCHECK_DYNAMIC_CONSTRUCT = +sig + val register : string * (string * string) -> theory -> theory + type mltype + val parse_pred : string -> string * mltype + val build_check : Proof.context -> string -> mltype * string -> string + (*val safe_check : string -> mltype * string -> string*) + val string_of_bool : bool -> string + val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string +end; + +structure SpecCheck_Dynamic_Construct : SPECCHECK_DYNAMIC_CONSTRUCT = +struct + +(* Parsing ML types *) + +datatype mltype = Var | Con of string * mltype list | Tuple of mltype list; + +(*Split string into tokens for parsing*) +fun split s = + let + fun split_symbol #"(" = "( " + | split_symbol #")" = " )" + | split_symbol #"," = " ," + | split_symbol #":" = " :" + | split_symbol c = Char.toString c + fun is_space c = c = #" " + in String.tokens is_space (String.translate split_symbol s) end; + +(*Accept anything that is not a recognized symbol*) +val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;")); + +(*Turn a type list into a nested Con*) +fun make_con [] = raise Empty + | make_con [c] = c + | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]); + +(*Parse a type*) +fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s + +and parse_type_arg s = (parse_tuple || parse_type_single) s + +and parse_type_single s = (parse_con || parse_type_basic) s + +and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s + +and parse_list s = + ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s + +and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s + +and parse_con s = ((parse_con_nest + || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl) + || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl)) + >> (make_con o rev)) s + +and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s + +and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s + +and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single) + >> (fn (t, tl) => Tuple (t :: tl))) s; + +(*Parse entire type + name*) +fun parse_function s = + let + val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":") + val (name, ty) = p (split s) + val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); + val (typ, _) = Scan.finite stop parse_type ty + in (name, typ) end; + +(*Create desired output*) +fun parse_pred s = + let + val (name, Con ("->", t :: _)) = parse_function s + in (name, t) end; + +(* Construct Generators and Pretty Printers *) + +(*copied from smt_config.ML *) +fun string_of_bool b = if b then "true" else "false" + +fun string_of_ref f r = f (!r) ^ " ref"; + +val initial_content = Symtab.make [ + ("bool", ("SpecCheck_Generator.bernoulli 0.5", "Gen_Construction.string_of_bool")), + ("option", ("SpecCheck_Generator.option (SpecCheck_Generator.bernoulli (2.0 / 3.0))", + "ML_Syntax.print_option")), + ("list", ("SpecCheck_Generator.unfold_while (K (SpecCheck_Generator.bernoulli (2.0 / 3.0)))", + " ML_Syntax.print_list")), + ("unit", ("gen_unit", "fn () => \"()\"")), + ("int", ("SpecCheck_Generator.range_int (~2147483647,2147483647)", "string_of_int")), + ("real", ("SpecCheck_Generator.real", "string_of_real")), + ("char", ("SpecCheck_Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")), + ("string", ("SpecCheck_Generator.string (SpecCheck_Generator.nonneg 100) SpecCheck_Generator.char", + "ML_Syntax.print_string")), + ("->", ("SpecCheck_Generator.function' o snd", "fn (_, _) => fn _ => \"fn\"")), + ("typ", ("SpecCheck_Generator.typ'' (SpecCheck_Generator.return 8) (SpecCheck_Generator.nonneg 4) (SpecCheck_Generator.nonneg 4) (1,1,1)", + "Pretty.string_of o Syntax.pretty_typ (Context.the_local_context ())")), + ("term", ("SpecCheck_Generator.term_tree (fn h => fn _ => " + ^ "let val ngen = SpecCheck_Generator.nonneg (Int.max (0, 4-h))\n" + ^ " val aterm_gen = SpecCheck_Generator.aterm' (SpecCheck_Generator.return 8) ngen (1,1,1,0)\n" + ^ "in SpecCheck_Generator.zip aterm_gen ngen end)", + "Pretty.string_of o Syntax.pretty_term (Context.the_local_context ())"))] + +structure Data = Theory_Data +( + type T = (string * string) Symtab.table + val empty = initial_content + val extend = I + fun merge data : T = Symtab.merge (K true) data +) + +fun data_of ctxt tycon = + (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of + SOME data => data + | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)) + +val generator_of = fst oo data_of +val printer_of = snd oo data_of + +fun register (ty, data) = Data.map (Symtab.update (ty, data)) + +(* +fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table); +*) + +fun combine dict [] = dict + | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts) + +fun compose_generator _ Var = "SpecCheck_Generator.range_int (~2147483647, 2147483647)" + | compose_generator ctxt (Con (s, types)) = + combine (generator_of ctxt s) (map (compose_generator ctxt) types) + | compose_generator ctxt (Tuple t) = + let + fun tuple_body t = space_implode "" + (map + (fn (ty, n) => implode ["val (x", string_of_int n, ", r", string_of_int n, ") = ", + compose_generator ctxt ty, " r", string_of_int (n - 1), " "]) + (t ~~ (1 upto (length t)))) + fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) + in + "fn r0 => let " ^ tuple_body t ^ + "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" + end + +fun compose_printer _ Var = "Int.toString" + | compose_printer ctxt (Con (s, types)) = + combine (printer_of ctxt s) (map (compose_printer ctxt) types) + | compose_printer ctxt (Tuple t) = + let + fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) + fun tuple_body t = space_implode " ^ \", \" ^ " + (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n) + (t ~~ (1 upto (length t)))) + in implode ["fn (", tuple_head (length t), ") => \"(\" ^ ", tuple_body t, " ^ \")\""] end + +(*produce compilable string*) +fun build_check ctxt name (ty, spec) = implode ["SpecCheck.check (Pretty.str o (", + compose_printer ctxt ty, ")) (", compose_generator ctxt ty, ") \"", name, + "\" (SpecCheck_Property.prop (", spec, + ")) (Context.the_local_context ()) (SpecCheck_Random.new ());"] + +(*produce compilable string - non-eqtype functions*) +(* +fun safe_check name (ty, spec) = + let + val default = + (case AList.lookup (op =) (!gen_table) "->" of + NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"") + | SOME entry => entry) + in + (gen_table := + AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table); + build_check name (ty, spec) before + gen_table := AList.update (op =) ("->", default) (!gen_table)) + end; +*) + +end; diff --git a/thys/SpecCheck/dynamic/speccheck_dynamic.ML b/thys/SpecCheck/dynamic/speccheck_dynamic.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/dynamic/speccheck_dynamic.ML @@ -0,0 +1,81 @@ +(* Title: SpecCheck/dynamic/speccheck_dynamic.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + +This file allows to run SpecCheck tests specified as a string representing ML code. + +TODO: this module is not very well tested. +*) + +signature SPECCHECK_DYNAMIC = +sig + val check_dynamic : Proof.context -> string -> unit +end + +structure SpecCheck_Dynamic : SPECCHECK_DYNAMIC = +struct + +(*call the compiler and pass resulting type string to the parser*) +fun determine_type ctxt s = + let + val return = Unsynchronized.ref "return" + val context : ML_Compiler0.context = + {name_space = #name_space ML_Env.context, + print_depth = SOME 1000000, + here = #here ML_Env.context, + print = fn r => return := r, + error = #error ML_Env.context} + val _ = + Context.setmp_generic_context (SOME (Context.Proof ctxt)) + (fn () => + ML_Compiler0.ML context + {line = 0, file = "generated code", verbose = true, debug = false} s) () + in SpecCheck_Dynamic_Construct.parse_pred (! return) end; + +(*call the compiler and run the test*) +fun run_test ctxt s = + Context.setmp_generic_context (SOME (Context.Proof ctxt)) + (fn () => + ML_Compiler0.ML ML_Env.context + {line = 0, file = "generated code", verbose = false, debug = false} s) (); + +(*split input into tokens*) +fun input_split s = + let + fun dot c = c = #"." + fun space c = c = #" " + val (head, code) = Substring.splitl (not o dot) (Substring.full s) + in + (String.tokens space (Substring.string head), + Substring.string (Substring.dropl dot code)) + end; + +(*create the function from the input*) +fun make_fun s = + let + val scan_param = Scan.one (fn s => s <> ";") + fun parameters s = Scan.repeat1 scan_param s + val p = $$ "ALL" |-- parameters + val (split, code) = input_split s + val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); + val (params, _) = Scan.finite stop p split + in "fn (" ^ commas params ^ ") => " ^ code end; + +(*read input and perform the test*) +fun gen_check_property check ctxt s = + let + val func = make_fun s + val (_, ty) = determine_type ctxt func + in run_test ctxt (check ctxt "Dynamic Test" (ty, func)) end; + +val check_dynamic = gen_check_property SpecCheck_Dynamic_Construct.build_check +(*val check_property_safe = gen_check_property Construct_Gen.safe_check*) + +(*perform test for specification function*) +(*fun gen_check_property_f check ctxt s = + let + val (name, ty) = determine_type ctxt s + in run_test ctxt (check ctxt name (ty, s)) end; + +val check_property_f = gen_check_property_f Gen_Dynamic.build_check*) +(*val check_property_safe_f_ = gen_check_property_f Construct_Gen.safe_check*) +end; diff --git a/thys/SpecCheck/examples/SpecCheck_Examples.thy b/thys/SpecCheck/examples/SpecCheck_Examples.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/examples/SpecCheck_Examples.thy @@ -0,0 +1,129 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Examples\ +theory SpecCheck_Examples +imports SpecCheck_Dynamic +begin + +subsection \List examples\ + +ML \ +open SpecCheck +open SpecCheck_Dynamic +structure Gen = SpecCheck_Generator +structure Prop = SpecCheck_Property +structure Show = SpecCheck_Show +structure Shrink = SpecCheck_Shrink +structure Random = SpecCheck_Random +\ + +ML_command \ +let + val int_gen = Gen.range_int (~10000000, 10000000) + val size_gen = Gen.nonneg 10 + val check_list = check_shrink (Show.list Show.int) (Shrink.list Shrink.int) + (Gen.list size_gen int_gen) + fun list_test (k, f, xs) = + AList.lookup (op=) (AList.map_entry (op=) k f xs) k = Option.map f (AList.lookup (op=) xs k) + + val list_test_show = Show.zip3 Show.int Show.none (Show.list (Show.zip Show.int Show.int)) + val list_test_gen = Gen.zip3 int_gen (Gen.function' int_gen) + (Gen.list size_gen (Gen.zip int_gen int_gen)) +in + Lecker.test_group @{context} (Random.new ()) [ + Prop.prop (fn xs => rev xs = xs) |> check_list "rev = I", + Prop.prop (fn xs => rev (rev xs) = xs) |> check_list "rev o rev = I", + Prop.prop list_test |> check list_test_show list_test_gen "lookup map equiv map lookup" + ] +end +\ + +text \The next three examples roughly correspond to the above test group (except that there's no +shrinking). Compared to the string-based method, the method above is more flexible - you can change +your generators, shrinking methods, and show instances - and robust - you are not reflecting strings +(which might contain typos) but entering type-checked code. In exchange, it is a bit more work to +set up the generators. However, in practice, one shouldn't rely on default generators in most cases +anyway.\ + +ML_command \ +check_dynamic @{context} "ALL xs. rev xs = xs"; +\ + +ML_command \ +check_dynamic @{context} "ALL xs. rev (rev xs) = xs"; +\ + +subsection \AList Specification\ + +ML_command \ +(*map_entry applies the function to the element*) +check_dynamic @{context} (implode + ["ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = ", + "Option.map f (AList.lookup (op =) xs k)"]) +\ + +ML_command \ +(*update always results in an entry*) +check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k"; +\ + +ML_command \ +(*update always writes the value*) +check_dynamic @{context} + "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v"; +\ + +ML_command \ +(*default always results in an entry*) +check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k"; +\ + +ML_command \ +(*delete always removes the entry*) +check_dynamic @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)"; +\ + +ML_command \ +(*default writes the entry iff it didn't exist*) +check_dynamic @{context} (implode + ["ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = ", + "(if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))"]) +\ + +subsection \Examples on Types and Terms\ + +ML_command \ +check_dynamic @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t"; +\ + +ML_command \ +check_dynamic @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t"; +\ + + +text \One would think this holds:\ + +ML_command \ +check_dynamic @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)" +\ + +text \But it only holds with this precondition:\ + +ML_command \ +check_dynamic @{context} + "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)" +\ + +subsection \Some surprises\ + +ML_command \ +check_dynamic @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)" +\ + + +ML_command \ +val thy = \<^theory>; +check_dynamic (Context.the_local_context ()) + "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true" +\ + +end diff --git a/thys/SpecCheck/generators/SpecCheck_Generators.thy b/thys/SpecCheck/generators/SpecCheck_Generators.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/SpecCheck_Generators.thy @@ -0,0 +1,20 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Generators\ +theory SpecCheck_Generators +imports SpecCheck_Base +begin + +paragraph \Summary\ +text \Generators for SpecCheck take a state and return a pair consisting of a generated value and +a new state. Refer to @{file "gen_base.ML"} for the most basic combinators.\ + +ML_file \gen_types.ML\ +ML_file \gen_base.ML\ +ML_file \gen_text.ML\ +ML_file \gen_int.ML\ +ML_file \gen_real.ML\ +ML_file \gen_function.ML\ +ML_file \gen_term.ML\ +ML_file \gen.ML\ + +end diff --git a/thys/SpecCheck/generators/gen.ML b/thys/SpecCheck/generators/gen.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen.ML @@ -0,0 +1,15 @@ +(* Title: SpecCheck/generators/gen.ML + Author: Kevin Kappelmann, TU Muenchen + +Structure containing all generators. +*) +structure SpecCheck_Generator = +struct +open SpecCheck_Gen_Types +open SpecCheck_Gen_Base +open SpecCheck_Gen_Text +open SpecCheck_Gen_Real +open SpecCheck_Gen_Int +open SpecCheck_Gen_Function +open SpecCheck_Gen_Term +end diff --git a/thys/SpecCheck/generators/gen_base.ML b/thys/SpecCheck/generators/gen_base.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_base.ML @@ -0,0 +1,244 @@ +(* Title: SpecCheck/generators/gen_base.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Basic utility functions to create and combine generators. +*) + +signature SPECCHECK_GEN_BASE = +sig + include SPECCHECK_GEN_TYPES + + (*generator that always returns the passed value*) + val return : 'a -> ('a, 's) gen_state + val join : (('a, 's) gen_state, 's) gen_state -> ('a, 's) gen_state + + val zip : ('a, 's) gen_state -> ('b, 's) gen_state -> ('a * 'b, 's) gen_state + val zip3 : ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state -> + ('a * 'b * 'c, 's) gen_state + val zip4 : ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state -> ('d, 's) gen_state -> + ('a * 'b * 'c * 'd, 's) gen_state + val map : ('a -> 'b) -> ('a, 's) gen_state -> ('b, 's) gen_state + val map2 : ('a -> 'b -> 'c) -> ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state + val map3 : ('a -> 'b -> 'c -> 'd) -> ('a, 's) gen_state -> ('b, 's) gen_state -> + ('c, 's) gen_state -> ('d, 's) gen_state + val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> ('a, 's) gen_state -> ('b, 's) gen_state -> + ('c, 's) gen_state -> ('d, 's) gen_state -> ('e, 's) gen_state + + (*ensures that all generated values fulfill the predicate; loops if the predicate is never + satisfied by the generated values.*) + val filter : ('a -> bool) -> ('a, 's) gen_state -> ('a, 's) gen_state + val filter_bounded : int -> ('a -> bool) -> ('a, 's) gen_state -> ('a, 's) gen_state + + (*bernoulli random variable with parameter p \ [0,1]*) + val bernoulli : real -> bool gen + + (*random variable following a binomial distribution with parameters p \ [0,1] and n \ 0*) + val binom_dist : real -> int -> int gen + + (*range_int (x,y) r returns a value in [x;y]*) + val range_int : int * int -> int gen + + (*randomly generates one of the given values*) + val elements : 'a vector -> 'a gen + (*randomly uses one of the given generators*) + val one_of : 'a gen vector -> 'a gen + + (*randomly generates one of the given values*) + val elementsL : 'a list -> 'a gen + (*randomly uses one of the given generators*) + val one_ofL : 'a gen list -> 'a gen + + (*chooses one of the given generators with a weighted random distribution.*) + val one_ofW : (int * 'a gen) vector -> 'a gen + (*chooses one of the given values with a weighted random distribution.*) + val elementsW : (int * 'a) vector -> 'a gen + + (*chooses one of the given generators with a weighted random distribution.*) + val one_ofWL : (int * 'a gen) list -> 'a gen + (*chooses one of the given values with a weighted random distribution.*) + val elementsWL : (int * 'a) list -> 'a gen + + (*creates a vector of length as returned by the passed int generator*) + val vector : (int, 's) gen_state -> ('a, 's) gen_state -> ('a vector, 's) gen_state + + (*creates a list of length as returned by the passed int generator*) + val list : (int, 's) gen_state -> ('a, 's) gen_state -> ('a list, 's) gen_state + + (*generates elements until the passed (generator) predicate fails; + returns a list of all values that satisfied the predicate*) + val unfold_while : ('a -> (bool, 's) gen_state) -> ('a, 's) gen_state -> ('a list, 's) gen_state + (*generates a random permutation of the given list*) + val shuffle : 'a list -> 'a list gen + + (*generates SOME value if passed bool generator returns true and NONE otherwise*) + val option : (bool, 's) gen_state -> ('a, 's) gen_state -> ('a option, 's) gen_state + + (*seq gen init_state creates a sequence where gen takes a state and returns the next element and + an updated state. The sequence stops when the first NONE value is returned by the generator.*) + val seq : ('a option, 's * SpecCheck_Random.rand) gen_state -> 's -> ('a Seq.seq) gen + + (*creates a generator that returns all elements of the sequence in order*) + val of_seq : ('a option, 'a Seq.seq) gen_state + + val unit : (unit, 's) gen_state + val ref_gen : ('a, 's) gen_state -> ('a Unsynchronized.ref, 's) gen_state + + (*variant i g creates the ith variant of a given generator. It raises an error if i is negative.*) + val variant : (int, 'b) cogen + val cobool : (bool, 'b) cogen + val colist : ('a, 'b) cogen -> ('a list, 'b) cogen + val cooption : ('a, 'b) cogen -> ('a option, 'b) cogen + +end + +structure SpecCheck_Gen_Base : SPECCHECK_GEN_BASE = +struct + +open SpecCheck_Gen_Types + +val return = pair +fun join g = g #> (fn (g', r') => g' r') + +fun zip g1 g2 = + g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2))) +fun zip3 g1 g2 g3 = + zip g1 (zip g2 g3) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3)) +fun zip4 g1 g2 g3 g4 = + zip (zip g1 g2) (zip g3 g4) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4)) + +fun map f g = g #>> f +fun map2 f = map (uncurry f) oo zip +fun map3 f = map (fn (a,b,c) => f a b c) ooo zip3 +fun map4 f = map (fn (a,b,c,d) => f a b c d) oooo zip4 + +fun filter p gen r = + let fun loop (x, r) = if p x then (x, r) else loop (gen r) + in loop (gen r) end + +fun filter_bounded bound p gen r = + let fun loop 0 _ = raise Fail "Generator failed to satisfy predicate" + | loop n (x, r) = if p x then (x, r) else loop (n-1) (gen r) + in loop bound (gen r) end + +fun bernoulli p r = let val (x,r) = SpecCheck_Random.real_unit r in (x <= p, r) end + +fun binom_dist p n r = + let + fun binom_dist_unchecked _ 0 r = (0, r) + | binom_dist_unchecked p n r = + let fun int_of_bool b = if b then 1 else 0 + in + bernoulli p r + |>> int_of_bool + ||> binom_dist_unchecked p (n-1) + |> (fn (x,(acc,r)) => (acc + x, r)) + end + in if n < 0 then raise Domain else binom_dist_unchecked p n r end + +fun range_int (min, max) r = + if min > max + then raise Fail (SpecCheck_Util.spaces ["Range_Int:", string_of_int min, ">", string_of_int max]) + else + SpecCheck_Random.real_unit r + |>> (fn s => Int.min (min + Real.floor (s * Real.fromInt (max - min + 1)), max)) + +fun one_of v r = + let val (i, r) = range_int (0, Vector.length v - 1) r + in Vector.sub (v, i) r end + +local +datatype ('a,'b) either = Left of 'a | Right of 'b +in +fun one_ofW (v : (int * 'a gen) vector) r = + let + val weight_total = Vector.foldl (fn ((freq,_),acc) => freq + acc) 0 v + fun selectGen _ (_, Right gen) = Right gen + | selectGen rand ((weight, gen), Left acc) = + let val acc = acc + weight + in if acc < rand + then Left acc + else Right gen + end + val (threshhold, r) = range_int (1, weight_total) r + val gen = case Vector.foldl (selectGen threshhold) (Left 0) v of + Right gen => gen + | _ => raise Fail "Error in one_ofW - did you pass an empty vector or invalid frequencies?" + in gen r end +end + +fun elements v = one_of (Vector.map return v) +fun elementsW v = one_ofW (Vector.map (fn p => p ||> return) v) + +fun one_ofL l = one_of (Vector.fromList l) +fun one_ofWL l = one_ofW (Vector.fromList l) +fun elementsL l = elements (Vector.fromList l) +fun elementsWL l = elementsW (Vector.fromList l) + +fun list length_g g r = + let val (l, r) = length_g r + in fold_map (K g) (map_range I l) r end + +fun unfold_while bool_g_of_elem g r = + let + fun unfold_while_accum (xs, r) = + let + val (x, r) = g r + val (continue, r) = bool_g_of_elem x r + in + if continue + then unfold_while_accum (x::xs, r) + else (xs, r) + end + in unfold_while_accum ([], r) |>> rev end + +fun shuffle xs r = + let + val (ns, r) = list (return (length xs)) SpecCheck_Random.real_unit r + val real_ord = make_ord (op <=) + val xs = ListPair.zip (ns, xs) |> sort (real_ord o apply2 fst) |> List.map snd + in (xs, r) end + +fun vector length_g g = list length_g g #>> Vector.fromList + +fun option bool_g g r = + case bool_g r of + (false, r) => (NONE, r) + | (true, r) => map SOME g r + +fun seq gen xq r = + let + val (r1, r2) = SpecCheck_Random.split r + fun gen_next p () = case gen p of + (NONE, _) => NONE + | (SOME v, p) => SOME (v, Seq.make (gen_next p)) + in (Seq.make (gen_next (xq, r1)), r2) end + +fun of_seq xq = case Seq.pull xq of + SOME (x, xq) => (SOME x, xq) + | NONE => (NONE, Seq.empty) + +fun unit s = return () s + +fun ref_gen gen r = let val (value, r) = gen r + in (Unsynchronized.ref value, r) end + +fun variant i g r = + if i < 0 then raise Subscript + else + let + fun nth i r = + let val (r1, r2) = SpecCheck_Random.split r + in if i = 0 then r1 else nth (i-1) r2 end + in g (nth i r) end + +fun cobool false = variant 0 + | cobool true = variant 1 + +fun colist _ [] = variant 0 + | colist co (x::xs) = colist co xs o co x o variant 1 + +fun cooption _ NONE = variant 0 + | cooption co (SOME x) = co x o variant 1 + +end diff --git a/thys/SpecCheck/generators/gen_function.ML b/thys/SpecCheck/generators/gen_function.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_function.ML @@ -0,0 +1,41 @@ +(* Title: SpecCheck/generators/gen_function.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random generators for functions. +*) + +signature SPECCHECK_GEN_FUNCTION = sig + val function : ('a, 'b) SpecCheck_Gen_Types.cogen -> 'b SpecCheck_Gen_Types.gen -> + ('a -> 'b) SpecCheck_Gen_Types.gen + val function' : 'b SpecCheck_Gen_Types.gen -> (''a -> 'b) SpecCheck_Gen_Types.gen +end + +structure SpecCheck_Gen_Function : SPECCHECK_GEN_FUNCTION = +struct + +fun function cogen gen r = + let + val (r1, r2) = SpecCheck_Random.split r + fun g x = fst (cogen x gen r1) + in (g, r2) end + +fun function' gen r = + let + val (internal, external) = SpecCheck_Random.split r + val seed = Unsynchronized.ref internal + val table = Unsynchronized.ref [] + fun new_entry k = + let + val (new_val, new_seed) = gen (!seed) + val _ = seed := new_seed + val _ = table := AList.update (op =) (k, new_val) (!table) + in new_val end + in + (fn v1 => + case AList.lookup (op =) (!table) v1 of + NONE => new_entry v1 + | SOME v2 => v2, external) + end + +end diff --git a/thys/SpecCheck/generators/gen_int.ML b/thys/SpecCheck/generators/gen_int.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_int.ML @@ -0,0 +1,38 @@ +(* Title: SpecCheck/generators/gen_int.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random generators for ints. +*) + +signature SPECCHECK_GEN_INT = sig + + (*pos m generates an integer in [1, m]*) + val pos : int -> int SpecCheck_Gen_Types.gen + (*neg m generates an integer in [m, 1]*) + val neg : int -> int SpecCheck_Gen_Types.gen + (*nonneg m generates an integer in [0, m]*) + val nonneg : int -> int SpecCheck_Gen_Types.gen + (*nonpos m generates an integer in [m, 0]*) + val nonpos : int -> int SpecCheck_Gen_Types.gen + + val coint : (int, 'b) SpecCheck_Gen_Types.cogen + +end + +structure SpecCheck_Gen_Int : SPECCHECK_GEN_INT = +struct + +open SpecCheck_Gen_Base + +fun pos m = range_int (1, m) +fun neg m = range_int (m, ~1) +fun nonneg m = range_int (0, m) +fun nonpos m = range_int (m, 0) + +fun coint n = + if n = 0 then variant 0 + else if n < 0 then coint (~n) o variant 1 + else coint (n div 2) o variant 2 + +end diff --git a/thys/SpecCheck/generators/gen_real.ML b/thys/SpecCheck/generators/gen_real.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_real.ML @@ -0,0 +1,65 @@ +(* Title: SpecCheck/generators/gen_real.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random generators for reals. +*) + +signature SPECCHECK_GEN_REAL = sig + + (*range_real (x,y) r returns a value in [x, y]*) + val range_real : real * real -> real SpecCheck_Gen_Types.gen + + val real : real SpecCheck_Gen_Types.gen + + val real_pos : real SpecCheck_Gen_Types.gen + val real_neg : real SpecCheck_Gen_Types.gen + + val real_nonneg : real SpecCheck_Gen_Types.gen + val real_nonpos : real SpecCheck_Gen_Types.gen + + val real_finite : real SpecCheck_Gen_Types.gen +end + +structure SpecCheck_Gen_Real : SPECCHECK_GEN_REAL = +struct + +open SpecCheck_Gen_Base +open SpecCheck_Gen_Text + +fun range_real (min, max) r = + if min > max + then + raise Fail (SpecCheck_Util.spaces ["Range_Real:", string_of_real min, ">", string_of_real max]) + else SpecCheck_Random.real_unit r |>> (fn s => min + (s * max - s * min)) + +val digits = string (range_int (1, Real.precision)) (range_char (#"0", #"9")) + +val {exp=minExp,...} = Real.toManExp Real.minPos +val {exp=maxExp,...} = Real.toManExp Real.posInf + +val ratio = 99 + +fun mk r = + let + val (a, r) = digits r + val (b, r) = digits r + val (e, r) = range_int (minExp div 4, maxExp div 4) r + val x = String.concat [a, ".", b, "E", Int.toString e] + in + (the (Real.fromString x), r) + end + +val real_pos = one_ofWL ((ratio, mk) :: + List.map ((pair 1) o return) [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos]) + +val real_neg = map Real.~ real_pos + +val real_nonneg = one_ofWL [(1, return 0.0), (ratio, real_pos)] +val real_nonpos = one_ofWL [(1, return 0.0), (ratio, real_neg)] + +val real = one_ofL [real_nonneg, real_nonpos] + +val real_finite = filter Real.isFinite real + +end diff --git a/thys/SpecCheck/generators/gen_term.ML b/thys/SpecCheck/generators/gen_term.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_term.ML @@ -0,0 +1,269 @@ +(* Title: SpecCheck/generators/gen_term.ML + Author: Sebastian Willenbrink and Kevin Kappelmann TU Muenchen + +Generators for terms and types. +*) +signature SPECCHECK_GEN_TERM = sig + (* sort generators *) + + (*first parameter determines the number of classes to pick*) + val sort : (int, 's) SpecCheck_Gen_Types.gen_state -> (class, 's) SpecCheck_Gen_Types.gen_state + -> (sort, 's) SpecCheck_Gen_Types.gen_state + val dummyS : (sort, 's) SpecCheck_Gen_Types.gen_state + + (* name generators *) + (*parameters: a base name and a generator for the number of variants to choose from based on then + passed base name*) + val basic_name : string -> int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen + + val indexname : (string, 's) SpecCheck_Gen_Types.gen_state -> + (int, 's) SpecCheck_Gen_Types.gen_state -> (indexname, 's) SpecCheck_Gen_Types.gen_state + + (*a variant with base name "k"*) + val type_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen + + (*creates a free type variable name from a passed basic name generator*) + val tfree_name : (string, 's) SpecCheck_Gen_Types.gen_state -> + (string, 's) SpecCheck_Gen_Types.gen_state + (*chooses a variant with base name "'a"*) + val tfree_name' : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen + + (*creates a type variable name from a passed basic name (e.g. "a") generator*) + val tvar_name : (indexname, 's) SpecCheck_Gen_Types.gen_state -> + (indexname, 's) SpecCheck_Gen_Types.gen_state + (*chooses a variant with base name "'a"*) + val tvar_name' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + indexname SpecCheck_Gen_Types.gen + + (*chooses a variant with base name "c"*) + val const_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen + (*chooses a variant with base name "f"*) + val free_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen + (*chooses a variant with base name "v*) + val var_name : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + indexname SpecCheck_Gen_Types.gen + + (* typ generators *) + + val tfree : (string, 's) SpecCheck_Gen_Types.gen_state -> + (sort, 's) SpecCheck_Gen_Types.gen_state -> (typ, 's) SpecCheck_Gen_Types.gen_state + (*uses tfree_name' and dummyS to create a free type variable*) + val tfree' : int SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen + + val tvar : (indexname, 's) SpecCheck_Gen_Types.gen_state -> + (sort, 's) SpecCheck_Gen_Types.gen_state -> (typ, 's) SpecCheck_Gen_Types.gen_state + (*uses tvar' and dummyS to create a type variable*) + val tvar' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + typ SpecCheck_Gen_Types.gen + + (*atyp tfree_gen tvar_gen (weight_tfree, weight_tvar)*) + val atyp : typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int) -> + typ SpecCheck_Gen_Types.gen + (*uses tfree' and tvar' to create an atomic type*) + val atyp' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> (int * int) -> + typ SpecCheck_Gen_Types.gen + + (*type' type_name_gen arity_gen tfree_gen tvar_gen (weight_type, weight_tfree, weight_tvar)*) + val type' : string SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> + (int * int * int) -> typ SpecCheck_Gen_Types.gen + (*uses type_name to generate a type*) + val type'' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int * int) -> + typ SpecCheck_Gen_Types.gen + + (*typ type_gen tfree_gen tvar_gen (wtype, wtfree, wtvar)*) + val typ : typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> + typ SpecCheck_Gen_Types.gen -> (int * int * int) -> typ SpecCheck_Gen_Types.gen + (*uses type'' for its type generator*) + val typ' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int * int) -> + typ SpecCheck_Gen_Types.gen + (*uses typ' with tfree' and tvar' parameters*) + val typ'' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + int SpecCheck_Gen_Types.gen -> (int * int * int) -> typ SpecCheck_Gen_Types.gen + + val dummyT : (typ, 's) SpecCheck_Gen_Types.gen_state + + (* term generators *) + + val const : (string, 's) SpecCheck_Gen_Types.gen_state -> + (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state + (*uses const_name and dummyT to create a constant*) + val const' : int SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen + + val free : (string, 's) SpecCheck_Gen_Types.gen_state -> + (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state + (*uses free_name and dummyT to create a free variable*) + val free' : int SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen + + val var : (indexname, 's) SpecCheck_Gen_Types.gen_state -> + (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state + (*uses var_name and dummyT to create a variable*) + val var' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + term SpecCheck_Gen_Types.gen + + val bound : (int, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state + + (*aterm const_gen free_gen var_gen bound_gen + (weight_const, weight_free, weight_var, weight_bound*) + val aterm : term SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen -> + term SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen -> (int * int * int * int) -> + term SpecCheck_Gen_Types.gen + (*uses const', free', and var' to create an atomic term*) + val aterm' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> + (int * int * int * int) -> term SpecCheck_Gen_Types.gen + + (*term_tree f init_state - where "f height index state" returns "((term, num_args), new_state)" - + generates a term by applying f to every node and expanding that node depending + on num_args returned by f. + Traversal order: function \ first argument \ ... \ last argument + The tree is returned in its applicative term form: (...((root $ child1) $ child2) .. $ childn). + + Arguments of f: + - height describes the distance from the root (starts at 0) + - index describes the global index in that tree layer, left to right (0 \ index < width) + - state is passed along according to above traversal order + + Return value of f: + - term is the term whose arguments will be generated next. + - num_args specifies how many arguments should be passed to the term. + - new_state is passed along according to the traversal above.*) + val term_tree : (int -> int -> (term * int, 's) SpecCheck_Gen_Types.gen_state) -> + (term, 's) SpecCheck_Gen_Types.gen_state + + (*In contrast to term_tree, f now takes a (term, index_of_argument) list which specifies the path + from the root to the current node.*) + val term_tree_path : ((term * int) list -> (term * int, 's) SpecCheck_Gen_Types.gen_state) -> + (term, 's) SpecCheck_Gen_Types.gen_state + +end + +structure SpecCheck_Gen_Term : SPECCHECK_GEN_TERM = +struct + +structure Gen = SpecCheck_Gen_Base + +fun sort size_gen = Gen.list size_gen +fun dummyS s = Gen.return Term.dummyS s + +fun basic_name name num_variants_gen = + num_variants_gen + #>> (fn i => name ^ "_" ^ string_of_int i) + +fun indexname basic_name_gen = Gen.zip basic_name_gen + +fun type_name num_variants_gen = basic_name "k" num_variants_gen + +fun tfree_name basic_name_gen = Gen.map (curry op^"'") basic_name_gen +fun tfree_name' num_variants_gen = tfree_name (basic_name "a" num_variants_gen) + +fun tvar_name indexname_gen = Gen.map (curry op^"'" |> apfst) indexname_gen +fun tvar_name' num_variants_gen = + tvar_name o indexname (basic_name "a" num_variants_gen) + +fun const_name num_variants_gen = basic_name "c" num_variants_gen +fun free_name num_variants_gen = basic_name "v" num_variants_gen +fun var_name num_variants_gen = indexname (free_name num_variants_gen) + +(* types *) + +fun tfree name_gen = Gen.map TFree o Gen.zip name_gen +fun tfree' num_variants_gen = + tfree_name' num_variants_gen + |> (fn name_gen => tfree name_gen dummyS) + +fun tvar idx_gen = Gen.map TVar o Gen.zip idx_gen +fun tvar' num_variants_gen = + tvar_name' num_variants_gen + #> (fn name_gen => tvar name_gen dummyS) + +fun atyp tfree_gen tvar_gen (wtfree, wtvar) = + Gen.one_ofWL [(wtfree, tfree_gen), (wtvar, tvar_gen)] +fun atyp' num_variants_gen = atyp (tfree' num_variants_gen) o tvar' num_variants_gen + +fun type' type_name_gen arity_gen tfree_gen tvar_gen (weights as (wtype, wtfree, wtvar)) = + (*eta-abstract to avoid strict evaluation, causing an infinite loop*) + [(wtype, fn r => type' type_name_gen arity_gen tfree_gen tvar_gen weights r), + (wtfree, fn r => tfree_gen r), (wtvar, fn r => tvar_gen r)] + |> Gen.one_ofWL + |> Gen.list arity_gen + |> Gen.zip type_name_gen + |> Gen.map Type + +fun type'' num_variants_gen = type_name num_variants_gen |> type' + +fun typ type_gen tfree_gen tvar_gen (wtype, wtfree, wtvar) = + Gen.one_ofWL [(wtype, type_gen), (wtfree, tfree_gen), (wtvar, tvar_gen)] +fun typ' num_variants_gen arity_gen tfree_gen tvar_gen weights = + typ (type'' num_variants_gen arity_gen tfree_gen tvar_gen weights) tfree_gen tvar_gen weights +fun typ'' num_variants_gen arity_gen = + typ' num_variants_gen arity_gen (tfree' num_variants_gen) o tvar' num_variants_gen + +fun dummyT s = Gen.return Term.dummyT s + +(* terms *) + +fun const name_gen = Gen.map Const o Gen.zip name_gen +fun const' num_variants_gen = + const_name num_variants_gen + |> (fn name_gen => const name_gen dummyT) + +fun free name_gen = Gen.map Free o Gen.zip name_gen +fun free' num_variants_gen = + free_name num_variants_gen + |> (fn name_gen => free name_gen dummyT) + +fun var idx_gen = Gen.map Var o Gen.zip idx_gen +fun var' num_variants_gen = + var_name num_variants_gen + #> (fn name_gen => var name_gen dummyT) + +fun bound int_gen = Gen.map Bound int_gen + +fun aterm const_gen free_gen var_gen bound_gen (wconst, wfree, wvar, wbound) = + Gen.one_ofWL [(wconst, const_gen), (wfree, free_gen), (wvar, var_gen), (wbound, bound_gen)] +fun aterm' num_variants_gen index_gen = + aterm (const' num_variants_gen) (free' num_variants_gen) (var' num_variants_gen index_gen) + (bound num_variants_gen) + +(*nth_map has no default*) +fun nth_map_default 0 f _ (x::xs) = f x :: xs + | nth_map_default 0 f d [] = [f d] + | nth_map_default n f d [] = replicate (n-1) d @ [f d] + | nth_map_default n f d (x::xs) = x :: nth_map_default (n-1) f d xs + +fun term_tree term_gen state = + let + fun nth_incr n = nth_map_default n (curry op+ 1) (~1) + fun build_tree indices height state = + let + (*indices stores the number of nodes visited so far at each height*) + val indices = nth_incr height indices + val index = nth indices height + (*generate the term for the current node*) + val ((term, num_args), state) = term_gen height index state + fun build_child (children, indices, state) = + build_tree indices (height + 1) state + |> (fn (child, indices, state) => (child :: children, indices, state)) + (*generate the subtrees for each argument*) + val (children, indices, state) = fold (K build_child) (1 upto num_args) ([], indices, state) + in (Term.list_comb (term, (rev children)), indices, state) end + in + build_tree [] 0 state + |> (fn (term, _, state) => (term, state)) + end + +fun term_tree_path f init_state = + let + fun build_tree path state = + let + val ((term, num_args), state) = f path state + fun build_children i (args, state) = + build_tree ((term, i) :: path) state + |>> (fn x => x :: args) + val (children, state) = fold build_children (0 upto num_args-1) ([], state) + in (Term.list_comb (term, (rev children)), state) end + in build_tree [] init_state end + +end diff --git a/thys/SpecCheck/generators/gen_text.ML b/thys/SpecCheck/generators/gen_text.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_text.ML @@ -0,0 +1,70 @@ +(* Title: SpecCheck/generators/gen_text.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random generators for chars and strings. +*) + +signature SPECCHECK_GEN_TEXT = sig + + val range_char : char * char -> char SpecCheck_Gen_Types.gen + val char : char SpecCheck_Gen_Types.gen + + val char_of : string -> char SpecCheck_Gen_Types.gen + + val string : int SpecCheck_Gen_Types.gen -> char SpecCheck_Gen_Types.gen -> + string SpecCheck_Gen_Types.gen + + val substring : string SpecCheck_Gen_Types.gen -> substring SpecCheck_Gen_Types.gen + + val cochar : (char, 'b) SpecCheck_Gen_Types.cogen + val costring : (string, 'b) SpecCheck_Gen_Types.cogen + val cosubstring : (substring, 'b) SpecCheck_Gen_Types.cogen + + val digit : char SpecCheck_Gen_Types.gen + val lowercase_letter : char SpecCheck_Gen_Types.gen + val uppercase_letter : char SpecCheck_Gen_Types.gen + val letter : char SpecCheck_Gen_Types.gen +end + +structure SpecCheck_Gen_Text : SPECCHECK_GEN_TEXT = +struct + +open SpecCheck_Gen_Base + +type char = Char.char +type string = String.string +type substring = Substring.substring + +fun range_char (lo, hi) = map Char.chr (range_int (Char.ord lo, Char.ord hi)) +val char = range_char (Char.minChar, Char.maxChar) + +fun char_of s = + one_of (Vector.tabulate (String.size s, fn i => return (String.sub (s, i)))) + +fun string length_g g = list length_g g #>> CharVector.fromList + +fun substring gen r = + let + val (s, r) = gen r + val (i, r) = range_int (0, String.size s) r + val (j, r) = range_int (0, String.size s - i) r + in + (Substring.substring (s, i, j), r) + end + +fun cochar c = + if Char.ord c = 0 then variant 0 + else cochar (Char.chr (Char.ord c div 2)) o variant 1 + +fun cosubstring s = colist cochar (Substring.explode s) + +fun costring s = cosubstring (Substring.full s) + +val digit = range_char (#"0", #"9") + +val lowercase_letter = range_char (#"a", #"z") +val uppercase_letter = range_char (#"A", #"Z") +val letter = one_ofL [lowercase_letter, uppercase_letter] + +end diff --git a/thys/SpecCheck/generators/gen_types.ML b/thys/SpecCheck/generators/gen_types.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/generators/gen_types.ML @@ -0,0 +1,34 @@ +(* Title: SpecCheck/generators/gen_types.ML + Author: Kevin Kappelmann + +Shared type definitions for SpecCheck generators. +*) + +signature SPECCHECK_GEN_TYPES = +sig + + (*consumes a state and returns a new state along with a generated value*) + type ('a, 's) gen_state = 's -> 'a * 's + (*consumes a random seed and returns an unused one along with a generated value*) + type 'a gen = ('a, SpecCheck_Random.rand) gen_state + + (*a cogenerator produces new generators depending on an input element and an existing generator.*) + type ('a, 'b, 's) cogen_state = 'a -> ('b, 's) gen_state -> ('b, 's) gen_state + + (*a cogenerator produces new generators depending on an input element and an existing generator.*) + type ('a, 'b) cogen = ('a, 'b, SpecCheck_Random.rand) cogen_state + +end + +structure SpecCheck_Gen_Types : SPECCHECK_GEN_TYPES = +struct + +type ('a, 's) gen_state = 's -> 'a * 's + +type 'a gen = ('a, SpecCheck_Random.rand) gen_state + +type ('a, 'b, 's) cogen_state = 'a -> ('b, 's) gen_state -> ('b, 's) gen_state + +type ('a, 'b) cogen = ('a, 'b, SpecCheck_Random.rand) cogen_state + +end diff --git a/thys/SpecCheck/lecker.ML b/thys/SpecCheck/lecker.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/lecker.ML @@ -0,0 +1,23 @@ +(* Title: SpecCheck/lecker.ML + Author: Kevin Kappelmann + +Testing framework that lets you combine SpecCheck tests into test suites. + +TODO: this file can be largely extended to become a pendant of Haskell's tasty: +https://hackage.haskell.org/package/tasty +*) + +signature LECKER = +sig + (*the first parameter to test_group will usually be a context*) + val test_group : 'a -> 's -> ('a -> 's -> 's) list -> 's +end + +structure Lecker : LECKER = +struct + +fun test_group _ s [] = s + | test_group fixed_param s (t::ts) = + fold (fn t => (Pretty.writeln (Pretty.para ""); t fixed_param)) ts (t fixed_param s) + +end diff --git a/thys/SpecCheck/output_styles/SpecCheck_Output_Style.thy b/thys/SpecCheck/output_styles/SpecCheck_Output_Style.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/output_styles/SpecCheck_Output_Style.thy @@ -0,0 +1,20 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Output Styles\ +theory SpecCheck_Output_Style +imports + SpecCheck_Base + SpecCheck_Show +begin + + +paragraph \Summary\ +text \Output styles for SpecCheck take the result of a test run and process it accordingly, +e.g. by printing it or storing it to a file.\ + + +ML_file \output_style_types.ML\ +ML_file \output_style_perl.ML\ +ML_file \output_style_custom.ML\ +ML_file \output_style.ML\ + +end diff --git a/thys/SpecCheck/output_styles/output_style.ML b/thys/SpecCheck/output_styles/output_style.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/output_styles/output_style.ML @@ -0,0 +1,20 @@ +(* Title: SpecCheck/output_styles/output_style.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Output styles for presenting SpecCheck results. +*) + +signature SPECCHECK_DEFAULT_OUTPUT_STYLE = +sig + include SPECCHECK_OUTPUT_STYLE_TYPES + val default : 'a output_style +end + +structure SpecCheck_Default_Output_Style : SPECCHECK_DEFAULT_OUTPUT_STYLE = +struct + +open SpecCheck_Output_Style_Types +val default = SpecCheck_Output_Style_Custom.style + +end diff --git a/thys/SpecCheck/output_styles/output_style_custom.ML b/thys/SpecCheck/output_styles/output_style_custom.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/output_styles/output_style_custom.ML @@ -0,0 +1,83 @@ +(* Title: SpecCheck/output_style/output_style_custom.ML + Author: Lukas Bulwahn, Nicolai Schaffroth, Kevin Kappelmann TU Muenchen + Author: Christopher League + +Custom-made, QuickCheck-inspired output style for SpecCheck. +*) + +structure SpecCheck_Output_Style_Custom : SPECCHECK_OUTPUT_STYLE = +struct + +open SpecCheck_Base + +fun print_success stats = + let + val num_success_tests = string_of_int (#num_success_tests stats) + val num_discarded_tests = #num_discarded_tests stats + val discarded_str = + if num_discarded_tests = 0 + then "." + else SpecCheck_Util.spaces [";", string_of_int num_discarded_tests, "discarded."] + in + implode ["OK, passed ", num_success_tests, " tests", discarded_str] + |> writeln + end + +fun print_gave_up stats = + let + val num_success_tests = string_of_int (#num_success_tests stats) + val num_discarded_tests = string_of_int (#num_discarded_tests stats) + in + SpecCheck_Util.spaces ["Gave up! Passed only", num_success_tests, "test(s);", num_discarded_tests, + "discarded test(s)."] + |> warning + end + +fun print_failure_data ctxt show_opt failure_data = + case #the_exception failure_data of + SOME exn => + cat_lines ["Exception during test run:", exnMessage exn] + |> warning + | NONE => case show_opt of + NONE => () + | SOME show => + let + val sort_counterexamples = Config.get ctxt SpecCheck_Configuration.sort_counterexamples + val maybe_sort = if sort_counterexamples then sort (int_ord o apply2 size) else I + val counterexamples = + #counterexamples failure_data + |> map (Pretty.string_of o show) + |> maybe_sort + in fold (fn x => fn _ => warning x) counterexamples () end + +fun print_failure ctxt show_opt (stats, failure_data) = + ((SpecCheck_Util.spaces ["Failed! Falsified (after", string_of_int (num_tests stats), "test(s) and ", + string_of_int (num_shrinks stats), "shrink(s)):"] |> warning); + print_failure_data ctxt show_opt failure_data) + +fun print_stats ctxt stats total_time = + let + val show_stats = Config.get ctxt SpecCheck_Configuration.show_stats + (*the time spent in the test function in relation to the total time spent; + the latter includes generating test cases and overhead from the framework*) + fun show_time {elapsed, ...} = + implode ["Time: ", Time.toString elapsed, "s (run) / ", Time.toString (#elapsed total_time), + "s (total)"] + in + if not show_stats + then () + else writeln (show_time (#timing stats)) + end + +fun style show_opt ctxt name total_time result = + let val stats = stats_of_result result + in + writeln (SpecCheck_Util.spaces ["Testing:", name]); + (case result of + Success _ => print_success stats + | Gave_Up _ => print_gave_up stats + | Failure data => print_failure ctxt show_opt data); + print_stats ctxt stats total_time + end + +end diff --git a/thys/SpecCheck/output_styles/output_style_perl.ML b/thys/SpecCheck/output_styles/output_style_perl.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/output_styles/output_style_perl.ML @@ -0,0 +1,54 @@ +(* Title: SpecCheck/output_styles/output_style_perl.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Perl output styles for SpecCheck. +*) + +structure SpecCheck_Output_Style_Perl : SPECCHECK_OUTPUT_STYLE = +struct + +open SpecCheck_Configuration +open SpecCheck_Base + +fun style show_opt ctxt name timing result = + let + val sort_counterexamples = Config.get ctxt sort_counterexamples + val maybe_sort = if sort_counterexamples then sort (int_ord o apply2 size) else I + + val stats = stats_of_result result + val num_failed_tests = #num_failed_tests stats + + fun code (Success _) = "ok" + | code (Gave_Up _) = "Gave up!" + | code (Failure _) = "FAILED" + + fun ratio stats = + let + val num_success_tests = #num_success_tests stats + in + if num_failed_tests = 0 + then implode ["(", string_of_int num_success_tests, " passed)"] + else implode ["(", string_of_int num_success_tests, "/", + string_of_int (num_success_tests + num_failed_tests), " passed)"] + end + + val result_string = name ^ ".\n" ^ code result ^ " " ^ ratio stats + + fun show_counterexamples counterexamples = + case show_opt of + SOME show => + (case maybe_sort (map (Pretty.string_of o show) counterexamples) of + [] => () + | es => (warning "Counterexamples:"; fold (fn x => fn _ => warning x) es ())) + | NONE => () + + in + case result of + Success _ => writeln result_string + | Gave_Up _ => warning result_string + | Failure (_, failure_data) => + (warning result_string; show_counterexamples (#counterexamples failure_data)) + end + +end diff --git a/thys/SpecCheck/output_styles/output_style_types.ML b/thys/SpecCheck/output_styles/output_style_types.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/output_styles/output_style_types.ML @@ -0,0 +1,24 @@ +(* Title: SpecCheck/output_styles/output_style_types.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Shared types for SpecCheck output styles. +*) +signature SPECCHECK_OUTPUT_STYLE_TYPES = +sig + type 'a output_style = 'a SpecCheck_Show.show option -> Proof.context -> string -> + Timing.timing -> 'a SpecCheck_Base.result -> unit +end + +structure SpecCheck_Output_Style_Types : SPECCHECK_OUTPUT_STYLE_TYPES = +struct + +type 'a output_style = 'a SpecCheck_Show.show option -> Proof.context -> string -> Timing.timing -> + 'a SpecCheck_Base.result -> unit + +end + +signature SPECCHECK_OUTPUT_STYLE = +sig + val style : 'a SpecCheck_Output_Style_Types.output_style +end diff --git a/thys/SpecCheck/property.ML b/thys/SpecCheck/property.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/property.ML @@ -0,0 +1,46 @@ +(* Title: SpecCheck/property.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +The base module of testable properties. +A property is the type of values that SpecCheck knows how to test. +Properties not only test whether a given predicate holds, but, for example, can also have +preconditions. +*) + +signature SPECCHECK_PROPERTY = +sig + + type 'a pred = 'a -> bool + (*the type of values testable by SpecCheck*) + type 'a prop + (*transforms a predicate into a testable property*) + val prop : 'a pred -> 'a prop + (*implication for properties: if the first argument evaluates to false, the test case is + discarded*) + val implies : 'a pred -> 'a prop -> 'a prop + (*convenient notation for `implies` working on predicates*) + val ==> : 'a pred * 'a pred -> 'a prop + +end + +structure SpecCheck_Property : SPECCHECK_PROPERTY = +struct + +type 'a pred = 'a -> bool +type 'a prop = 'a -> SpecCheck_Base.result_single + +fun apply f x = SpecCheck_Base.Result (f x) + (*testcode may throw arbitrary exceptions; interrupts must not be caught!*) + handle exn => if Exn.is_interrupt exn then Exn.reraise exn else SpecCheck_Base.Exception exn + +fun prop f x = apply f x + +fun implies cond prop x = + if cond x + then prop x + else SpecCheck_Base.Discard + +fun ==> (p1, p2) = implies p1 (prop p2) + +end diff --git a/thys/SpecCheck/random.ML b/thys/SpecCheck/random.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/random.ML @@ -0,0 +1,61 @@ +(* Title: SpecCheck/random.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +A Lehmer random number generator: +https://en.wikipedia.org/wiki/Lehmer_random_number_generator +We use int to avoid any float imprecision problems (and the seed is an int anyway). +The parameters "a" and "m" are selected according to the recommendation in above article; +they are an an improved version of the so-called "minimal standard" (MINSTD) generator. + +This file only contains those functions that rely on the internal integer representation of rand. +*) + +signature SPECCHECK_RANDOM = +sig + type rand + (*creates a new random seed*) + val new : unit -> rand + (*creates a new random seed from a given one*) + val next : rand -> rand + (*use this function for reproducible randomness; inputs \ 0 are mapped to 1*) + val deterministic_seed : int -> rand + + (*returns a real in the unit interval [0;1]; theoretically, with 2^31-2 equidistant discrete + values*) + val real_unit : rand -> real * rand + + (*splits a seed into two new independent seeds*) + val split : rand -> rand * rand +end + +structure SpecCheck_Random : SPECCHECK_RANDOM = +struct + +type rand = int + +val a = 48271 +val m = 2147483647 (* 2^31 - 1 *) + +fun next seed = (seed * a) mod m + +(*TODO: Time is not sufficiently random when polled rapidly!*) +fun new () = + Time.now () + |> Time.toMicroseconds + |> (fn x => Int.max (1, x mod m)) (*The seed must be within [1;m)*) + |> next + +fun deterministic_seed r = Int.max (1, r mod m) + +fun real_unit r = ((Real.fromInt (r - 1)) / (Real.fromInt (m - 2)), next r) + +(*TODO: In theory, the current implementation could return two seeds directly adjacent in the +sequence of the pseudorandom number generator. Practically, however, it should be good enough.*) +fun split r = + let + val r0 = next r + val r1 = r - r0 + in (next r0, next r1) end + +end diff --git a/thys/SpecCheck/show/SpecCheck_Show.thy b/thys/SpecCheck/show/SpecCheck_Show.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/show/SpecCheck_Show.thy @@ -0,0 +1,15 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Show\ +theory SpecCheck_Show +imports Pure +begin + +paragraph \Summary\ +text \Show functions (pretty-printers) for SpecCheck take a value and return a @{ML_type Pretty.T} +representation of the value. Refer to @{file "show_base.ML"} for some basic examples.\ + +ML_file \show_types.ML\ +ML_file \show_base.ML\ +ML_file \show.ML\ + +end diff --git a/thys/SpecCheck/show/show.ML b/thys/SpecCheck/show/show.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/show/show.ML @@ -0,0 +1,9 @@ +(* Title: SpecCheck/show/show.ML + Author: Kevin Kappelmann, TU Muenchen + +Structure containing all show functions. +*) +structure SpecCheck_Show = +struct +open SpecCheck_Show_Base +end diff --git a/thys/SpecCheck/show/show_base.ML b/thys/SpecCheck/show/show_base.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/show/show_base.ML @@ -0,0 +1,47 @@ +(* Title: SpecCheck/show/show_base.ML + Author: Kevin Kappelmann + +Basic utility functions to create and combine show functions. +*) + +signature SPECCHECK_SHOW_BASE = +sig + include SPECCHECK_SHOW_TYPES + + val none : 'a show + val char : char show + val string : string show + val int : int show + val real : real show + val bool : bool show + val list : 'a show -> ('a list) show + val option : 'a show -> ('a option) show + + val zip : 'a show -> 'b show -> ('a * 'b) show + val zip3 : 'a show -> 'b show -> 'c show -> ('a * 'b * 'c) show + val zip4 : 'a show -> 'b show -> 'c show -> 'd show -> ('a * 'b * 'c * 'd) show + +end + +structure SpecCheck_Show_Base : SPECCHECK_SHOW_BASE = +struct + +open SpecCheck_Show_Types + +fun none _ = Pretty.str "" +val char = Pretty.enclose "'" "'" o single o Pretty.str o Char.toString +val string = Pretty.quote o Pretty.str +val int = Pretty.str o string_of_int +val real = Pretty.str o string_of_real +fun bool b = Pretty.str (if b then "true" else "false") +fun list show = Pretty.list "[" "]" o map show +fun option _ NONE = Pretty.str "NONE" + | option show (SOME v) = Pretty.block [Pretty.str "SOME ", show v] + +fun pretty_tuple ps = ps |> Pretty.commas |> Pretty.enclose "(" ")" + +fun zip showA showB (a, b) = pretty_tuple [showA a, showB b] +fun zip3 showA showB showC (a, b, c) = pretty_tuple [showA a, showB b, showC c] +fun zip4 showA showB showC showD (a, b, c, d) = pretty_tuple [showA a, showB b, showC c, showD d] + +end diff --git a/thys/SpecCheck/show/show_types.ML b/thys/SpecCheck/show/show_types.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/show/show_types.ML @@ -0,0 +1,17 @@ +(* Title: SpecCheck/show/show_types.ML + Author: Kevin Kappelmann + +Shared type definitions for SpecCheck showable types. +*) + +signature SPECCHECK_SHOW_TYPES = +sig + type 'a show = 'a -> Pretty.T +end + +structure SpecCheck_Show_Types : SPECCHECK_SHOW_TYPES = +struct + +type 'a show = 'a -> Pretty.T + +end diff --git a/thys/SpecCheck/shrink/SpecCheck_Shrink.thy b/thys/SpecCheck/shrink/SpecCheck_Shrink.thy new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/shrink/SpecCheck_Shrink.thy @@ -0,0 +1,15 @@ +\<^marker>\creator "Kevin Kappelmann"\ +section \Shrinkers\ +theory SpecCheck_Shrink +imports SpecCheck_Generators +begin + +paragraph \Summary\ +text \Shrinkers for SpecCheck take a value and return a sequence of smaller values derived from it. +Refer to @{file "shrink_base.ML"} for some basic examples.\ + +ML_file \shrink_types.ML\ +ML_file \shrink_base.ML\ +ML_file \shrink.ML\ + +end diff --git a/thys/SpecCheck/shrink/shrink.ML b/thys/SpecCheck/shrink/shrink.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/shrink/shrink.ML @@ -0,0 +1,11 @@ +(* Title: SpecCheck/shrink/shrink.ML + Author: Kevin Kappelmann, TU Muenchen + +Structure containing all shrink functions. +*) +structure SpecCheck_Shrink = +struct + +open SpecCheck_Shrink_Base + +end diff --git a/thys/SpecCheck/shrink/shrink_base.ML b/thys/SpecCheck/shrink/shrink_base.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/shrink/shrink_base.ML @@ -0,0 +1,89 @@ +(* Title: SpecCheck/shrink/shrink_base.ML + Author: Kevin Kappelmann + +Basic utility functions to create and combine shrink functions. +*) + +signature SPECCHECK_SHRINK_BASE = +sig + include SPECCHECK_SHRINK_TYPES + + val none : 'a shrink + + val product : 'a shrink -> 'b shrink -> ('a * 'b) shrink + val product3 : 'a shrink -> 'b shrink -> 'c shrink -> ('a * 'b * 'c) shrink + val product4 : 'a shrink -> 'b shrink -> 'c shrink -> 'd shrink -> ('a * 'b * 'c * 'd) shrink + + val int : int shrink + + val list : 'a shrink -> ('a list shrink) + val list' : ('a list) shrink + + val term : term shrink + +end + +structure SpecCheck_Shrink_Base : SPECCHECK_SHRINK_BASE = +struct +open SpecCheck_Shrink_Types + +fun none _ = Seq.empty + +fun product_seq xq yq (x, y) = + let + val yqy = Seq.append yq (Seq.single y) + val zq1 = Seq.maps (fn x => Seq.map (pair x) yqy) xq + val zq2 = Seq.map (pair x) yq + in Seq.append zq1 zq2 end + +fun product shrinkA shrinkB (a, b) = product_seq (shrinkA a) (shrinkB b) (a, b) + +fun product3 shrinkA shrinkB shrinkC (a, b, c) = + product shrinkA shrinkB (a, b) + |> (fn abq => product_seq abq (shrinkC c) ((a,b),c)) + |> Seq.map (fn ((a,b),c) => (a,b,c)) + +fun product4 shrinkA shrinkB shrinkC shrinkD (a, b, c, d) = + product3 shrinkA shrinkB shrinkC (a, b, c) + |> (fn abcq => product_seq abcq (shrinkD d) ((a,b,c),d)) + |> Seq.map (fn ((a,b,c),d) => (a,b,c,d)) + +(*bit-shift right until it hits zero (some special care needs to be taken for negative numbers*) +fun int 0 = Seq.empty + | int i = + let + val absi = abs i + val signi = Int.sign i + fun seq 0w0 () = NONE + | seq w () = + let + val next_value = signi * IntInf.~>> (absi, w) + val next_word = Word.- (w, 0w1) + in SOME (next_value, Seq.make (seq next_word)) end + val w = Word.fromInt (IntInf.log2 (abs i)) + in Seq.cons 0 (Seq.make (seq w)) end + +fun list _ [] = Seq.single [] + | list elem_shrink [x] = Seq.cons [] (Seq.map single (elem_shrink x)) + | list elem_shrink (x::xs) = + let + val elems = Seq.append (elem_shrink x) (Seq.single x) + val seq = Seq.maps (fn xs => Seq.map (fn x => x :: xs) elems) (list elem_shrink xs) + in Seq.cons [] seq end + +fun list' xs = list none xs + +fun term (t1 $ t2) = + let + val s1 = Seq.append (term t1) (Seq.single t1) + val s2 = Seq.append (term t2) (Seq.single t2) + val s3 = Seq.map (op$) (product term term (t1, t2)) + in Seq.append s1 (Seq.append s2 s3) end + | term (Abs (x, T, t)) = + let + val s1 = Seq.append (term t) (Seq.single t) + val s2 = Seq.map (fn t => Abs (x, T, t)) (term t) + in Seq.append s1 s2 end + | term _ = Seq.empty + +end diff --git a/thys/SpecCheck/shrink/shrink_types.ML b/thys/SpecCheck/shrink/shrink_types.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/shrink/shrink_types.ML @@ -0,0 +1,17 @@ +(* Title: SpecCheck/shrink/shrink_types.ML + Author: Kevin Kappelmann + +Shared type definitions for SpecCheck shrinkable types. +*) + +signature SPECCHECK_SHRINK_TYPES = +sig + type 'a shrink = 'a -> 'a Seq.seq +end + +structure SpecCheck_Shrink_Types : SPECCHECK_SHRINK_TYPES = +struct + +type 'a shrink = 'a -> 'a Seq.seq + +end diff --git a/thys/SpecCheck/speccheck.ML b/thys/SpecCheck/speccheck.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/speccheck.ML @@ -0,0 +1,205 @@ +(* Title: SpecCheck/speccheck.ML + Author: Lukas Bulwahn, Nicolai Schaffroth, and Kevin Kappelmann TU Muenchen + Author: Christopher League + +Specification-based testing of ML programs. +*) + +signature SPECCHECK = +sig + + (*tries to shrink a given (failing) input to a smaller, failing input*) + val try_shrink : 'a SpecCheck_Property.prop -> 'a SpecCheck_Shrink.shrink -> 'a -> int -> + SpecCheck_Base.stats -> ('a * SpecCheck_Base.stats) + + (*runs a property for a given test case and returns the result and the updated the statistics*) + val run_a_test : 'a SpecCheck_Property.prop -> 'a -> SpecCheck_Base.stats -> + SpecCheck_Base.result_single * SpecCheck_Base.stats + + (*returns the new state after executing the test*) + val check_style : 'a SpecCheck_Output_Style_Types.output_style -> + ('a SpecCheck_Show.show) option -> 'a SpecCheck_Shrink.shrink -> + ('a, 's) SpecCheck_Generator.gen_state -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 's -> 's + val check_shrink : 'a SpecCheck_Show.show -> 'a SpecCheck_Shrink.shrink -> + ('a, 's) SpecCheck_Generator.gen_state -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 's -> 's + val check : 'a SpecCheck_Show.show -> ('a, 's) SpecCheck_Generator.gen_state -> string -> + 'a SpecCheck_Property.prop -> Proof.context -> 's -> 's + val check_base : ('a, 's) SpecCheck_Generator.gen_state -> string -> + 'a SpecCheck_Property.prop -> Proof.context -> 's -> 's + + (*returns all unprocessed elements of the sequence*) + val check_seq_style : 'a SpecCheck_Output_Style_Types.output_style -> + ('a SpecCheck_Show.show) option -> 'a Seq.seq -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 'a Seq.seq + val check_seq : 'a SpecCheck_Show.show -> 'a Seq.seq -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 'a Seq.seq + val check_seq_base : 'a Seq.seq -> string -> 'a SpecCheck_Property.prop -> Proof.context -> + 'a Seq.seq + + (*returns all unused elements of the list*) + val check_list_style : 'a SpecCheck_Output_Style_Types.output_style -> + ('a SpecCheck_Show.show) option -> 'a list -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 'a Seq.seq + val check_list : 'a SpecCheck_Show.show -> 'a list -> string -> 'a SpecCheck_Property.prop -> + Proof.context -> 'a Seq.seq + val check_list_base : 'a list -> string -> 'a SpecCheck_Property.prop -> Proof.context -> + 'a Seq.seq + +end + +structure SpecCheck : SPECCHECK = +struct + +open SpecCheck_Base + +fun run_a_test prop input { + num_success_tests, + num_failed_tests, + num_discarded_tests, + num_recently_discarded_tests, + num_success_shrinks, + num_failed_shrinks, + timing + } = + let + val (time, result) = Timing.timing (fn () => prop input) () + val is_success = case result of Result is_success => is_success | _ => false + val is_discard = case result of Discard => true | _ => false + val is_failure = not is_discard andalso not is_success + + val num_success_tests = num_success_tests + (if is_success then 1 else 0) + val num_failed_tests = num_failed_tests + (if is_failure then 1 else 0) + val num_discarded_tests = num_discarded_tests + (if is_discard then 1 else 0) + val num_recently_discarded_tests = if is_discard then num_recently_discarded_tests + 1 else 0 + val timing = add_timing timing time + + val stats = { + num_success_tests = num_success_tests, + num_failed_tests = num_failed_tests, + num_discarded_tests = num_discarded_tests, + num_recently_discarded_tests = num_recently_discarded_tests, + num_success_shrinks = num_success_shrinks, + num_failed_shrinks = num_failed_shrinks, + timing = timing + } + in (result, stats) end + +fun add_num_success_shrinks stats n = { + num_success_tests = #num_success_tests stats, + num_failed_tests = #num_failed_tests stats, + num_discarded_tests = #num_discarded_tests stats, + num_recently_discarded_tests = #num_recently_discarded_tests stats, + num_success_shrinks = #num_success_shrinks stats + n, + num_failed_shrinks = #num_failed_shrinks stats, + timing = #timing stats +} + +fun add_num_failed_shrinks stats n = { + num_success_tests = #num_success_tests stats, + num_failed_tests = #num_failed_tests stats, + num_discarded_tests = #num_discarded_tests stats, + num_recently_discarded_tests = #num_recently_discarded_tests stats, + num_success_shrinks = #num_success_shrinks stats, + num_failed_shrinks = #num_failed_shrinks stats + n, + timing = #timing stats +} + +fun try_shrink prop shrink input max_shrinks stats = + let + fun is_failure input = case run_a_test prop input empty_stats |> fst of + Result is_success => not is_success + | Discard => false + | Exception _ => false (*do not count exceptions as a failure because the shrinker might + just have broken some invariant of the function*) + fun find_first_failure xq pulls_left stats = + if pulls_left <= 0 + then (NONE, pulls_left, stats) + else + case Seq.pull xq of + NONE => (NONE, pulls_left, stats) + | SOME (x, xq) => + if is_failure x + then (SOME x, pulls_left - 1, add_num_success_shrinks stats 1) + else find_first_failure xq (pulls_left - 1) (add_num_failed_shrinks stats 1) + in + (*always try the first successful branch and abort without backtracking once no further + shrink is possible.*) + case find_first_failure (shrink input) max_shrinks stats of + (*recursively shrink*) + (SOME input, shrinks_left, stats) => try_shrink prop shrink input shrinks_left stats + | (NONE, _, stats) => (input, stats) + end + +fun test output_style init_stats show_opt shrink opt_gen name prop ctxt state = + let + val max_discard_ratio = Config.get ctxt SpecCheck_Configuration.max_discard_ratio + val max_success = Config.get ctxt SpecCheck_Configuration.max_success + (*number of counterexamples to generate before stopping the test*) + val num_counterexamples = + let val conf_num_counterexamples = + Config.get ctxt SpecCheck_Configuration.num_counterexamples + in if conf_num_counterexamples > 0 then conf_num_counterexamples else ~1 end + val max_shrinks = Config.get ctxt SpecCheck_Configuration.max_shrinks + + fun run_tests opt_gen state stats counterexamples = + (*stop the test run if enough (successful) tests were run or counterexamples were found*) + if #num_success_tests stats >= max_success then (Success stats, state) + else if num_tests stats >= max_success orelse + #num_failed_tests stats = num_counterexamples + then (Failure (stats, failure_data counterexamples), state) + else (*test input and attempt to shrink on failure*) + let val (input_opt, state) = opt_gen state + in + case input_opt of + NONE => + if #num_failed_tests stats > 0 + then (Failure (stats, failure_data counterexamples), state) + else (Success stats, state) + | SOME input => + let val (result, stats) = run_a_test prop input stats + in + case result of + Result true => run_tests opt_gen state stats counterexamples + | Result false => + let val (counterexample, stats) = try_shrink prop shrink input max_shrinks stats + in run_tests opt_gen state stats (counterexample :: counterexamples) end + | Discard => + if #num_recently_discarded_tests stats > max_discard_ratio + then + if #num_failed_tests stats > 0 + then (Failure (stats, failure_data counterexamples), state) + else (Gave_Up stats, state) + else run_tests opt_gen state stats counterexamples + | Exception exn => + (Failure (stats, failure_data_exn (input :: counterexamples) exn), state) + end + end + in + Timing.timing (fn _ => run_tests opt_gen state init_stats []) () + |> uncurry (apfst o output_style show_opt ctxt name) + |> snd + end + +fun check_style style show_opt shrink = + test style empty_stats show_opt shrink o SpecCheck_Generator.map SOME + +fun check_shrink show = check_style SpecCheck_Default_Output_Style.default (SOME show) +fun check show = check_shrink show SpecCheck_Shrink.none + +fun check_base gen = + check_style SpecCheck_Default_Output_Style.default NONE SpecCheck_Shrink.none gen + +fun check_seq_style style show_opt xq name prop ctxt = + test style empty_stats show_opt SpecCheck_Shrink.none SpecCheck_Generator.of_seq name prop ctxt + xq + +fun check_seq show = check_seq_style SpecCheck_Default_Output_Style.default (SOME show) +fun check_seq_base xq = check_seq_style SpecCheck_Default_Output_Style.default NONE xq + +fun check_list_style style show = check_seq_style style show o Seq.of_list +fun check_list show = check_seq show o Seq.of_list +fun check_list_base xs = check_seq_base (Seq.of_list xs) + +end diff --git a/thys/SpecCheck/speccheck_base.ML b/thys/SpecCheck/speccheck_base.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/speccheck_base.ML @@ -0,0 +1,111 @@ +(* Title: SpecCheck/speccheck_base.ML + Author: Kevin Kappelmann + +Types returned by single tests and complete test runs as well as simple utility methods on them. +*) + +signature SPECCHECK_BASE = +sig + + datatype result_single = Result of bool | Discard | Exception of exn + + type stats = { + num_success_tests : int, + num_failed_tests : int, + num_discarded_tests : int, + num_recently_discarded_tests : int, + num_success_shrinks : int, + num_failed_shrinks : int, + timing : Timing.timing + } + + val add_timing : Timing.timing -> Timing.timing -> Timing.timing + + val empty_stats : stats + val num_tests : stats -> int + val num_shrinks : stats -> int + + type 'a failure_data = { + counterexamples : 'a list, + the_exception : exn option + } + + val failure_data : 'a list -> 'a failure_data + val failure_data_exn : 'a list -> exn -> 'a failure_data + + datatype 'a result = + Success of stats | + Gave_Up of stats | + Failure of stats * 'a failure_data + + val stats_of_result : 'a result -> stats + +end + +structure SpecCheck_Base : SPECCHECK_BASE = +struct + +datatype result_single = Result of bool | Discard | Exception of exn + +type stats = { + num_success_tests : int, + num_failed_tests : int, + num_discarded_tests : int, + num_recently_discarded_tests : int, + num_success_shrinks : int, + num_failed_shrinks : int, + timing : Timing.timing +} + +val empty_stats = { + num_success_tests = 0, + num_failed_tests = 0, + num_discarded_tests = 0, + num_recently_discarded_tests = 0, + num_success_shrinks = 0, + num_failed_shrinks = 0, + timing = { + cpu = Time.zeroTime, + elapsed = Time.zeroTime, + gc = Time.zeroTime + } +} + +fun add_timing {elapsed = elapsed1, cpu = cpu1, gc = gc1} + {elapsed = elapsed2, cpu = cpu2, gc = gc2} = { + elapsed = elapsed1 + elapsed2, + cpu = cpu1 + cpu2, + gc = gc1 + gc2 +} + +fun num_tests {num_success_tests, num_failed_tests, ...} = + num_success_tests + num_failed_tests + +fun num_shrinks {num_success_shrinks, num_failed_shrinks, ...} = + num_success_shrinks + num_failed_shrinks + +type 'a failure_data = { + counterexamples : 'a list, + the_exception : exn option +} + +fun failure_data counterexamples = { + counterexamples = counterexamples, + the_exception = NONE +} + +fun failure_data_exn counterexamples exn = { + counterexamples = counterexamples, + the_exception = SOME exn +} + +datatype 'a result = + Success of stats | + Gave_Up of stats | + Failure of stats * 'a failure_data + +fun stats_of_result (Success stats) = stats + | stats_of_result (Gave_Up stats) = stats + | stats_of_result (Failure (stats, _)) = stats + +end diff --git a/thys/SpecCheck/util.ML b/thys/SpecCheck/util.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/util.ML @@ -0,0 +1,19 @@ +(* Title: SpecCheck/util.ML + Author: Kevin Kappelmann + +General utility functions for SpecCheck. +*) + +signature SPECCHECK_UTIL = +sig + +val spaces : string list -> string + +end + +structure SpecCheck_Util : SPECCHECK_UTIL = +struct + +val spaces = space_implode " " + +end