avoid "Code" as structure name (cf. 3bc39cfe27fe)
authorbulwahn
Tue Sep 06 16:40:22 2011 +0200 (2011-09-06)
changeset 44751f523923d8182
parent 44744 bdf8eb8f126b
child 44752 eaf394237ba7
avoid "Code" as structure name (cf. 3bc39cfe27fe)
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 14:25:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 16:40:22 2011 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  import Control.Exception;
     1.5  import System.IO;
     1.6  import System.Exit;
     1.7 -import Code;
     1.8 +import Generated_Code;
     1.9  
    1.10  type Pos = [Int];
    1.11  
     2.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 14:25:16 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 16:40:22 2011 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  import System.Exit
     2.5  import Maybe
     2.6  import List (partition, findIndex)
     2.7 -import Code
     2.8 +import Generated_Code
     2.9  
    2.10  
    2.11  type Pos = [Int]
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 14:25:16 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 16:40:22 2011 +0200
     3.3 @@ -235,17 +235,17 @@
     3.4        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     3.5      fun run in_path = 
     3.6        let
     3.7 -        val code_file = Path.append in_path (Path.basic "Code.hs")
     3.8 +        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
     3.9          val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    3.10          val main_file = Path.append in_path (Path.basic "Main.hs")
    3.11          val main = "module Main where {\n\n" ^
    3.12            "import System;\n" ^
    3.13            "import Narrowing_Engine;\n" ^
    3.14 -          "import Code;\n\n" ^
    3.15 -          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
    3.16 +          "import Generated_Code;\n\n" ^
    3.17 +          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
    3.18            "}\n"
    3.19 -        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    3.20 -          (unprefix "module Code where {" code)
    3.21 +        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    3.22 +          (unprefix "module Generated_Code where {" code)
    3.23          val _ = File.write code_file code'
    3.24          val _ = File.write narrowing_engine_file
    3.25            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
     4.1 --- a/src/Tools/Code/code_target.ML	Tue Sep 06 14:25:16 2011 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Tue Sep 06 16:40:22 2011 +0200
     4.3 @@ -394,7 +394,7 @@
     4.4  
     4.5  fun check_code_for thy target strict args naming program names_cs =
     4.6    let
     4.7 -    val module_name = "Code";
     4.8 +    val module_name = "Generated_Code";
     4.9      val { env_var, make_destination, make_command } =
    4.10        (#check o the_fundamental thy) target;
    4.11      fun ext_check p =
    4.12 @@ -435,7 +435,7 @@
    4.13  fun evaluator thy target naming program consts =
    4.14    let
    4.15      val (mounted_serializer, prepared_program) = mount_serializer thy
    4.16 -      target NONE "Code" [] naming program consts;
    4.17 +      target NONE "Generated_Code" [] naming program consts;
    4.18    in evaluation mounted_serializer prepared_program consts end;
    4.19  
    4.20  end; (* local *)