{-# LANGUAGE Trustworthy, Rank2Types, ScopedTypeVariables, MagicHash, UnboxedTuples, FlexibleInstances, GeneralizedNewtypeDeriving, NoMonomorphismRestriction #-}
-- | A linear type-based I/O system a la Clean - including a "safe C" (like Cyclone).
--
--   This is an alternative to composing monads - one can decompose them into their
--   corresponding comonads, with linear operations for manipulating them.
--   (See Kieburtz, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.5169&rep=rep1&type=pdf)
module Control.Linear (St, A, Blank, Pair, Fn, (>>==), rtn,
-- * Algebraic operations
run, bimap, assoc1, assoc2, drop1, drop2, undrop1, undrop2, swap, apply, curry, distr, assoc3, assoc4, void', bimap',
-- * Basic I/O system
Exclusive, Semiclosed, Open, Placeholder(Placeholder), open, getStdin, getStdout, getStderr, close, close1, fileSize, setFileSize, eof, seek, tell, char, line, lookahead, contents, putC, putS, random,
-- * Safe pointer facilities
Pointer, Linear(Linear), Nonlinear(Nonlinear), Focused(Focused), Fix(In), fixInj1, fixInj2, Weakening(weakening), contraction, new, free, split, ptrSwap,
-- ** Focusing
focus, focusHdl,
-- ** Strong update
peek', poke', changeType,
-- ** Operations on nonlinear data / Weak update
newNonlinear, peek1, poke1,
-- * Multithreading
fork, join',
-- * Example programs
helloWorld, printStuff, concurrent
) where

import Control.Arrow
import Control.Category
import Control.Monad
import Control.Parallel
import GHC.Prim
import GHC.IO
import GHC.Base (realWorld#)
import System.IO
import Foreign.ForeignPtr hiding (unsafeForeignPtrToPtr)
import Foreign.ForeignPtr.Unsafe
import Foreign.StablePtr
import Foreign.Ptr
import qualified Foreign.Marshal.Alloc as A
import Foreign.Storable
import Data.Default
import Data.Int
import Prelude hiding (id, (.), curry)
import System.Random hiding (split, random)
import System.IO.Unsafe

-- * Linear type machinery

-- | Values representing the real world.
data St = St (State# RealWorld)

-- | Linear computations are arrows over linear data, but monads over nonlinear data.
newtype A t u v = A (u -> (v, t))

type Fn t u = A () (Pair t St) (Pair u St)

data Blank = Blank

data Pair t u = Pair t u

instance (Default a) => Category (A a) where
	id = rtn def
	a . a2 = a2 >>== \(_ :: a) -> a

instance (Default a) => Arrow (A a) where
	arr f = A (\x -> (f x, def))
	first (A f) = A (\(x, y) -> let (z, a) = f x in ((z, y), a))

instance (Default a) => ArrowChoice (A a) where
	A f +++ A g = A (\ei -> either (\x -> let (y, z) = f x in (Left y, z))
		(\x -> let (y, z) = g x in (Right y, z))
		ei)
	left a = a +++ id

infixl 1 >>==

-- | Monadic bind (for nonlinear data).
{-# INLINE[0] (>>==) #-}
A f >>== g = A (\x -> case f x of
	(y, z) -> case g z of
		A h -> h y)

-- | Monadic return
{-# INLINE[0] rtn #-}
rtn x = A (\y -> (y, x))

-- | This setup is from http://cs.ioc.ee/~tarmo/tsem11/jeltsch1602-slides.pdf
--
-- It implements some of http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf

{-# INLINE[0] run #-}
run :: A a St St -> IO a
run (A f) = IO $ \world -> case f (St world) of (St world', x) -> (# world', x #)

{-# INLINE[0] bimap #-}
bimap (A f) (A g) = A (\(Pair a b) -> let
	(c, d) = f a
	(e, h) = g b in
	(c `par` e) `seq` (Pair c e, (d, h)))

{-# INLINE[0] assoc1 #-}
assoc1 = A (\(Pair (Pair a b) c) -> (Pair a (Pair b c), ()))

{-# INLINE[0] assoc2 #-}
assoc2 = A (\(Pair a (Pair b c)) -> (Pair (Pair a b) c, ()))

{-# INLINE[0] drop1 #-}
drop1 = A (\(Pair Blank x) -> (x, ()))

{-# INLINE[0] drop2 #-}
drop2 = A (\(Pair x Blank) -> (x, ()))

{-# INLINE[0] undrop1 #-}
undrop1 = A (\x -> (Pair Blank x, ()))

{-# INLINE[0] undrop2 #-}
undrop2 = A (\x -> (Pair x Blank, ()))

{-# INLINE[0] swap #-}
swap = A (\(Pair x y) -> (Pair y x, ()))

{-# INLINE[0] apply #-}
apply = A (\(Pair (A f) x) -> f x)

{-# INLINE[0] curry #-}
curry (A f) = A (\x -> (A (\y -> f (Pair x y)), ()))

{-# INLINE[0] distr #-}
distr = A (\(Pair a ei) -> (either (Left . Pair a) (Right . Pair a) ei, ()))

{-# INLINE[0] assoc3 #-}
assoc3 ((x, y), z) = (x, (y, z))

{-# INLINE[0] assoc4 #-}
assoc4 (x, (y, z)) = ((x, y), z)

------------------------------------------------------

{-# INLINE[2] void' #-}
void' = (>>== const (rtn ()))

{-# INLINE[2] bimap' #-}
bimap' :: A () t u -> A () v w -> A () (Pair t v) (Pair u w)
bimap' a a2 = void' (bimap a a2)

------------------------------------------------------

newtype Exclusive = Exclusive Handle deriving Storable

newtype Semiclosed = Semiclosed Handle deriving Storable

newtype Open p = Open Handle deriving Storable

class Openhandle h where
	getHdl :: h -> Handle

instance Openhandle Exclusive where
	getHdl (Exclusive h) = h

instance Openhandle (Open p) where
	getHdl (Open h) = h

{-# INLINE lift #-}
lift f = A $ \(Pair x (St world)) -> let
	IO g = f x
	(# world', (y, z) #) = g world in (Pair y (St world'), z)

open file mode = lift (\Blank -> liftM (\hdl -> (Exclusive hdl, ())) $ openFile file mode) . undrop1

getStdin = A (\Blank -> (Open stdin, ()))

getStdout = A (\Blank -> (Open stdout, ()))

getStderr = A (\Blank -> (Open stderr, ()))

close = drop1 . lift (\(Exclusive hdl) -> hClose hdl >> return (Blank, ()))

close1 = drop1 . lift (\(Semiclosed hdl) -> hClose hdl >> return (Blank, ()))

fileSize = lift (\h -> liftM ((,) h) (hFileSize (getHdl h)))

setFileSize sz = lift (\h -> hSetFileSize (getHdl h) sz >> return (h, ()))

eof = lift (\h -> liftM ((,) h) (hIsEOF (getHdl h)))

seek mode pos = lift (\h -> hSeek (getHdl h) mode pos >> return (h, ()))

tell = lift (\h -> liftM ((,) h) (hTell (getHdl h)))

char = lift (\h -> liftM ((,) h) (hGetChar (getHdl h)))

line = lift (\h -> liftM ((,) h) (hGetLine (getHdl h)))

lookahead = lift (\h -> liftM ((,) h) (hLookAhead (getHdl h)))

contents = lift (\(Exclusive hdl) -> liftM ((,) (Semiclosed hdl)) (hGetContents hdl))

putC c = lift  (\h -> hPutChar (getHdl h) c >> return (h, ()))

putS s = lift (\h -> hPutStr (getHdl h) s >> return (h, ()))

setBinary b = lift (\h -> hSetBinaryMode (getHdl h) b >> return (h, ()))

{-# NOINLINE random #-}
-- Random numbers have no interesting dependence on the world state,
-- so it is not threaded.
random rng = A (\Blank -> unsafePerformIO $ getStdGen >>= \g -> let (x, g') = randomR rng g in setStdGen g' >> return (Blank, x))

--------------------------------------------------------

instance Storable Blank where
	sizeOf _ = 0
	alignment _ = 1
	peek _ = return Blank
	poke _ Blank = return ()

align x y = ((sizeOf x - 1) `div` alignment y + 1) * alignment y

frst :: (Storable a, Storable b) => Ptr (Pair a b) -> Ptr a
frst = castPtr

secnd :: forall a b. (Storable a, Storable b) => Ptr (Pair a b) -> Ptr b
secnd = castPtr . (`plusPtr` align (undefined :: a) (undefined :: b))

instance (Storable a, Storable b) => Storable (Pair a b) where
	sizeOf _ = align (undefined :: a) (undefined :: b) + sizeOf (undefined :: b)
	alignment _ = alignment (undefined :: a)
		`lcm` alignment (undefined :: b)
	peek p = liftM2 Pair (peek (frst p)) (peek (secnd p))
	poke p (Pair x y) = do
		poke (frst p) x
		poke (secnd p) y

coerce :: Ptr Handle -> Ptr Int32
coerce = castPtr

instance Storable Handle where
	sizeOf _ = 4
	alignment _ = 4
	peek = peek . castPtr
	poke = poke . castPtr

-- | With the Fix constructor, I can build data structures of linear data.
data Fix f = In (f (Fix f))

fixInj1 :: Pointer p s (Fix f) -> Pointer p s (f (Fix f))
fixInj1 (Pointer fp p) = Pointer fp (castPtr p)

fixInj2 :: Pointer p s (f (Fix f)) -> Pointer p s (Fix f)
fixInj2 (Pointer fp p) = Pointer fp (castPtr p)

data Pointer p s t = Pointer !(ForeignPtr Blank) !(Ptr t)

instance Storable (Pointer p s t) where
	sizeOf _ = 8
	alignment _ = 4
	poke p (Pointer fp p2) = do
		sp <- newStablePtr fp
		pokeByteOff p 0 sp
		pokeByteOff p 4 p2
	peek p = do
		sp <- peekByteOff p 0
		fp <- deRefStablePtr sp
		freeStablePtr sp
		p2 <- peekByteOff p 4
		return (Pointer fp p2)

-- | Pointers can be linear, nonlinear, or focused. There are the following
--   tradeoffs:
--
--   * Linear pointers support strong update, but can only be split
--       under focusing.
--
--   * Nonlinear pointers can be split, but do not support strong update.
--
--   Placeholders classify pointers that either point to junk or to data that
--   is not allowed to be used (to maintain linearity).
data Linear = Linear

data Focused = Focused

data Nonlinear = Nonlinear

data Placeholder = Placeholder

class Splittable s

instance Splittable Nonlinear

instance Splittable Focused

{-# NOINLINE dummy #-}
dummy :: ForeignPtr Blank
dummy = unsafePerformIO (A.malloc >>= newForeignPtr_)

contraction :: A () (Pointer Nonlinear s t) (Pair (Pointer Nonlinear s t) (Pointer Nonlinear s t))
contraction = A (\p -> (Pair p p, ()))

class Weakening t where
	weakening :: A () (Pair t St) St

instance Weakening (Pointer p Focused t) where
	weakening = A (\(Pair (Pointer _ _) st) -> (st, ()))

instance Weakening (Pointer p Nonlinear t) where
	weakening = drop1 . lift (\(Pointer fp _) -> touchForeignPtr fp >> return (Blank, ()))

instance Weakening (Open p) where
	weakening = A (\(Pair (Open _) st) -> (st, ()))

-- | Allocate a new linear block (containing junk), Use 'poke'' to initialize it.
{-# NOINLINE new #-}
new :: (Storable t) => A () St (Pair (Pointer p Placeholder t) St)
new = lift (\Blank -> liftM (\p -> (Pointer dummy p, ())) A.malloc) . undrop1

-- | Use 'peek'' to take ownership of the contents of a block before freeing it.
free :: A () (Pair (Pointer p2 Placeholder t) St) St
free = drop1 . lift (\(Pointer _ p) -> A.free p >> return (Blank, ()))

-- | Split a pointer to a pair, into a pair of pointers.
split :: forall t u p s. (Storable t, Storable u, Splittable s) => A () (Pointer p s (Pair t u)) (Pair (Pointer p s t) (Pointer p s u))
split = A (\(Pointer fp p) -> (Pair
	(Pointer fp (frst p))
	(Pointer fp (secnd p)), ()))

ptrSwap ::  (Storable t) => Fn (Pair (Pointer p s t) t) (Pair (Pointer p s t) t)
ptrSwap = lift (\(Pair ptr@(Pointer _ p) x) -> peek p >>= \y -> poke p x >> return (Pair ptr y, ()))

-- | Focusing on a pointer.
--
--   Temporarily turns a linear pointer into a focused pointer. I get the linear
--   pointer back after all copies have been surrendered (with 'weakening').
focus :: (forall p. A a (Pair (Pointer p Focused t) u) v)
	-> A a (Pair (Pointer p s t) u) (Pair (Pointer p s t) v)
focus (A f) = A (\(Pair ptr@(Pointer fp p) x) -> first (Pair ptr) (f (Pair (Pointer fp p) x)))

-- | Focusing on a handle.
focusHdl :: (forall p. A a (Pair (Open p) t) u) -> A a (Pair Exclusive t) (Pair Exclusive u)
focusHdl (A f) = A (\(Pair h@(Exclusive hdl) x) -> first (Pair h) (f (Pair (Open hdl) x)))

-- | Take the data out of a block, making it a placeholder.
peek' :: (Storable t) => Fn (Pointer p Linear t) (Pair (Pointer p Placeholder t) t)
peek' = lift (\(Pointer fp p) -> liftM (\x -> (Pair (Pointer fp p) x, ())) (peek p))

-- | The reverse operation.
poke' :: (Storable t) => Fn (Pair (Pointer p Placeholder t) t) (Pointer p Linear t)
poke' = lift (\(Pair (Pointer fp p) x) -> poke p x >> return (Pointer fp p, ()))

-- | A placeholder block can change its type.
changeType :: forall t u p. (Storable t, Storable u) => A () (Pointer p Placeholder t) (Pointer p Placeholder u)
changeType = if sizeOf (undefined :: u) <= sizeOf (undefined :: t) then
		A (\(Pointer fp p) -> (Pointer (castForeignPtr fp) (castPtr p), ()))
	else
		error "Control.Linear.changeType: value won't fit"

-- Linearity ensures that a program must touch the pointer in order to dispose of it.
-- | Allocate a nonlinear pointer.
{-# NOINLINE newNonlinear #-}
newNonlinear :: (Storable t) => t -> A () Blank (Pointer p Nonlinear t)
newNonlinear x = A (\Blank -> unsafePerformIO $ do
	p <- A.malloc
	poke p x
	fp <- newForeignPtr_ p
	return (Pointer (castForeignPtr fp) p, ()))

peek1 :: (Storable t) => A t (Pair (Pointer Nonlinear s t) St) (Pair (Pointer Nonlinear s t) St)
peek1 = lift (\ptr@(Pointer _ p) -> liftM (\x -> (ptr, x)) $ peek p)

poke1 :: (Storable t) => t -> Fn (Pointer p s t) (Pointer p s t)
poke1 x = lift (\ptr@(Pointer _ p) -> poke p x >> return (ptr, ()))

-- | Duplicate the world state. This is interpreted as creating a thread.
fork :: A () St (Pair St St)
fork = A (\st -> (Pair st st, ()))

-- St --------new----X
--              \
--               \
--                \
-- St ------------free----- St
--
-- By exchanging a pointer,
-- | Sync together two world states.
{-# NOINLINE join' #-}
join' :: A () (Pair St St) St
join' = A (\(Pair _ st) -> (st, ())) . bimap' id free . assoc1 . bimap' (swap . (new :: A () St (Pair (Pointer p Placeholder Blank) St))) id

------------------------------------------------------
--- Sample programs

helloWorld = undrop1
	>>> bimap' getStdout id
	>>> putS "Hello world!\n"
	>>> weakening

printStuff = undrop1
	>>> bimap' getStdout id
	>>> iterate (putS "Stuff\n" >>>) id !! 10000
	>>> weakening

concurrent = fork
	>>> bimap' (open "C:\\users\\james\\videos\\Biggest number.wmv" ReadMode) printStuff
	>>> bimap' (contents >>== \text -> last text `seq` close1 >>> undrop1 >>> bimap' getStdout id >>> putS (take 10000 text)) id
	>>> bimap' weakening id
	>>> join'