changed name space policy for Haskell includes
authorhaftmann
Tue Feb 03 19:37:00 2009 +0100 (2009-02-03)
changeset 2979386cac1fab613
parent 29790 02557b98bd0a
child 29794 32d00a2a6f28
changed name space policy for Haskell includes
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/ex/ImperativeQuicksort.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Feb 03 16:54:31 2009 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Feb 03 19:37:00 2009 +0100
     1.3 @@ -198,12 +198,12 @@
     1.4  
     1.5  subsubsection {* Haskell *}
     1.6  
     1.7 -code_type array (Haskell "STArray/ RealWorld/ _")
     1.8 +code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
     1.9  code_const Array (Haskell "error/ \"bare Array\"")
    1.10 -code_const Array.new' (Haskell "newArray/ (0,/ _)")
    1.11 -code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
    1.12 -code_const Array.length' (Haskell "lengthArray")
    1.13 -code_const Array.nth' (Haskell "readArray")
    1.14 -code_const Array.upd' (Haskell "writeArray")
    1.15 +code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
    1.16 +code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
    1.17 +code_const Array.length' (Haskell "Heap.lengthArray")
    1.18 +code_const Array.nth' (Haskell "Heap.readArray")
    1.19 +code_const Array.upd' (Haskell "Heap.writeArray")
    1.20  
    1.21  end
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Feb 03 16:54:31 2009 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Feb 03 19:37:00 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Library/Heap_Monad.thy
     2.5 -    ID:         $Id$
     2.6      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     2.7  *)
     2.8  
     2.9 @@ -375,7 +374,7 @@
    2.10  
    2.11  text {* Adaption layer *}
    2.12  
    2.13 -code_include Haskell "STMonad"
    2.14 +code_include Haskell "Heap"
    2.15  {*import qualified Control.Monad;
    2.16  import qualified Control.Monad.ST;
    2.17  import qualified Data.STRef;
    2.18 @@ -386,9 +385,6 @@
    2.19  type STRef s a = Data.STRef.STRef s a;
    2.20  type STArray s a = Data.Array.ST.STArray s Int a;
    2.21  
    2.22 -runST :: (forall s. ST s a) -> a;
    2.23 -runST s = Control.Monad.ST.runST s;
    2.24 -
    2.25  newSTRef = Data.STRef.newSTRef;
    2.26  readSTRef = Data.STRef.readSTRef;
    2.27  writeSTRef = Data.STRef.writeSTRef;
    2.28 @@ -408,14 +404,11 @@
    2.29  writeArray :: STArray s a -> Int -> a -> ST s ();
    2.30  writeArray = Data.Array.ST.writeArray;*}
    2.31  
    2.32 -code_reserved Haskell RealWorld ST STRef Array
    2.33 -  runST
    2.34 -  newSTRef reasSTRef writeSTRef
    2.35 -  newArray newListArray lengthArray readArray writeArray
    2.36 +code_reserved Haskell Heap
    2.37  
    2.38  text {* Monad *}
    2.39  
    2.40 -code_type Heap (Haskell "ST/ RealWorld/ _")
    2.41 +code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
    2.42  code_const Heap (Haskell "error/ \"bare Heap\"")
    2.43  code_monad "op \<guillemotright>=" Haskell
    2.44  code_const return (Haskell "return")
     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Feb 03 16:54:31 2009 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Feb 03 19:37:00 2009 +0100
     3.3 @@ -82,10 +82,10 @@
     3.4  
     3.5  subsubsection {* Haskell *}
     3.6  
     3.7 -code_type ref (Haskell "STRef/ RealWorld/ _")
     3.8 +code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
     3.9  code_const Ref (Haskell "error/ \"bare Ref\"")
    3.10 -code_const Ref.new (Haskell "newSTRef")
    3.11 -code_const Ref.lookup (Haskell "readSTRef")
    3.12 -code_const Ref.update (Haskell "writeSTRef")
    3.13 +code_const Ref.new (Haskell "Heap.newSTRef")
    3.14 +code_const Ref.lookup (Haskell "Heap.readSTRef")
    3.15 +code_const Ref.update (Haskell "Heap.writeSTRef")
    3.16  
    3.17  end
    3.18 \ No newline at end of file
     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Feb 03 16:54:31 2009 +0100
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Feb 03 19:37:00 2009 +0100
     4.3 @@ -308,7 +308,7 @@
     4.4  code_reserved Haskell Nat
     4.5  
     4.6  code_type nat
     4.7 -  (Haskell "Nat")
     4.8 +  (Haskell "Nat.Nat")
     4.9  
    4.10  code_instance nat :: eq
    4.11    (Haskell -)
     5.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Tue Feb 03 16:54:31 2009 +0100
     5.2 +++ b/src/HOL/ex/ImperativeQuicksort.thy	Tue Feb 03 19:37:00 2009 +0100
     5.3 @@ -629,9 +629,9 @@
     5.4  
     5.5  ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
     5.6  
     5.7 -export_code qsort in SML_imp module_name Arr
     5.8 -export_code qsort in OCaml module_name Arr file -
     5.9 -export_code qsort in OCaml_imp module_name Arr file -
    5.10 -export_code qsort in Haskell module_name Arr file -
    5.11 +export_code qsort in SML_imp module_name QSort
    5.12 +export_code qsort in OCaml module_name QSort file -
    5.13 +export_code qsort in OCaml_imp module_name QSort file -
    5.14 +export_code qsort in Haskell module_name QSort file -
    5.15  
    5.16  end
    5.17 \ No newline at end of file