# HG changeset patch # User bulwahn # Date 1299836258 -3600 # Node ID 383bbdad1650779f8717c9c1fd68b13cecd8cc84 # Parent 3bd9a21366d2ee547057c8a5e41fc5dd3a141f0c replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype diff -r 3bd9a21366d2 -r 383bbdad1650 src/HOL/Library/LSC.thy --- a/src/HOL/Library/LSC.thy Fri Mar 11 10:37:37 2011 +0100 +++ b/src/HOL/Library/LSC.thy Fri Mar 11 10:37:38 2011 +0100 @@ -9,6 +9,16 @@ subsection {* Counterexample generator *} +subsubsection {* Code generation setup *} + +code_type typerep + ("Haskell" "Typerep") + +code_const Typerep.Typerep + ("Haskell" "Typerep") + +code_reserved Haskell Typerep + subsubsection {* Type code_int for Haskell's Int type *} typedef (open) code_int = "UNIV \ int set" diff -r 3bd9a21366d2 -r 383bbdad1650 src/HOL/Tools/LSC/lazysmallcheck.ML --- a/src/HOL/Tools/LSC/lazysmallcheck.ML Fri Mar 11 10:37:37 2011 +0100 +++ b/src/HOL/Tools/LSC/lazysmallcheck.ML Fri Mar 11 10:37:38 2011 +0100 @@ -25,7 +25,7 @@ fun value ctxt (get, put, put_ml) (code, value) = let - val prefix = "LSC" + val tmp_prefix = "LSC" fun make_cmd executable files = getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^ " -o " ^ executable ^ " && " ^ executable @@ -39,7 +39,9 @@ "import Code;\n\n" ^ "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^ "}\n" - val _ = File.write code_file code + 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 main_file main val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc")) @@ -47,7 +49,7 @@ in bash_output cmd end - val result = Isabelle_System.with_tmp_dir prefix run + 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) val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml