module a11

import StdEnv

import Data.Functor
import Control.Applicative
import Control.Monad => qualified join
import Control.Monad.Trans
import Control.Monad.State
import Data.Maybe
import Data.Error
import Data.Either
import Data.Func
import Text

:: Step pre post = Step
:: High = High
:: Low = Low

class action v
where
	moveToShip :: v (Step High High)
	moveToQuay :: v (Step High High)
	moveUp :: v (Step Low High)
	moveDown :: v (Step High Low)
	lock :: v (Step Low Low)
	unlock :: v (Step Low Low)
	wait :: v (Step a a)
	(:.) infixl 1 :: (v (Step a b)) (v (Step b c)) -> v (Step a c)
	While :: (v Bool) (v (Step a a)) -> v (Step a a)

class expr v
where
	containersBelow :: v Int
	lit :: t -> v t | toString t
	(<.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
	(>.) infix 4 :: (v t) (v t) -> (v Bool) | Ord t
	(+.) infix 4 :: (v t) (v t) -> (v t) | + t

:: Var a = Var Int
class var v
where
	def :: (v t) ((v (Var t)) -> (v (Step a b))) -> v (Step a b) | TC t
	var :: (v (Var t)) -> v t | TC t
	(=.) infixr 2 :: (v (Var t)) (v t) -> v (Step a a) | TC t

//Printing
:: Printer a = P (Int Int [String] -> [String])
runPrinter (P a) = a 0 0

word :: String -> Printer a
word s = P \v i c->[createArray i '\t',s:c]

instance action Printer
where
	moveToShip = word "moveToShip"
	moveToQuay = word "moveToQuay"
	moveUp = word "moveUp"
	moveDown = word "moveDown"
	lock = word "lock"
	unlock = word "unlock"
	wait = word "wait"
	(:.) (P a) (P b) = P \v i c->a v i [":.\n":b v i c]
	While (P b) (P a) = P \v i c->["while (":b v 0 [")\n":a v (i+1) ["\n)":c]]]

instance expr Printer
where
	containersBelow = P \v i c->["containerBelow":c]
	lit x = P \v i c->[toString x:c]
	(<.) (P x) (P y) = P \v i c->x v i [" < ":y v i c]
	(>.) (P x) (P y) = P \v i c->x v i [" > ":y v i c]
	(+.) (P x) (P y) = P \v i c->x v i [" + ":y v i c]

varname i = "v" +++ toString i
instance var Printer
where
	def (P e) fun = P \v i c->[createArray i '\t',"def ":e v i [" \\",varname v,".\n":let (P f) = fun (P \_ i c->[varname v:c]) in f (inc v) i c]]
	var (P e) = P e
	(=.) (P a) (P b) = P \v i c->[createArray i '\t':a v i [" = ":b v i c]]

//Evaluating
:: Eval a :== StateT SemState (Either String) a
cast f = f >>| pure Step
fail s = liftT (Left s)
runEval = runStateT
instance action (StateT SemState (Either String))
where
	moveToShip = modify (\s->{s & craneOnQuay=False})
	moveToQuay = cast $ modify (\s->{s & craneOnQuay=True})
	moveUp     = cast $ modify (\s->{s & craneUp=True})
	moveDown   = cast $ modify (\s->{s & craneUp=False})
	lock       = cast $ getState >>= \s->case s of
		{locked=Just _}                   = fail "Already locked"
		{craneOnQuay=True,onQuay=[]}      = fail "No container to lock to"
		{craneOnQuay=False,onShip=[]}     = fail "No container to lock to"
		{craneOnQuay=True,onQuay=[x:xs]}  = put {s & onQuay=xs,locked=Just x}
		{craneOnQuay=False,onShip=[x:xs]} = put {s & onShip=xs,locked=Just x}
		_                                 = fail "Shouldn't happen"
	unlock       = cast $ getState >>= \s->case s of
		{locked=Nothing}                  = fail "Already unlocked"
		{craneOnQuay=True,locked=Just x}  = put {s & onQuay=[x:s.onQuay],locked=Nothing}
		{craneOnQuay=False,locked=Just x} = put {s & onShip=[x:s.onShip],locked=Nothing}
		_                                 = fail "Shouldn't happen"
	wait = pure Step
	(:.) x y = cast $ x >>| y
	While x y = x >>= \b->if b (y :. (While x y)) (pure Step)

instance expr (StateT SemState (Either String))
where
	containersBelow = gets (\s->length if s.craneOnQuay s.onQuay s.onShip)
	lit x = pure x
	(<.) x y = (<) <$> x <*> y
	(>.) x y = (>) <$> x <*> y
	(+.) x y = (+) <$> x <*> y

instance var (StateT SemState (Either String))
where
	def d fun = d >>= \v->gets (\s->length s.variables) >>= \i->modify (\s->{s & variables=s.variables ++ [dynamic v]}) >>| fun (pure (Var i))
	var a = a >>= \(Var i)->gets (\s->s.variables !! i) >>= cast
	where
		cast :: Dynamic -> StateT SemState (Either String) a | TC a
		cast (a :: a^) = pure a
		cast_ =  fail "Something went horribly wrong"
	(=.) a b = cast $ a >>= \(Var i)->b >>= \v->modify (\s->{s & variables=updateAt i (dynamic v) s.variables})

:: SemState =
	{ onShip      :: [String]
	, onQuay      :: [String]
	, craneUp     :: Bool
	, craneOnQuay :: Bool
	, locked      :: Maybe String
	, variables   :: [Dynamic]
	}

state0 =
	{ onShip = []
	, onQuay = ["apples","beer","camera's"]
	, craneUp = True
	, craneOnQuay = True
	, locked = Nothing
	, variables = []
	}

/*
//Optimization
:: BM a b =
	{ t2 :: A.v: (v a) -> v b
	, f2 :: A.v: (v b) -> v a
	}
:: Opt a
	//Actions
	= OMoveToShip (BM a (Step High High))
	| OMoveToQuay (BM a (Step High High))
	| OMoveUp (BM a (Step Low High))
	| OMoveDown (BM a (Step High Low))
	| OLock (BM a (Step Low Low))
	| OUnlock (BM a (Step Low Low))
	| E.e: OWait (BM a (Step e e))
	| E.e b: OWhile (BM b Bool) (BM a (Step e e)) (Opt b) (Opt a)
	| E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
	//Expressions
	| OContainersBelow (BM a Int)
	| E.b: OLit (BM a b) b                   & toString b
	| E.b: OLe (BM a Bool) (Opt b) (Opt b)   & Ord b
	| E.b: OGe (BM a Bool) (Opt b) (Opt b)   & Ord b
	| E.b: OPlus (BM a b) (Opt b) (Opt b)    & + b
	//Variables
	| E.b: OVar (BM a b) (Opt (Var b))       & TC b
	| E.b e: OAssign (BM a (Step e e)) (Opt (Var b)) (Opt b) & TC b
	| E.e b c: ODef (BM a (Step b c)) (Opt e) ((Opt (Var e)) -> (Opt (Step b c))) & TC e

instance action Opt
where
	moveToShip = OMoveToShip bm
	moveToQuay = OMoveToQuay bm
	moveUp = OMoveUp bm
	moveDown = OMoveDown bm
	lock = OLock bm
	unlock = OUnlock bm
	wait = OWait bm sbm
	(:.) a b = OSeq bm a b
	While a b = OWhile bm bm a b

instance expr Opt
where
	containersBelow = OContainersBelow bm
	lit x = OLit bm x
	(<.) a b = OLe bm a b
	(>.) a b = OGe bm a b
	(+.) a b = OPlus bm a b

instance var Opt
where
	def a b = ODef bm a b
	var v = OVar bm v
	(=.) a b = OAssign bm a b

opti :: (Opt a) -> v a | action, expr, var v
//Action
opti (OMoveToShip bm) = bm.f2 moveToShip
opti (OMoveToQuay bm) = bm.f2 moveToQuay
opti (OMoveDown bm) = bm.f2 moveDown
opti (OMoveUp bm) = bm.f2 moveUp
opti (OLock bm) = bm.f2 lock
opti (OUnlock bm) = bm.f2 unlock
opti (OWait bm sbm) = bm.f2 wait
opti (OWhile bm1 bm2 p a) = bm2.f2 (While (opti (bm1.t2 p)) (opti (bm2.t2 a)))
//opti (OSeq bm1 (OWait bm2) r) =
/*
l :: (Step pre inter)
| E.pre post inter: OSeq (BM a (Step pre post)) (Opt (Step pre inter)) (Opt (Step inter post))
bm2 :: BM (Step pre inter)
| E.e: OWait (BM (Step inter post) (Step post post)) (SBM inter post)

need:
:: BM (Step pre inter) (Step pre post)
*/
opti (OSeq bm1 l (OWait bm2 sbm)) = bm.f2 (opti (sbm.st2 l))
opti (OSeq bm l r) = bm.f2 (opti l :. opti r)
//Expr
opti (OContainersBelow bm) = bm.f2 containersBelow
opti (OLit bm x) = bm.f2 (lit x)
opti (OLe bm x y) = bm.f2 (opti x <. opti y)
opti (OGe bm x y) = bm.f2 (opti x >. opti y)
opti (OPlus bm x y) = bm.f2 (opti x +. opti y)
//Variables
opti (OVar bm v) = bm.f2 (var (opti v))
opti (OAssign bm a b) = bm.f2 (opti a =. opti b)
//opti (ODef bm a b) = bm.f2 (def (opti a) \v->opti (b (OVar bm v))
//

Start :: [String]
Start = runPrinter (opti (loadShip)) []
*/

Start = 42
	
loadShip =
	While (containersBelow >. lit 0) (
		moveDown:.
		lock:.
		moveUp:.
		moveToShip:.
		wait:.
		moveDown:.
		wait:.
		unlock:.
		moveUp:.
		moveToQuay
	)

loadShip2 =
	def containersBelow \n.
	def (lit 0) \m.
	While (var n >. lit 0) (
		moveDown:.
		lock:.
		moveUp:.
		moveToShip:.
		wait:.
		moveDown:.
		wait:.
		unlock:.
		moveUp:.
		moveToQuay:.
		n =. var n +. lit (-1)
	)