module BiArrow

import StdGeneric

from StdInt import 
	class toInt(..), class toChar(..), class isOdd(..),
	class +(..), class -(..), class *(..), class /(..),
	instance toInt Char, instance isOdd Int,
	instance + Int, instance - Int, instance * Int, instance / Int	, instance == Int
from StdChar import isLower, isUpper, instance toChar Int, instance == Char
from StdBool import not

from StdTuple import fst, snd, uncurry, curry
from StdList import hd, take, drop, ++, flatten, repeatn, class length(..), instance length [],
	class ==(..), instance == []
from StdFunc import o, id, const
from StdMisc import abort

:: Void = Void
:: Either a b = Left a | Right b
:: Maybe a = Nothing | Just a

derive bimap Maybe

class Arrow arr where
	arr :: (a -> b) -> arr a b
	(>>>) infixr 1 :: (arr a b) (arr b c) -> arr a c
	first :: (arr a b) -> arr (a, c) (b, c)
	
// BiArrow class

class BiArrow arr | Arrow arr where
	(<->) infix 8 :: (a -> b) (b -> a) -> arr a b
	inv :: (arr a b) -> arr b a

arrA :: (a -> b) -> arr a b | BiArrow arr
arrA f = f <-> const (abort "arr has no inverse")

second :: (arr a b) -> arr (c, a) (c, b) | BiArrow, Arrow arr
second f = swap <-> swap >>> first f >>> swap <-> swap

(***) infix 2 :: (arr a b) (arr c d) -> arr (a, c) (b, d) | BiArrow, Arrow arr
(***) f g = first f >>> second g

idA :: arr a a | BiArrow arr
idA = id <-> id
	

// Arrow class

class ArrowChoice arr where
	left :: (arr a b) -> arr (Either a c) (Either b c)

right :: (arr a b) -> arr (Either c a) (Either c b) | ArrowChoice, BiArrow, Arrow arr
right f = mirror <-> mirror >>> left f >>> mirror <-> mirror

(+++) infix 2 :: (arr a b) (arr c d) -> arr (Either a c) (Either b d) | ArrowChoice, BiArrow, Arrow arr
(+++) f g = left f >>> right g

// ArrowZero class

class ArrowZero arr | Arrow arr where
	zeroArrow :: arr a b

// function arrow

instance Arrow (->) where
	arr f = f
	(>>>) f g = g o f
	first f = f <*> id

instance ArrowChoice (->) where
	left f = f <+> id

(`split`) infixl 9 :: (a -> b) (a -> c) a -> (b, c)
(`split`) f g t = (f t, g t)

(`either`) infixl 9 :: (a -> b) (c -> b)(Either a c) -> b
(`either`) f g (Left x)		= f x
(`either`) f g (Right y)	= g y


swap :: ((a, b) -> (b, a))
swap = snd `split` fst

mirror :: ((Either a b) -> (Either b a))
mirror = Right `either` Left

swapA = swap <-> swap
mirrorA = mirror <-> mirror

(<*>) :: (a -> b) (c -> d) -> (a, c) -> (b, d)
(<*>) f g = (f o fst) `split` (g o snd)

(<+>) :: (a -> b) (c -> d) -> (Either a c) -> (Either b d)
(<+>) f g = (Left o f) `either` (Right o g)

assocSA = (Left o Left) `either` ((Left o Right) `either` Right)
			<->
		  (Left `either` (Right o Left)) `either` (Right o Right)
		  
assocPA = (fst o fst) `split` ((snd o fst) `split` snd)
		  	 <->
		  (fst `split` (fst o snd)) `split` (snd o snd)

swapXYA :: arr (a,(b,c)) (b,(a,c)) | BiArrow arr
swapXYA = inv assocPA >>> first swapA >>> assocPA
swapYZA = assocPA >>> second swapA >>> inv assocPA

(<<<) infixl 1
(<<<) f g = g >>> f

lawP4L f = first (first f) >>> assocPA
lawP4R f = assocPA >>> first f

lawS4L f = left (left f) <<< assocSA
lawS4R f = assocSA <<< left f

// embedded-projection arrow

:: EP arr a b = EP (arr a b) (arr b a)

derive bimap EP

ep :: !(EP arr a b) -> arr a b
ep (EP f f`) = f

pe :: !(EP arr a b) -> arr b a
pe (EP f f`) = f`

instance Arrow (EP arr) | Arrow arr where
	arr f = arrA f
	(>>>) f g = EP (ep f >>> ep g) (pe g >>> pe f)
	first f = EP (first (ep f)) (first (pe f))

instance BiArrow (EP arr) | Arrow arr where
	(<->) f f` = EP (arr f) (arr f`)
	inv f = EP (pe f) (ep f)

instance ArrowChoice (EP arr) | ArrowChoice arr where
	left f = EP (left (ep f)) (left (pe f))

// reverse example


list2EitherA = list_either <-> either_list
	where
		list_either  []			= Left  Void
		list_either  [x:xs]		= Right (x, xs)
	
		either_list (Left Void)		= []
		either_list (Right (x, xs))	= [x:xs]


($) infixl 0
($) f x = f x

liftRSA :: arr (a, Either b c) (Either (a, b) (a, c)) | BiArrow arr 
liftRSA = liftr <-> rtfil
    where
        liftr = uncurry (uncurry (<+>) o (pair `split` pair))
        rtfil =  (id <*> Left) `either` (id <*> Right)
		pair x y = (x,y)

liftLSA :: arr (Either a b, c) (Either (a, c) (b, c)) | BiArrow, ArrowChoice arr
liftLSA = swapA >>> liftRSA >>> (swapA +++ swapA)
 
reverseA :: arr [a] [a] | ArrowChoice, BiArrow, Arrow arr
reverseA =	list2EitherA
		>>>	right (second reverseA >>> appElemA)
		>>>	inv list2EitherA


appElemA = second list2EitherA >>> liftRSA >>>
				right (swapXYA >>> second appElemA) >>>
			inv (second list2EitherA >>> liftRSA)



reverse_example = ep (inv reverseA) [1, 2, 3]

appelem_example = ep appElemA (4, [1, 2, 3])
// map

generic mapl t1 t2 :: arr t1 t2 | ArrowChoice, BiArrow, Arrow arr

mapl{|UNIT|} = idA
mapl{|PAIR|} mapl_a mapl_b = inv prodA >>> mapl_a *** mapl_b >>> prodA

(`splt`) infix 9
(`splt`) f g p = PAIR (f p) (g p)
exl (PAIR x y) = x
exr (PAIR x y) = y

(`junc`) infix 9
(`junc`) f g (LEFT l) = f l
(`junc`) f g (RIGHT r) = g r

prodA :: arr (a, b) (PAIR a b) | BiArrow arr
prodA = (fst `splt` snd) <-> (exl `split` exr)
	
mapl{|EITHER|} mapl_a mapl_b = inv sumA >>> mapl_a +++ mapl_b >>> sumA

sumA :: arr (Either a b) (EITHER a b) | BiArrow arr
sumA = (LEFT `either` RIGHT) <-> (Left `junc` Right)

mapl{|OBJECT|} mapl_o = inv objA >>> mapl_o >>> objA

objA :: arr a (OBJECT a) | BiArrow arr
objA = obj <-> jbo
	where
		obj x = OBJECT x
		jbo (OBJECT x) = x

mapl{|CONS|} mapl_o = inv consA >>> mapl_o >>> consA

consA :: arr a (CONS a) | BiArrow arr
consA = cons <-> snoc
	where
		cons x = CONS x
		snoc (CONS x) = x

derive mapl []

mapr :: (arr a b) -> arr (t a) (t b) | mapl{|*->*|} t & ArrowChoice, BiArrow, Arrow, bimap{|*->*->*|} arr
mapr f = inv (mapl{|*->*|} (inv f))

:: Tree a = Leaf a | (Node) infixl (Tree a) (Tree a)

derive mapl Tree 
	
map_example = ep (mapl{|*->*|} ((\x -> x + 1) <-> (\x -> x - 1))) (Leaf 1 Node Leaf 2 Node Leaf 3)

// state arrow

:: S s arr a b = S (arr (a, s) (b, s))

derive bimap (,), S

s :: !(S s arr a b) -> arr (a, s) (b, s)
s (S f) = f

instance Arrow (S s arr) | BiArrow, Arrow arr where
	arr f = S (first (arr f))
	(>>>) f g = S (s f >>> s g)
	first f = S (swapYZA >>> first (s f) >>> swapYZA)


instance BiArrow (S s arr) | BiArrow, Arrow arr where
	(<->) f g = S (first (f <-> g))
	inv f = S (inv (s f))

instance ArrowChoice (S s arr) | ArrowChoice, BiArrow, Arrow arr where
	left f = S (liftLSA >>> left (s f) >>> inv liftLSA)

/*
class IO m where
	get :: (m a) -> (a, m Void)
	put :: (a, m Void) -> m a


class Adapt m where
	pushA :: arr (m (a,b) c) (m a c, b)
	liftA :: arr (Either (m a c) (m b c)) (m (Either a b) c)
*/		

// shape

getputA :: S [a] arr Void a | BiArrow arr
getputA = S (get <-> put)
	where
		get (Void, [x:xs]) = (x, xs)
		put (x, xs) = (Void, [x:xs])

//combine :: S [a] arr (t Void) (t a) | MaplC t & ArrowChoice, BiArrow, Arrow arr
combine = maplc getputA

//separate :: S [a] arr (t a) (t Void) | mapl{|*->*|} t & ArrowChoice, BiArrow, Arrow arr
separate = inv combine

shape_example = (ep o s) combine (Leaf Void Node Leaf Void Node Leaf Void, [3, 4, 5])

// (de)serialisation

int2KBitsA :: Int -> arr Int [Bool] | BiArrow arr
int2KBitsA k = int2bits k <-> bits2int k
	where
		int2bits 0 n = []
		int2bits k n = [isOdd n:int2bits (k-1) (n / 2)]
		bits2int 0 bs = 0
		bits2int k [b:bs] = (if b 1 0) + bits2int (k-1) bs * 2


//decodeInt :: Int -> S [Bool] arr Void Int | BiArrow, Arrow, ArrowChoice arr
decodeInt k = createShapeA k >>> combine >>> inv (int2KBitsA k)
where
	createShapeA :: Int -> arr Void [Void] | BiArrow arr
	createShapeA size = (\Void -> (repeatn size Void)) <->
						(\l -> if (length l == size) (const Void) abort "cannot occur")

//encodeInt :: Int -> S [Bool] arr Int Void | BiArrow, Arrow, ArrowChoice arr
encodeInt k = inv (decodeInt k)

generic decode t :: S [Bool] arr Void t | ArrowChoice, BiArrow, Arrow arr

decode{|UNIT|} = voidUnitA

decode{|Int|} = decodeInt 32

decode{|Char|} = decodeInt 8 >>> toChar <-> toInt

decode{|Bool|} = getputA

decode{|PAIR|} decode_a decode_b = dupVoidA >>> decode_a *** decode_b >>> prodA

decode{|EITHER|} decode_a decode_b = getputA >>> bool2EitherA >>> decode_a +++ decode_b >>> sumA

decode{|OBJECT|} decode_a = decode_a >>> objA

decode{|CONS|} decode_a = decode_a >>> consA

voidUnitA	= (\_ -> UNIT) <-> (\_ -> Void)
dupVoidA	= (\_ -> (Void, Void)) <-> (\_ -> Void)

bool2EitherA = bool2either <-> either2bool
	where
		bool2either b	= if b (Right Void) (Left Void)
		either2bool		= const False `either` const True 

derive decode Tree

encode :: S [Bool] arr t Void | decode{|*|} t & ArrowChoice, BiArrow, Arrow, bimap{|*->*->*|} arr
encode = inv decode{|*|}

encode_example = (length o snd) ((ep o s) encode (Leaf 1 Node Leaf 2 Node Leaf 3, []))

// zip

generic zip t1 t2 t3 :: arr (t1, t2) t3 | ArrowZero, ArrowChoice, BiArrow arr

zip{|UNIT|} = (\_ -> UNIT) <-> (\_ -> (UNIT, UNIT))

zip{|PAIR|} zip_a zip_b = unprod2A >>> zip_a *** zip_b >>> prodA

unprod2A = dorp <-> prod
	where
		dorp (PAIR x1 x2, PAIR y1 y2) = ((x1, y1) , (x2, y2))
		prod ( (x1, y1), (x2, y2) ) = (PAIR x1 x2, PAIR y1 y2)

zip{|OBJECT|} zip_a = unobj2A >>> zip_a >>> objA

unobj2A = jbo <-> obj
	where
		jbo (OBJECT x1, OBJECT y1) = (x1, y1)
		obj (x1, y1) = (OBJECT x1, OBJECT y1)


zip{|CONS|} zip_a = uncons2A >>> zip_a >>> consA

uncons2A = snoc <-> cons
	where
		snoc (CONS x1, CONS y1) = (x1, y1)
		cons (x1, y1) = (CONS x1, CONS y1)


unzip f = inv (zip{|*->*|} f)

// zip with zero

(||>) infix 4 :: (arr b c) (arr d c) -> arr (Either b d) c | ArrowChoice, BiArrow, Arrow arr
(||>) f g = f +++ g >>> untagRA

untagRA = (id `either` id) <-> Right

zip{|EITHER|} zip_a zip_b = unsum2FA >>> zeroArrow ||> (zip_a +++ zip_b) >>> sumA
where
	unsum2FA = mus <-> sum
		where
			mus (LEFT l1, LEFT l2) = Right (Left (l1, l2) )
			mus (RIGHT r1, RIGHT r2) = Right (Right (r1, r2) )
			mus (s1, s2) = Left (s1, s2)
			sum (Right (Left (l1, l2) ) ) = (LEFT l1, LEFT l2)
			sum (Right (Right (r1, r2) ) ) = (RIGHT r1, RIGHT r2)
			sum (Left (s1, s2) ) = (s1, s2)

// Monad(Plus) class

class Monad m where
	return :: a -> m a
	(>>=) :: (m a) (a -> m b) -> m b

class MonadPlus m | Monad m  where
	mzero :: m a
	mplus :: (m a) (m a) -> m a

liftM :: (a -> b) -> (m a) -> m b | Monad m
liftM f = \m -> m >>= \a -> return (f a)

//lift2M :: (a -> b) -> (m a) -> m b | Monad m

// monadic arrow

class MaplC m where 
	maplc :: (arr a b) -> arr (m a) (m b) | ArrowChoice, BiArrow, Arrow, bimap{|*->*->*|} arr

instance MaplC Maybe where
	maplc f = mapl{|*->*|} f

instance MaplC Tree where
	maplc f = mapl{|*->*|} f

instance MaplC [] where
	maplc f = mapl{|*->*|} f
	
derive mapl Maybe

instance Monad Maybe where
	return x = Just x
	(>>=) (Just x) g = g x
	(>>=) Nothing g = Nothing

instance MonadPlus Maybe where
	mzero = Nothing
	mplus (Just f) g = Just f
	mplus Nothing g = g

:: M m arr a b = M (arr (m a) (m b))

derive bimap M

m :: !(M m arr a b) -> arr (m a) (m b)
m (M f) = f

(=<<) f m = m >>= f

firstMA = joinP <-> splitP
	where
		joinP	= (=<<) (\(mx, y) -> mx >>= \x -> return (x, y))
		splitP	= (=<<) (\(x, y) -> return (return x, y))

leftMA = joinS <-> splitS
	where
		joinS   = (=<<) ((=<<) (return o Left) `either` (return o Right))
		splitS  = (=<<) ((return o Left o return) `either` (return o Right))


instance Arrow (M m arr) | ArrowChoice, BiArrow, Arrow, bimap{|*->*->*|} arr & Monad, MaplC m where
	arr f = arrA f
	(>>>) f g = M (m f >>> m g)
	first f = M (inv firstMA >>> maplc (first (m f)) >>> firstMA)
	
instance BiArrow (M m arr) | BiArrow, bimap{|*->*->*|}arr & Monad, MaplC m where
	(<->) f g = M (liftM f <-> liftM g)
	inv f = M (inv (m f))

instance ArrowChoice (M m arr) | ArrowChoice, BiArrow, Arrow, bimap{|*->*->*|} arr & Monad, MaplC m where
	left f = M (inv leftMA >>> maplc (left (m f)) >>> leftMA)

instance ArrowZero (M m arr) | BiArrow arr & MonadPlus m where
	zeroArrow = M ((const mzero) <-> (const mzero))

derive zip Tree

zip_example = (ep o m) (zip{|*->*|} idA) (Just (Leaf 1 Node Leaf 3, Leaf 2 Node Leaf 4))

monad_example = (ep o m) (zip{|*->*|} idA) (Just (Leaf 1 Node Leaf 3, Leaf 2))
/*
instance MaplC [] where
	maplc f = mapl{|*->*|} f
*/	
instance Monad [] where
	return x = [x]
	(>>=) xs g = flatten [g x \\ x <- xs]

instance MonadPlus [] where
	mzero		= []
	mplus f g	= f ++ g
/*
monad_example = (ep o m) (inv (zip{|*->*|} idA)) ([Leaf (1, 2) Node Leaf (3, 4), Leaf (8, 9)])
*/
// main

// 

class ArrowPlus arr | Arrow arr where
	(+>) infixl 4 ::	(arr a b) (arr a c) -> arr a (Either b c)


// Instances of ArrowZero and ArrowPlus for S

instance ArrowZero (S s arr) | ArrowZero arr 
where
	zeroArrow = S (first zeroArrow)

instance ArrowPlus (S s arr) | ArrowPlus, BiArrow, ArrowChoice arr where
	(+>) f g = S ((s f +> s g) >>> inv liftLSA)

// Instance of ArrowPlus for M

inlMA = inlM <-> uninlM
where
	inlM  	=  (=<<) (return o Left)
	uninlM 	=  (=<<) (return `either` const mzero)


inrMA = inrM <-> uninrM
where
	inrM 	= (=<<) (return o Right)
	uninrM 	= (=<<) (const mzero `either` return)

dupMA = (\x->(x,x)) <-> (uncurry mplus)

instance ArrowPlus (M mon arr) | BiArrow arr & MonadPlus mon where
	(+>) l r = M (dupMA >>> ((m l >>> inlMA) *** (m r >>> inrMA)) >>> (inv dupMA))

	
::	Expression
		= App Expression Expression
		| Nested Expression
		| Lambda [Char] Expression
		| Variable		[Char]
		| Constructor	[Char]

::	Token = Id_T [Char] | Lambda_T | Open_T | Close_T | Arrow_T | EOF_T

instance == Token
where
	(==) Lambda_T	Lambda_T	= True
	(==) Open_T		Open_T 		= True
	(==) Close_T	Close_T		= True
	(==) Arrow_T	Arrow_T		= True
	(==) (Id_T x) 	(Id_T y)	= x == y
	(==) EOF_T 		EOF_T		= True
	(==) _ 			_ 			= False

:: Parser arr t :==  S [Token] arr Void t

(>**) infixl 6 :: (a Void b) (a Void c) -> a Void (b,c) | BiArrow a
(>**) f g = dupVoidA >>> (f *** g)

parseVariable		= parserIdentifier (isLower o hd)
parseConstructor	= parserIdentifier (isUpper o hd)

isLowerId [c:cs] = isLower c

parserIdentifier p = getputA >>> tagIDA p >>> (zeroArrow ||> idA)
	where
		tagIDA p = tagID p  <-> (id `either` Id_T)

		tagID p (Id_T name)	| p name = Right name
		tagID _ token                = Left token

parseOneOrMore p = (p >** parseOneOrMore p) +> p >>> untagListA
where
	untagListA = untag <-> tag
	where
		untag (Left  (x, (y, l)))	= (x, [y:l])
		untag (Right  x)			= (x, [])
	 
		tag (x, [y:l]) 	= Left (x, (y, l))
		tag (x, []) 	= Right x

parseExpression = parseOneOrMore parseTerm >>> toExpressionA
	where
		toExpressionA = uncurry to_apply <-> from_apply [] 
		where
			to_apply app []		= app
			to_apply app [x:xs]	= to_apply (App app x) xs
			
			from_apply l (App f a)  = from_apply [a:l] f
			from_apply l t 			= (t, l)


parseTerm = parseNested +> parseLambda +> parseVariable +> parseConstructor >>> to_expr <-> from_expr
	where
		to_expr = Nested `either` uncurry Lambda `either` Variable `either` Constructor

		from_expr (Lambda var expr)		= Left (Left (Right (var, expr)))
		from_expr (Variable var)		= Left (Right var)
		from_expr (Constructor cons)	= Right cons
		from_expr (Nested nested)		= Left (Left (Left nested))		

parseLambda = (parseKeyword Lambda_T >** parseVariable >** parseKeyword Arrow_T >** parseExpression)
		>>> (to_lambda <-> from_lambda)
	where
		to_lambda	(((_,v),_),e)	= (v, e) 
		from_lambda = const Lambda_T `split` fst  `split` const Arrow_T `split` snd
		

parseNested = (parseKeyword Open_T >** parseExpression >** parseKeyword Close_T) >>> (to_expr <-> from_expr)
	where
		to_expr ((_,e), _)	= e 
		from_expr 			= const Open_T `split` id `split` const Close_T 

parseKeyword token
	= getputA >>> tagTokenA token >>> (zeroArrow ||> idA)
where
	tagTokenA t = tag t <-> (id `either` id)
	
	tag t1 t2 = if (t1 == t2) (Right t2) (Left t2)

tokens	= [Open_T,Lambda_T,Id_T ['x'],Arrow_T,Id_T ['x'],Close_T,Id_T ['y'],EOF_T]
expr	= Lambda ['x'] (Lambda ['xs']
				(App (App (Constructor ['Cons']) (Variable ['x'])) (Variable ['xs'])))
expr2	= App (Lambda ['x'] (Variable ['x']))(Lambda ['y'] (Variable ['y']))
//expr2	= App (Nested (Lambda ['x'] (Variable ['x'])))(Lambda ['y'] (Variable ['y']))
tokens2	= [Open_T,Lambda_T,Id_T ['x'],Arrow_T,Id_T ['x'],Close_T,Lambda_T,Id_T ['y'],Arrow_T,Id_T ['y'],EOF_T]
tokens3	= [Lambda_T,Id_T ['x'],Arrow_T,Id_T ['x'],Lambda_T,Id_T ['y'],Arrow_T,Id_T ['y'],EOF_T]

parse = parseExpression >** parseKeyword EOF_T >>> eofA
    where
        eofA = fst <-> (\x -> (x, EOF_T))

print = (inv parse)

test_parse ::  [(Expression, [Token])]
test_parse = (s >>> m >>> ep) parse   (return (Void, tokens3))


test_print ::  [(Void, [Token])]
test_print = (s >>> m >>> ep) print   (return (expr2, []))

//print_parse ::  Maybe (Expression, [Token])

print_parse ::  [(Expression, [Token])]
print_parse = (s >>> m >>> ep) (parse <<< print) (return (expr2, []))

Start = (appelem_example,
	(reverse_example, map_example, shape_example, zip_example, monad_example),
	(test_parse, "\n\n", test_print, "\n\n", print_parse))