# HG changeset patch
# User haftmann
# Date 1233686220 -3600
# Node ID 86cac1fab6130db30c885cb8140269c2b9359b37
# Parent  02557b98bd0a09fbeb31e2b29a0f2d2da23a129e
changed name space policy for Haskell includes

diff -r 02557b98bd0a -r 86cac1fab613 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Feb 03 19:37:00 2009 +0100
@@ -198,12 +198,12 @@
 
 subsubsection {* Haskell *}
 
-code_type array (Haskell "STArray/ RealWorld/ _")
+code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
 code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "newArray/ (0,/ _)")
-code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "lengthArray")
-code_const Array.nth' (Haskell "readArray")
-code_const Array.upd' (Haskell "writeArray")
+code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
+code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
+code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.nth' (Haskell "Heap.readArray")
+code_const Array.upd' (Haskell "Heap.writeArray")
 
 end
diff -r 02557b98bd0a -r 86cac1fab613 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Feb 03 19:37:00 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Heap_Monad.thy
-    ID:         $Id$
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
@@ -375,7 +374,7 @@
 
 text {* Adaption layer *}
 
-code_include Haskell "STMonad"
+code_include Haskell "Heap"
 {*import qualified Control.Monad;
 import qualified Control.Monad.ST;
 import qualified Data.STRef;
@@ -386,9 +385,6 @@
 type STRef s a = Data.STRef.STRef s a;
 type STArray s a = Data.Array.ST.STArray s Int a;
 
-runST :: (forall s. ST s a) -> a;
-runST s = Control.Monad.ST.runST s;
-
 newSTRef = Data.STRef.newSTRef;
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
@@ -408,14 +404,11 @@
 writeArray :: STArray s a -> Int -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
-code_reserved Haskell RealWorld ST STRef Array
-  runST
-  newSTRef reasSTRef writeSTRef
-  newArray newListArray lengthArray readArray writeArray
+code_reserved Haskell Heap
 
 text {* Monad *}
 
-code_type Heap (Haskell "ST/ RealWorld/ _")
+code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
 code_const Heap (Haskell "error/ \"bare Heap\"")
 code_monad "op \<guillemotright>=" Haskell
 code_const return (Haskell "return")
diff -r 02557b98bd0a -r 86cac1fab613 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Feb 03 19:37:00 2009 +0100
@@ -82,10 +82,10 @@
 
 subsubsection {* Haskell *}
 
-code_type ref (Haskell "STRef/ RealWorld/ _")
+code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
 code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const Ref.new (Haskell "newSTRef")
-code_const Ref.lookup (Haskell "readSTRef")
-code_const Ref.update (Haskell "writeSTRef")
+code_const Ref.new (Haskell "Heap.newSTRef")
+code_const Ref.lookup (Haskell "Heap.readSTRef")
+code_const Ref.update (Haskell "Heap.writeSTRef")
 
 end
\ No newline at end of file
diff -r 02557b98bd0a -r 86cac1fab613 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Feb 03 19:37:00 2009 +0100
@@ -308,7 +308,7 @@
 code_reserved Haskell Nat
 
 code_type nat
-  (Haskell "Nat")
+  (Haskell "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
diff -r 02557b98bd0a -r 86cac1fab613 src/HOL/ex/ImperativeQuicksort.thy
--- a/src/HOL/ex/ImperativeQuicksort.thy	Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Tue Feb 03 19:37:00 2009 +0100
@@ -629,9 +629,9 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort in SML_imp module_name Arr
-export_code qsort in OCaml module_name Arr file -
-export_code qsort in OCaml_imp module_name Arr file -
-export_code qsort in Haskell module_name Arr file -
+export_code qsort in SML_imp module_name QSort
+export_code qsort in OCaml module_name QSort file -
+export_code qsort in OCaml_imp module_name QSort file -
+export_code qsort in Haskell module_name QSort file -
 
 end
\ No newline at end of file