diff --git a/thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy b/thys/SpecCheck/Dynamic/SpecCheck_Dynamic.thy rename from thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy rename to thys/SpecCheck/Dynamic/SpecCheck_Dynamic.thy --- a/thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy +++ b/thys/SpecCheck/Dynamic/SpecCheck_Dynamic.thy @@ -1,16 +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 +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 rename from thys/SpecCheck/dynamic/dynamic_construct.ML rename to thys/SpecCheck/Dynamic/dynamic_construct.ML --- a/thys/SpecCheck/dynamic/dynamic_construct.ML +++ b/thys/SpecCheck/Dynamic/dynamic_construct.ML @@ -1,188 +1,188 @@ -(* Title: SpecCheck/dynamic/dynamic_construct.ML +(* 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 rename from thys/SpecCheck/dynamic/speccheck_dynamic.ML rename to thys/SpecCheck/Dynamic/speccheck_dynamic.ML --- a/thys/SpecCheck/dynamic/speccheck_dynamic.ML +++ b/thys/SpecCheck/Dynamic/speccheck_dynamic.ML @@ -1,81 +1,81 @@ -(* Title: SpecCheck/dynamic/speccheck_dynamic.ML +(* 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 rename from thys/SpecCheck/examples/SpecCheck_Examples.thy rename to thys/SpecCheck/Examples/SpecCheck_Examples.thy diff --git a/thys/SpecCheck/generators/SpecCheck_Generators.thy b/thys/SpecCheck/Generators/SpecCheck_Generators.thy rename from thys/SpecCheck/generators/SpecCheck_Generators.thy rename to thys/SpecCheck/Generators/SpecCheck_Generators.thy diff --git a/thys/SpecCheck/generators/gen.ML b/thys/SpecCheck/Generators/gen.ML rename from thys/SpecCheck/generators/gen.ML rename to thys/SpecCheck/Generators/gen.ML --- a/thys/SpecCheck/generators/gen.ML +++ b/thys/SpecCheck/Generators/gen.ML @@ -1,15 +1,15 @@ -(* Title: SpecCheck/generators/gen.ML +(* 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 rename from thys/SpecCheck/generators/gen_base.ML rename to thys/SpecCheck/Generators/gen_base.ML --- a/thys/SpecCheck/generators/gen_base.ML +++ b/thys/SpecCheck/Generators/gen_base.ML @@ -1,244 +1,244 @@ -(* Title: SpecCheck/generators/gen_base.ML +(* 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 rename from thys/SpecCheck/generators/gen_function.ML rename to thys/SpecCheck/Generators/gen_function.ML --- a/thys/SpecCheck/generators/gen_function.ML +++ b/thys/SpecCheck/Generators/gen_function.ML @@ -1,41 +1,41 @@ -(* Title: SpecCheck/generators/gen_function.ML +(* 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 rename from thys/SpecCheck/generators/gen_int.ML rename to thys/SpecCheck/Generators/gen_int.ML --- a/thys/SpecCheck/generators/gen_int.ML +++ b/thys/SpecCheck/Generators/gen_int.ML @@ -1,38 +1,38 @@ -(* Title: SpecCheck/generators/gen_int.ML +(* 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 rename from thys/SpecCheck/generators/gen_real.ML rename to thys/SpecCheck/Generators/gen_real.ML --- a/thys/SpecCheck/generators/gen_real.ML +++ b/thys/SpecCheck/Generators/gen_real.ML @@ -1,65 +1,65 @@ -(* Title: SpecCheck/generators/gen_real.ML +(* 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 rename from thys/SpecCheck/generators/gen_term.ML rename to thys/SpecCheck/Generators/gen_term.ML --- a/thys/SpecCheck/generators/gen_term.ML +++ b/thys/SpecCheck/Generators/gen_term.ML @@ -1,269 +1,270 @@ -(* Title: SpecCheck/generators/gen_term.ML +(* Title: SpecCheck/Generators/gen_term.ML Author: Sebastian Willenbrink and Kevin Kappelmann TU Muenchen Generators for terms and types. *) -signature SPECCHECK_GEN_TERM = sig +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 rename from thys/SpecCheck/generators/gen_text.ML rename to thys/SpecCheck/Generators/gen_text.ML --- a/thys/SpecCheck/generators/gen_text.ML +++ b/thys/SpecCheck/Generators/gen_text.ML @@ -1,70 +1,70 @@ -(* Title: SpecCheck/generators/gen_text.ML +(* 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 rename from thys/SpecCheck/generators/gen_types.ML rename to thys/SpecCheck/Generators/gen_types.ML --- a/thys/SpecCheck/generators/gen_types.ML +++ b/thys/SpecCheck/Generators/gen_types.ML @@ -1,34 +1,34 @@ -(* Title: SpecCheck/generators/gen_types.ML +(* 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/output_styles/SpecCheck_Output_Style.thy b/thys/SpecCheck/Output_Styles/SpecCheck_Output_Style.thy rename from thys/SpecCheck/output_styles/SpecCheck_Output_Style.thy rename to thys/SpecCheck/Output_Styles/SpecCheck_Output_Style.thy diff --git a/thys/SpecCheck/output_styles/output_style.ML b/thys/SpecCheck/Output_Styles/output_style.ML rename from thys/SpecCheck/output_styles/output_style.ML rename to thys/SpecCheck/Output_Styles/output_style.ML --- a/thys/SpecCheck/output_styles/output_style.ML +++ b/thys/SpecCheck/Output_Styles/output_style.ML @@ -1,20 +1,20 @@ -(* Title: SpecCheck/output_styles/output_style.ML +(* 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 rename from thys/SpecCheck/output_styles/output_style_custom.ML rename to thys/SpecCheck/Output_Styles/output_style_custom.ML --- a/thys/SpecCheck/output_styles/output_style_custom.ML +++ b/thys/SpecCheck/Output_Styles/output_style_custom.ML @@ -1,83 +1,83 @@ -(* Title: SpecCheck/output_style/output_style_custom.ML +(* 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 rename from thys/SpecCheck/output_styles/output_style_perl.ML rename to thys/SpecCheck/Output_Styles/output_style_perl.ML --- a/thys/SpecCheck/output_styles/output_style_perl.ML +++ b/thys/SpecCheck/Output_Styles/output_style_perl.ML @@ -1,54 +1,54 @@ -(* Title: SpecCheck/output_styles/output_style_perl.ML +(* 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 rename from thys/SpecCheck/output_styles/output_style_types.ML rename to thys/SpecCheck/Output_Styles/output_style_types.ML --- a/thys/SpecCheck/output_styles/output_style_types.ML +++ b/thys/SpecCheck/Output_Styles/output_style_types.ML @@ -1,24 +1,24 @@ -(* Title: SpecCheck/output_styles/output_style_types.ML +(* 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/README.md b/thys/SpecCheck/README.md --- a/thys/SpecCheck/README.md +++ b/thys/SpecCheck/README.md @@ -1,61 +1,59 @@ # 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 --- a/thys/SpecCheck/ROOT +++ b/thys/SpecCheck/ROOT @@ -1,30 +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 + 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/show/SpecCheck_Show.thy b/thys/SpecCheck/Show/SpecCheck_Show.thy rename from thys/SpecCheck/show/SpecCheck_Show.thy rename to thys/SpecCheck/Show/SpecCheck_Show.thy --- a/thys/SpecCheck/show/SpecCheck_Show.thy +++ b/thys/SpecCheck/Show/SpecCheck_Show.thy @@ -1,15 +1,16 @@ \<^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_term.ML\ ML_file \show.ML\ end diff --git a/thys/SpecCheck/show/show.ML b/thys/SpecCheck/Show/show.ML rename from thys/SpecCheck/show/show.ML rename to thys/SpecCheck/Show/show.ML --- a/thys/SpecCheck/show/show.ML +++ b/thys/SpecCheck/Show/show.ML @@ -1,9 +1,10 @@ -(* Title: SpecCheck/show/show.ML +(* Title: SpecCheck/Show/show.ML Author: Kevin Kappelmann, TU Muenchen Structure containing all show functions. *) structure SpecCheck_Show = struct open SpecCheck_Show_Base +open SpecCheck_Show_Term end diff --git a/thys/SpecCheck/show/show_base.ML b/thys/SpecCheck/Show/show_base.ML rename from thys/SpecCheck/show/show_base.ML rename to thys/SpecCheck/Show/show_base.ML --- a/thys/SpecCheck/show/show_base.ML +++ b/thys/SpecCheck/Show/show_base.ML @@ -1,47 +1,47 @@ -(* Title: SpecCheck/show/show_base.ML +(* 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_term.ML b/thys/SpecCheck/Show/show_term.ML new file mode 100644 --- /dev/null +++ b/thys/SpecCheck/Show/show_term.ML @@ -0,0 +1,54 @@ +(* Title: SpecCheck/Show/show_term.ML + Author: Kevin Kappelmann + +Show functions for terms, types, and related data structures. +*) + +signature SPECCHECK_SHOW_TERM = +sig + + val term : Proof.context -> term SpecCheck_Show_Types.show + val typ : Proof.context -> typ SpecCheck_Show_Types.show + val thm : Proof.context -> thm SpecCheck_Show_Types.show + + val tyenv : Proof.context -> Type.tyenv SpecCheck_Show_Types.show + val tenv : Proof.context -> Envir.tenv SpecCheck_Show_Types.show + val env : Proof.context -> Envir.env SpecCheck_Show_Types.show + +end + +structure SpecCheck_Show_Term : SPECCHECK_SHOW_TERM = +struct + +structure Show = SpecCheck_Show_Base + +val term = Syntax.pretty_term +val typ = Syntax.pretty_typ +fun thm ctxt = term ctxt o Thm.prop_of + +local +fun show_env_aux show_entry = + Vartab.dest + #> map show_entry + #> Pretty.list "[" "]" + +fun show_env_entry show (s, t) = Pretty.enum " := " "" "" (map show [s, t]) +in + +fun tyenv ctxt = + let + val show_entry = show_env_entry (typ ctxt) + fun get_typs (v, (s, T)) = (TVar (v, s), T) + in show_env_aux (show_entry o get_typs) end + +fun tenv ctxt = + let + val show_entry = show_env_entry (term ctxt) + fun get_trms (v, (T, t)) = (Var (v, T), t) + in show_env_aux (show_entry o get_trms) end + +end + +fun env ctxt env = Show.zip (tyenv ctxt) (tenv ctxt) (Envir.type_env env, Envir.term_env env) + +end diff --git a/thys/SpecCheck/show/show_types.ML b/thys/SpecCheck/Show/show_types.ML rename from thys/SpecCheck/show/show_types.ML rename to thys/SpecCheck/Show/show_types.ML --- a/thys/SpecCheck/show/show_types.ML +++ b/thys/SpecCheck/Show/show_types.ML @@ -1,17 +1,17 @@ -(* Title: SpecCheck/show/show_types.ML +(* 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 rename from thys/SpecCheck/shrink/SpecCheck_Shrink.thy rename to thys/SpecCheck/Shrink/SpecCheck_Shrink.thy diff --git a/thys/SpecCheck/shrink/shrink.ML b/thys/SpecCheck/Shrink/shrink.ML rename from thys/SpecCheck/shrink/shrink.ML rename to thys/SpecCheck/Shrink/shrink.ML --- a/thys/SpecCheck/shrink/shrink.ML +++ b/thys/SpecCheck/Shrink/shrink.ML @@ -1,11 +1,11 @@ -(* Title: SpecCheck/shrink/shrink.ML +(* 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 rename from thys/SpecCheck/shrink/shrink_base.ML rename to thys/SpecCheck/Shrink/shrink_base.ML --- a/thys/SpecCheck/shrink/shrink_base.ML +++ b/thys/SpecCheck/Shrink/shrink_base.ML @@ -1,89 +1,89 @@ -(* Title: SpecCheck/shrink/shrink_base.ML +(* 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 rename from thys/SpecCheck/shrink/shrink_types.ML rename to thys/SpecCheck/Shrink/shrink_types.ML --- a/thys/SpecCheck/shrink/shrink_types.ML +++ b/thys/SpecCheck/Shrink/shrink_types.ML @@ -1,17 +1,17 @@ -(* Title: SpecCheck/shrink/shrink_types.ML +(* 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.thy b/thys/SpecCheck/SpecCheck.thy --- a/thys/SpecCheck/SpecCheck.thy +++ b/thys/SpecCheck/SpecCheck.thy @@ -1,17 +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 \lecker.ML\ ML_file \speccheck.ML\ -ML_file \lecker.ML\ end diff --git a/thys/SpecCheck/lecker.ML b/thys/SpecCheck/lecker.ML --- a/thys/SpecCheck/lecker.ML +++ b/thys/SpecCheck/lecker.ML @@ -1,23 +1,28 @@ (* 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 + type ('f, 's) test_state = 'f -> 's -> 's + type 'f test = ('f, SpecCheck_Random.rand) test_state (*the first parameter to test_group will usually be a context*) - val test_group : 'a -> 's -> ('a -> 's -> 's) list -> 's + val test_group : 'f -> 's -> (('f, 's) test_state) list -> 's end structure Lecker : LECKER = struct +type ('f, 's) test_state = 'f -> 's -> 's +type 'f test = ('f, SpecCheck_Random.rand) test_state + 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) + fold (fn t => (Pretty.writeln (Pretty.brk 0); t fixed_param)) ts (t fixed_param s) end diff --git a/thys/SpecCheck/speccheck.ML b/thys/SpecCheck/speccheck.ML --- a/thys/SpecCheck/speccheck.ML +++ b/thys/SpecCheck/speccheck.ML @@ -1,205 +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 + (Proof.context, 's) Lecker.test_state 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 + (Proof.context, 's) Lecker.test_state val check : 'a SpecCheck_Show.show -> ('a, 's) SpecCheck_Generator.gen_state -> string -> - 'a SpecCheck_Property.prop -> Proof.context -> 's -> 's + 'a SpecCheck_Property.prop -> (Proof.context, 's) Lecker.test_state val check_base : ('a, 's) SpecCheck_Generator.gen_state -> string -> - 'a SpecCheck_Property.prop -> Proof.context -> 's -> 's + 'a SpecCheck_Property.prop -> (Proof.context, 's) Lecker.test_state (*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