src/HOL/Matrix/Compute_Oracle/am_ghc.ML

 (*  Title:      Tools/Compute_Oracle/am_ghc.ML
     Author:     Steven Obua
 *)
 
-structure AM_GHC : ABSTRACT_MACHINE = struct
+structure AM_GHC : ABSTRACT_MACHINE =
+struct
 
 open AbstractMachine;
 
 type program = string * string * (int Inttab.table)
 

 fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
 fun wrap s = "\""^s^"\""
 
 fun writeTextFile name s = File.write (Path.explode name) s
     
-val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
-
 fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
 
 fun compile cache_patterns const_arity eqs = 
     let
         val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()

         val module = "AMGHC_Prog_"^guid
         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 _ = bash ((!ghc)^" -c "^module_file)
-        val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
+        val _ = bash ("\"$ISABELLE_GHC\" -c " ^ module_file)
+        val _ =
+          if not (fileExists 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) 

         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 _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
-        val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
+        val _ = bash ("\"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
+        val result = readResultFile 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
     in
         t'