support for ISABELLE_GHC on Windows, using the native version (mingw32);

--- a/src/HOL/Library/code_test.ML	Mon May 22 19:42:52 2017 +0200
+++ b/src/HOL/Library/code_test.ML	Mon May 22 21:47:07 2017 +0200
@@ -510,8 +510,8 @@
     val compiled_path = Path.append path (Path.basic "test")
     val compile_cmd =
       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
-      Config.get ctxt ghc_options ^ " -o " ^ File.bash_path compiled_path ^ " " ^
-      File.bash_path driver_path ^ " -i" ^ File.bash_path path
+      Config.get ctxt ghc_options ^ " -o " ^ Bash.string (File.platform_path compiled_path) ^ " " ^
+      Bash.string (File.platform_path driver_path) ^ " -i" ^ Bash.string (File.platform_path path)
 
     val run_cmd = File.bash_path compiled_path
   in

--- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Mon May 22 19:42:52 2017 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Mon May 22 21:47:07 2017 +0200
@@ -7,7 +7,7 @@
 
 open AbstractMachine;
 
-type program = string * string * (int Inttab.table)
+type program = string * Path.T * (int Inttab.table)
 
 fun count_patternvars PVar = 1
   | count_patternvars (PConst (_, ps)) =
@@ -210,11 +210,7 @@
         string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c
     end
 
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
-
-fun writeTextFile name s = File.write (Path.explode name) s
-
-fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
+fun tmp_file s = Path.expand (File.tmp_path (Path.basic s));
 
 fun compile eqs = 
     let
@@ -225,18 +221,18 @@
         val (arity, source) = haskell_prog module eqs
         val module_file = tmp_file (module^".hs")
         val object_file = tmp_file (module^".o")
-        val _ = writeTextFile module_file source
-        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
+        val _ = File.write module_file source
         val _ =
-          if not (fileExists object_file) then
+          Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^
+            Bash.string (File.platform_path module_file))
+        val _ =
+          if not (File.exists object_file) then
             raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
           else ()
     in
         (guid, module_file, arity)      
     end
 
-fun readResultFile name = File.read (Path.explode name) 
-
 fun parse_result arity_of result =
     let
         val result = String.explode result
@@ -308,14 +304,19 @@
         val result_file = tmp_file (module^"_Result_"^callguid^".txt")
         val call_file = tmp_file (call^".hs")
         val term = print_term arity_of 0 t
-        val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
-        val _ = writeTextFile call_file call_source
-        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
-        val result = readResultFile result_file handle IO.Io _ =>
+        val call_source =
+          "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^
+            File.platform_path result_file^"\" ("^term^")"
+        val _ = File.write call_file call_source
+        val _ =
+          Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^
+            Bash.string (File.platform_path module_file) ^ " " ^
+            Bash.string (File.platform_path call_file))
+        val result = File.read result_file handle IO.Io _ =>
           raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
         val t' = parse_result arity_of result
-        val _ = OS.FileSys.remove call_file
-        val _ = OS.FileSys.remove result_file
+        val _ = File.rm call_file
+        val _ = File.rm result_file
     in
         t'
     end

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 22 19:42:52 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 22 21:47:07 2017 +0200
@@ -256,14 +256,13 @@
               [(narrowing_engine_file,
                 if contains_existentials then pnf_narrowing_engine else narrowing_engine),
                (code_file, code), (main_file, main)])
-        val executable =
-          File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+        val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")
         val cmd =
           "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
             (space_implode " "
-              (map File.bash_path
+              (map (Bash.string o File.platform_path)
                 (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
-          " -o " ^ executable ^ ";"
+          " -o " ^ Bash.string (File.platform_path executable) ^ ";"
         val (_, compilation_time) =
           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
         val _ = Quickcheck.add_timing compilation_time current_result
@@ -278,7 +277,8 @@
               val ((response, _), timing) =
                 elapsed_time ("execution of size " ^ string_of_int k)
                   (fn () => Isabelle_System.bash_output
-                    (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
+                    (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
+                      string_of_int k))
               val _ = Quickcheck.add_timing timing current_result
             in
               if response = "NONE\n" then with_size genuine_only (k + 1)