# HG changeset patch # User wenzelm # Date 1369939130 -7200 # Node ID 81fcc11d8c658cf0c1dc222d68f8156c9ec101c4 # Parent 2c141c169624c685d9cb49f86272862af0cbacd0 minor tuning -- more linebreaks; diff -r 2c141c169624 -r 81fcc11d8c65 src/HOL/Spec_Check/output_style.ML --- a/src/HOL/Spec_Check/output_style.ML Thu May 30 20:27:33 2013 +0200 +++ b/src/HOL/Spec_Check/output_style.ML Thu May 30 20:38:50 2013 +0200 @@ -28,16 +28,18 @@ fun result ({count=0,...}, _) _ = "dubious" | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" - | result ({count,tags,...}, badobjs) true = if not (null badobjs) then "FAILED" - else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" else "ok" + | result ({count,tags,...}, badobjs) true = + if not (null badobjs) then "FAILED" + else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" + else "ok" fun ratio (0, _) = "(0/0 passed)" | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" fun update (stats, badobjs) donep = - "\r" ^ (padRight #"." namew tag) ^ "." ^ (padRight #" " resultw (result (stats, badobjs) donep)) - ^ (padRight #" " countw (ratio (#count stats, length badobjs))) + "\r" ^ padRight #"." namew tag ^ "." ^ padRight #" " resultw (result (stats, badobjs) donep) + ^ padRight #" " countw (ratio (#count stats, length badobjs)) fun status (_, result, (stats, badobjs)) = if Property.failure result then writeln (update (stats, badobjs) false) else () @@ -93,7 +95,8 @@ let val gen_target = Config.get_generic ctxt Spec_Check.gen_target val _ = writeln ("[testing " ^ tag ^ "... ") - fun finish ({count, ...}, badobjs) = case (count, badobjs) of + fun finish ({count, ...}, badobjs) = + (case (count, badobjs) of (0, []) => writeln ("no valid cases generated]") | (n, []) => writeln ( if n >= gen_target then "ok]" @@ -105,7 +108,7 @@ | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) in (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ()) - end + end) in {status = K (), finish = finish} end diff -r 2c141c169624 -r 81fcc11d8c65 src/HOL/Spec_Check/property.ML --- a/src/HOL/Spec_Check/property.ML Thu May 30 20:27:33 2013 +0200 +++ b/src/HOL/Spec_Check/property.ML Thu May 30 20:38:50 2013 +0200 @@ -56,9 +56,13 @@ fun classify' f = wrap (fn (x, result, {tags, count}) => - { tags = if is_some result then - case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags - else tags, count = count }) + { tags = + if is_some result then + (case f x of + NONE => tags + | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags) + else tags, + count = count }) fun classify p tag = classify' (fn x => if p x then SOME tag else NONE) diff -r 2c141c169624 -r 81fcc11d8c65 src/HOL/Spec_Check/spec_check.ML --- a/src/HOL/Spec_Check/spec_check.ML Thu May 30 20:27:33 2013 +0200 +++ b/src/HOL/Spec_Check/spec_check.ML Thu May 30 20:38:50 2013 +0200 @@ -7,7 +7,6 @@ signature SPEC_CHECK = sig - val gen_target : int Config.T val gen_max : int Config.T val examples : int Config.T @@ -17,11 +16,13 @@ val style : string Config.T type output_style = Context.generic -> string -> - {status : string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit} + {status : string option * Property.result * (Property.stats * string option list) -> unit, + finish: Property.stats * string option list -> unit} val register_style : (string * output_style) -> theory -> theory - val checkGen : Context.generic -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit + val checkGen : Context.generic -> + 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit val check_property : Proof.context -> string -> unit end; @@ -46,7 +47,8 @@ type 'a rep = ('a -> string) option type output_style = Context.generic -> string -> - {status: string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit} + {status: string option * Property.result * (Property.stats * string option list) -> unit, + finish: Property.stats * string option list -> unit} fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen @@ -112,13 +114,14 @@ fun checks ctxt = cpsCheck ctxt Property.stats fun checkGen ctxt (gen, show) (tag, prop) = - check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream + check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream fun checkGenShrink ctxt shrink (gen, show) (tag, prop) = - cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink - (limit ctxt gen, show) (tag, prop) Generator.stream + cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink + (limit ctxt gen, show) (tag, prop) Generator.stream -fun checkOne ctxt show (tag, prop) obj = check ctxt (List.getItem, show) (tag, prop) [obj] +fun checkOne ctxt show (tag, prop) obj = + check ctxt (List.getItem, show) (tag, prop) [obj] (*calls the compiler and passes resulting type string to the parser*) fun determine_type context s = @@ -140,7 +143,8 @@ (*calls the compiler and runs the test*) fun run_test context s = let - val _ = Context.proof_map + val _ = + Context.proof_map (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") true s)) context in () end; @@ -152,7 +156,8 @@ 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; + Substring.string (Substring.dropl dot code)) + end; (*create the function from the input*) fun make_fun s =