src/HOL/Matrix/Compute_Oracle/am_ghc.ML
changeset 41953 994d088fbfbc
parent 41952 c7297638599b
child 41959 b460124855b8
equal deleted inserted replaced
41952:c7297638599b 41953:994d088fbfbc
   225         val module = "AMGHC_Prog_"^guid
   225         val module = "AMGHC_Prog_"^guid
   226         val (arity, source) = haskell_prog module eqs
   226         val (arity, source) = haskell_prog module eqs
   227         val module_file = tmp_file (module^".hs")
   227         val module_file = tmp_file (module^".hs")
   228         val object_file = tmp_file (module^".o")
   228         val object_file = tmp_file (module^".o")
   229         val _ = writeTextFile module_file source
   229         val _ = writeTextFile module_file source
   230         val _ = bash ("\"$ISABELLE_GHC\" -c " ^ module_file)
   230         val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
   231         val _ =
   231         val _ =
   232           if not (fileExists object_file) then
   232           if not (fileExists object_file) then
   233             raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
   233             raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
   234           else ()
   234           else ()
   235     in
   235     in
   309         val result_file = tmp_file (module^"_Result_"^callguid^".txt")
   309         val result_file = tmp_file (module^"_Result_"^callguid^".txt")
   310         val call_file = tmp_file (call^".hs")
   310         val call_file = tmp_file (call^".hs")
   311         val term = print_term arity_of 0 t
   311         val term = print_term arity_of 0 t
   312         val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
   312         val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
   313         val _ = writeTextFile call_file call_source
   313         val _ = writeTextFile call_file call_source
   314         val _ = bash ("\"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
   314         val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
   315         val result = readResultFile result_file handle IO.Io _ =>
   315         val result = readResultFile result_file handle IO.Io _ =>
   316           raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
   316           raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
   317         val t' = parse_result arity_of result
   317         val t' = parse_result arity_of result
   318         val _ = OS.FileSys.remove call_file
   318         val _ = OS.FileSys.remove call_file
   319         val _ = OS.FileSys.remove result_file
   319         val _ = OS.FileSys.remove result_file