# HG changeset patch
# User haftmann
# Date 1547882356 0
# Node ID 1fb204399d8d04aa2a773d4bfd493ebd3032c32a
# Parent  ab5a8a2519b0f4b9acd78709f0110b18c9425b10
self-contained code modules for Haskell

diff -r ab5a8a2519b0 -r 1fb204399d8d NEWS
--- a/NEWS	Fri Jan 18 19:48:04 2019 -0500
+++ b/NEWS	Sat Jan 19 07:19:16 2019 +0000
@@ -81,6 +81,10 @@
 file-system. To get generated code dumped into output, use "file \<open>\<close>".
 Minor INCOMPATIBILITY.
 
+* Code generation for Haskell: code includes for Haskell must contain
+proper module frame, nothing is added magically any longer.
+INCOMPATIBILITY.
+
 * Simplified syntax setup for big operators under image. In rare
 situations, type conversions are not inserted implicitly any longer
 and need to be given explicitly. Auxiliary abbreviations INFIMUM,
diff -r ab5a8a2519b0 -r 1fb204399d8d src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/Doc/Codegen/Adaptation.thy	Sat Jan 19 07:19:16 2019 +0000
@@ -379,9 +379,10 @@
   "code_printing"} command:
 \<close>
 
-code_printing %quotett
-  code_module "Errno" \<rightharpoonup> (Haskell)
-    \<open>errno i = error ("Error number: " ++ show i)\<close>
+code_printing %quotett code_module "Errno" \<rightharpoonup> (Haskell)
+ \<open>module Errno(errno) where
+
+  errno i = error ("Error number: " ++ show i)\<close>
 
 code_reserved %quotett Haskell Errno
 
@@ -393,4 +394,3 @@
 \<close>
 
 end
-
diff -r ab5a8a2519b0 -r 1fb204399d8d src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jan 19 07:19:16 2019 +0000
@@ -536,37 +536,34 @@
 text \<open>Adaption layer\<close>
 
 code_printing code_module "Heap" \<rightharpoonup> (Haskell)
-\<open>import qualified Control.Monad;
-import qualified Control.Monad.ST;
-import qualified Data.STRef;
-import qualified Data.Array.ST;
+\<open>
+module Heap(ST, RealWorld, STRef, newSTRef, readSTRef, writeSTRef,
+  STArray, newArray, newListArray, newFunArray, lengthArray, readArray, writeArray) where
 
-type RealWorld = Control.Monad.ST.RealWorld;
-type ST s a = Control.Monad.ST.ST s a;
-type STRef s a = Data.STRef.STRef s a;
-type STArray s a = Data.Array.ST.STArray s Integer a;
+import Control.Monad(liftM)
+import Control.Monad.ST(RealWorld, ST)
+import Data.STRef(STRef, newSTRef, readSTRef, writeSTRef)
+import qualified Data.Array.ST
 
-newSTRef = Data.STRef.newSTRef;
-readSTRef = Data.STRef.readSTRef;
-writeSTRef = Data.STRef.writeSTRef;
+type STArray s a = Data.Array.ST.STArray s Integer a
+
+newArray :: Integer -> a -> ST s (STArray s a)
+newArray k = Data.Array.ST.newArray (0, k - 1)
 
-newArray :: Integer -> a -> ST s (STArray s a);
-newArray k = Data.Array.ST.newArray (0, k - 1);
+newListArray :: [a] -> ST s (STArray s a)
+newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs - 1) xs
 
-newListArray :: [a] -> ST s (STArray s a);
-newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs - 1) xs;
-
-newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
-newFunArray k f = Data.Array.ST.newListArray (0, k - 1) (map f [0..k-1]);
+newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a)
+newFunArray k f = Data.Array.ST.newListArray (0, k - 1) (map f [0..k-1])
 
-lengthArray :: STArray s a -> ST s Integer;
-lengthArray a = Control.Monad.liftM (\(_, l) -> l + 1) (Data.Array.ST.getBounds a);
+lengthArray :: STArray s a -> ST s Integer
+lengthArray a = liftM (\(_, l) -> l + 1) (Data.Array.ST.getBounds a)
 
-readArray :: STArray s a -> Integer -> ST s a;
-readArray = Data.Array.ST.readArray;
+readArray :: STArray s a -> Integer -> ST s a
+readArray = Data.Array.ST.readArray
 
-writeArray :: STArray s a -> Integer -> a -> ST s ();
-writeArray = Data.Array.ST.writeArray;\<close>
+writeArray :: STArray s a -> Integer -> a -> ST s ()
+writeArray = Data.Array.ST.writeArray\<close>
 
 code_reserved Haskell Heap
 
diff -r ab5a8a2519b0 -r 1fb204399d8d src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/HOL/Library/Code_Lazy.thy	Sat Jan 19 07:19:16 2019 +0000
@@ -165,10 +165,12 @@
 
 
 code_printing
-  code_module Lazy \<rightharpoonup> (Haskell) 
-\<open>newtype Lazy a = Lazy a;
-delay f = Lazy (f ());
-force (Lazy x) = x;\<close> for type_constructor lazy constant delay force
+  code_module Lazy \<rightharpoonup> (Haskell) \<open>
+module Lazy(Lazy, delay, force) where
+
+newtype Lazy a = Lazy a
+delay f = Lazy (f ())
+force (Lazy x) = x\<close> for type_constructor lazy constant delay force
 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
diff -r ab5a8a2519b0 -r 1fb204399d8d src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/HOL/Library/IArray.thy	Sat Jan 19 07:19:16 2019 +0000
@@ -194,6 +194,8 @@
 
 code_printing
   code_module "IArray" \<rightharpoonup> (Haskell) \<open>
+module IArray(IArray, tabulate, of_list, sub, length) where {
+
   import Prelude (Bool(True, False), not, Maybe(Nothing, Just),
     Integer, (+), (-), (<), fromInteger, toInteger, map, seq, (.));
   import qualified Prelude;
@@ -213,8 +215,9 @@
   sub (IArray v, i) = v `Data.Array.Base.unsafeAt` fromInteger i;
 
   length :: IArray e -> Integer;
-  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
-  for type_constructor iarray constant IArray IArray.tabulate IArray.sub' IArray.length'
+  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));
+
+}\<close> for type_constructor iarray constant IArray IArray.tabulate IArray.sub' IArray.length'
 
 code_reserved Haskell IArray_Impl
 
diff -r ab5a8a2519b0 -r 1fb204399d8d src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Jan 19 07:19:16 2019 +0000
@@ -15,6 +15,8 @@
 
 code_printing
   code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) \<open>
+module Typerep(Typerep(..)) where
+
 data Typerep = Typerep String [Typerep]
 \<close> for type_constructor typerep constant Typerep.Typerep
 | type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
diff -r ab5a8a2519b0 -r 1fb204399d8d src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Jan 18 19:48:04 2019 -0500
+++ b/src/Tools/Code/code_haskell.ML	Sat Jan 19 07:19:16 2019 +0000
@@ -407,7 +407,7 @@
       end;
 
   in
-    (Code_Target.Hierarchy (map (fn (module_name, content) => print_module_frame module_name [] NONE [content]) includes
+    (Code_Target.Hierarchy (map (fn (module_name, content) => ([module_name ^ ".hs"], content)) includes
       @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
         ((flat o rev o Graph.strong_conn) haskell_program)), try (deresolver ""))
   end;