# HG changeset patch # User bulwahn # Date 1299853273 -3600 # Node ID 1e008cc4883a758a0a9af95fdbac7158506a8cd6 # Parent c3c8b14f480ad174712830ca752d56860dac4368 renaming lazysmallcheck ML file to Quickcheck_Narrowing diff -r c3c8b14f480a -r 1e008cc4883a src/HOL/Library/Quickcheck_Narrowing.thy --- a/src/HOL/Library/Quickcheck_Narrowing.thy Fri Mar 11 15:21:13 2011 +0100 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy Fri Mar 11 15:21:13 2011 +0100 @@ -1,10 +1,10 @@ (* Author: Lukas Bulwahn, TU Muenchen *) -header {* Counterexample generator based on LazySmallCheck *} +header {* Counterexample generator preforming narrowing-based testing *} -theory LSC +theory Quickcheck_Narrowing imports Main "~~/src/HOL/Library/Code_Char" -uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML") +uses ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML") begin subsection {* Counterexample generator *} @@ -161,10 +161,10 @@ shows "apply f a d = apply f' a' d'" proof - note assms moreover - have "int_of (LSC.of_int 0) < int_of d' ==> int_of (LSC.of_int 0) <= int_of (LSC.of_int (int_of d' - int_of (LSC.of_int 1)))" + have "int_of (of_int 0) < int_of d' ==> int_of (of_int 0) <= int_of (of_int (int_of d' - int_of (of_int 1)))" by (simp add: of_int_inverse) moreover - have "int_of (LSC.of_int (int_of d' - int_of (LSC.of_int 1))) < int_of d'" + have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'" by (simp add: of_int_inverse) ultimately show ?thesis unfolding apply_def by (auto split: cons.split type.split simp add: Let_def) @@ -343,9 +343,9 @@ subsubsection {* Setting up the counterexample generator *} -use "~~/src/HOL/Tools/LSC/lazysmallcheck.ML" +use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML" -setup {* Lazysmallcheck.setup *} +setup {* Narrowing_Generators.setup *} hide_const (open) empty diff -r c3c8b14f480a -r 1e008cc4883a src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 11 15:21:13 2011 +0100 @@ -1,11 +1,11 @@ -(* Title: HOL/Tools/LSC/lazysmallcheck.ML +(* Title: HOL/Tools/Quickcheck/narrowing_generators.ML Author: Lukas Bulwahn, TU Muenchen -Prototypic implementation to invoke lazysmallcheck in Isabelle +Narrowing-based counterexample generation *) -signature LAZYSMALLCHECK = +signature NARROWING_GENERATORS = sig val compile_generator_expr: Proof.context -> term -> int -> term list option * Quickcheck.report option @@ -13,26 +13,25 @@ val setup: theory -> theory end; -structure Lazysmallcheck : LAZYSMALLCHECK = +structure Narrowing_Generators : NARROWING_GENERATORS = struct +val target = "Haskell" + (* invocation of Haskell interpreter *) -val lsc_module = File.read (Path.explode "~~/src/HOL/Tools/LSC/LazySmallCheck.hs") +val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs") fun exec verbose code = ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) fun value ctxt (get, put, put_ml) (code, value) = let - val tmp_prefix = "LSC" - fun make_cmd executable files = - getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^ - " -o " ^ executable ^ " && " ^ executable + val tmp_prefix = "Quickcheck_Narrowing" fun run in_path = let val code_file = Path.append in_path (Path.basic "Code.hs") - val lsc_file = Path.append in_path (Path.basic "LazySmallCheck.hs") + val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs") val main_file = Path.append in_path (Path.basic "Main.hs") val main = "module Main where {\n\n" ^ "import LazySmallCheck;\n" ^ @@ -42,13 +41,15 @@ val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n" (unprefix "module Code where {" code) val _ = File.write code_file code' - val _ = File.write lsc_file lsc_module + val _ = File.write narrowing_engine_file narrowing_engine val _ = File.write main_file main val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc")) - val cmd = make_cmd executable [code_file, lsc_file, main_file] + val cmd = getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ + (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^ + " -o " ^ executable ^ " && " ^ executable in bash_output cmd - end + end val result = Isabelle_System.with_tmp_dir tmp_prefix run val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result) @@ -70,26 +71,27 @@ fun dynamic_value_strict cookie thy postproc t args = let fun evaluator naming program ((_, vs_ty), t) deps = - evaluation cookie thy (Code_Target.evaluator thy "Haskell" naming program deps) (vs_ty, t) args; + evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args; in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; (* counterexample generator *) -structure Lazysmallcheck_Result = Proof_Data +structure Quickcheck_Narrowing_Result = Proof_Data ( type T = unit -> term list option - fun init _ () = error "Lazysmallcheck_Result" + fun init _ () = error " Quickcheck_Narrowing_Result" ) -val put_counterexample = Lazysmallcheck_Result.put +val put_counterexample = Quickcheck_Narrowing_Result.put fun compile_generator_expr ctxt t size = let val thy = ProofContext.theory_of ctxt fun ensure_testable t = - Const (@{const_name LSC.ensure_testable}, fastype_of t --> fastype_of t) $ t + Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t val t = dynamic_value_strict - (Lazysmallcheck_Result.get, Lazysmallcheck_Result.put, "Lazysmallcheck.put_counterexample") + (Quickcheck_Narrowing_Result.get, Quickcheck_Narrowing_Result.put, + "Quickcheck_Narrowing.put_counterexample") thy (Option.map o map) (ensure_testable t) [] in (t, NONE)