implementation module Smurf

from StdFunc import o, flip
import StdArray
import StdList
import StdString
import StdTuple
import StdFile

from Data.Func import $
import Control.Applicative
import Control.Monad
import Data.Maybe
import Data.List
from Text import class Text(concat), instance Text String

import GenEq
import GenPrint

import SmurfParse
import LaTeX

derive gEq Stm
derive gPrint (,)

(<+) infixr 5 :: a b -> String | toString a & toString b
(<+) a b = toString a +++ toString b

instance == Stm where == a b = a === b

instance zero [a] where zero = []

instance toString Stm
where
    toString (Push s) = quotify s
    toString Input = "i"
    toString Output = "o"
    toString Cat = "+"
    toString Head = "h"
    toString Tail = "t"
    toString Quotify = "q"
    toString Put = "p"
    toString Get = "g"
    toString Exec = "x"

instance toChar Stm where toChar stm = (toString stm).[0]

instance fromChar Stm
where
	fromChar '"' = Push ""
	fromChar 'i' = Input
	fromChar 'o' = Output
	fromChar '+' = Cat
	fromChar 'h' = Head
	fromChar 't' = Tail
	fromChar 'q' = Quotify
	fromChar 'p' = Put
	fromChar 'g' = Get
	fromChar 'x' = Exec

printList :: [a] -> String | toString a
printList xs = "[" <+ concat (intersperse ":" (map (\s->'"' <+ s <+ '"') xs)) <+ "]"

instance zero State where zero = { stack = zero, store = zero }

instance zero ListIO where zero = {input=[], output=[]}

instance toString State
where
	toString {stack,store} = "(" <+ printToString stack <+ "," <+ printToString store <+ ")"

instance toString Transition
where
	toString ((p1, ip1, st1) --> (ip2, op, st2))
		= "<" <+ simple 2 p1 <+ "," <+ st1 <+ "," <+ printList ip1 <+ "> -> ("
			<+ printList ip2 <+ "," <+ printList op <+ "," <+ st2 <+ ")"
	where
		simple :: !Int !Program -> String
		simple _ [] = "λ"
		simple i pgm
			| i >= length pgm = concat $ intersperse ":" $ map toString pgm
			= simple i (take i pgm) +++ ":..."

instance toString DerivationTree
where toString ts = concat $ intersperse "\n" $ map toString $ reverse ts

instance toLaTeX Stm
where
	toLaTeX (Push s) = List [Command "StmPush" [], Raw "~", sToLaTeX s]
	toLaTeX Input    = Command "StmInput" []
	toLaTeX Output   = Command "StmOutput" []
	toLaTeX Cat      = Command "StmCat" []
	toLaTeX Head     = Command "StmHead" []
	toLaTeX Tail     = Command "StmTail" []
	toLaTeX Quotify  = Command "StmQuotify" []
	toLaTeX Put      = Command "StmPut" []
	toLaTeX Get      = Command "StmGet" []
	toLaTeX Exec     = Command "StmExec" []

instance toLaTeX Program
where
	toLaTeX []  = Command "lambda" []
	toLaTeX pgm = List $ intersperse (Text ":") (map toLaTeX pgm)

instance toLaTeX String where toLaTeX s = Text s

instance toLaTeX Store
where
	toLaTeX [] = Command "emptyset" []
	toLaTeX ass
		= List
			([Command "{" []] ++
			intersperse (Raw ",") (map assToLaTeX ass) ++
			[Command "}" []])
	where
		assToLaTeX :: (String,String) -> LaTeX
		assToLaTeX (var,val)
			= List
				[ sToLaTeX var
				, Command "mapsto" []
				, sToLaTeX val
				]

instance toLaTeX State
where
	toLaTeX {stack,store}
		= List
			[ Command "left" []
			, Raw "("
			, stackToLaTeX stack
			, Raw ","
			, toLaTeX store
			, Command "right" []
			, Raw ")"
			]

instance toLaTeX Transition
where
	toLaTeX ((p1,ip1,st1) --> (ip2,op,st2))
		= Command "trans"
			[ toLaTeX p1
			, stackToLaTeX ip1
			, toLaTeX st1
			, stackToLaTeX ip2
			, stackToLaTeX op
			, toLaTeX st2
			]

stackToLaTeX :: [String] -> LaTeX
stackToLaTeX ss
	= List $ intersperse (Text ":") (map sToLaTeX ss ++ [Command "Nil" []])

sToLaTeX :: String -> LaTeX
sToLaTeX s = Command "texttt" [List [Raw "\"", Text s, Raw "\""]]

instance toLaTeX DerivationTree
where
	toLaTeX ts = toL ts
	where
		toL :: DerivationTree -> LaTeX
		toL []  = List []
		toL [t]
			= List
				[ Command "axjustifies" []
				, toLaTeX t
				, Command "using" [Command "rlambdans" []]
				]
		toL [t=:((p1,_,_)-->_):ts]
			= List
				[ Command "[" []
				, toL ts
				, Command "]" []
				, Command "justifies" []
				, toLaTeX t
				, Command "using" [Command rule []]
				]
		where
			rule = case p1 of
				[Push _:_]  = "rpushns"
				[Input:_]   = "rinputns"
				[Output:_]  = "routputns"
				[Cat:_]     = "rcatns"
				[Head:_]    = "rheadns"
				[Tail:_]    = "rtailns"
				[Quotify:_] = "rquotifyns"
				[Put:_]     = "rputns"
				[Get:_]     = "rgetns"
				[Exec:_]    = "rexecns"

run :: !Program State io (IO io) -> (Maybe State, io)
run prog st io iofuncs
    # (mbProgSt, io) = step prog st io iofuncs
    | isNothing mbProgSt = (Nothing, io)
    # (prog, st) = fromJust mbProgSt
    = if (isEmpty prog) (Just st, io) (run prog st io iofuncs)

step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io)
step [] st io _
    = (pure ([], st), io)
step [Push s:p] st io _
    = (pure (p, { st & stack = push s st.stack }), io)
step [Input:p] st io (IO input _)
	# (ip, io) = input io
    = (pure (p, { st & stack = push ip st.stack }), io)
step [Output:p] st io (IO _ output)
    # mbSStk = pop st.stack
    | isNothing mbSStk = (empty, io)
    # (s, stk) = fromJust mbSStk
    = (pure (p, { st & stack = stk }), output s io)
step [Cat:p] st io _
    = (pop st.stack >>= \(x,stk) -> pop stk >>= \(y,stk`) ->
        pure (p, { st & stack = push (y +++ x) stk` }), io)
step [Head:p] st io _
    = (pop st.stack >>= \(x,stk) -> head x >>= \x` ->
        pure (p, { st & stack = push x` stk }), io)
step [Tail:p] st io _
    = (pop st.stack >>= \(x,stk) -> tail x >>= \x` ->
        pure (p, { st & stack = push x` stk }), io)
step [Quotify:p] st io _
    = (pop st.stack >>= \(x,stk) ->
        pure (p, { st & stack = push (quotify x) stk }), io)
step [Put:p] st io _
    = (pop st.stack >>= \(var,stk) -> pop stk >>= \(val,stk`) ->
        pure (p, { st & stack = stk`, store = put var val st.store }), io)
step [Get:p] st io _
    = (pop st.stack >>= \(var,stk) ->
        pure (p, { st & stack = push (get var st.store) stk }), io)
step [Exec:p] st io _
    = (pop st.stack >>= parse o fromString o fst >>= \p ->
        pure (p, zero), io)

push :: String Stack -> Stack
push s st = [s:st]

pop :: Stack -> Maybe (String, Stack)
pop [] = empty
pop [s:ss] = pure (s, ss)

head :: String -> Maybe String
head "" = empty
head s = pure $ s % (0,0)

tail :: String -> Maybe String
tail "" = empty
tail s = pure $ s % (1, size s - 1)

put :: String String Store -> Store
put var val store = [(var,val) : filter ((<>)var o fst) store]

get :: String Store -> String
get var store = case filter ((==)var o fst) store of [] = ""; [(_,val):_] = val

quotify :: (String -> String)
quotify = (flip (+++) "\"") o ((+++)"\"") o toString o quot o fromString
where
    quot :: [Char] -> [Char]
    quot []        = []
    quot ['\\':cs] = ['\\':'\\':quot cs]
    quot ['\n':cs] = ['\\':'n':quot cs]
    quot ['\r':cs] = ['\\':'r':quot cs]
    quot ['\t':cs] = ['\\':'t':quot cs]
    quot ['"':cs]  = ['\\':'"':quot cs]
    quot [c:cs]    = [c:quot cs]

listIO :: IO ListIO
listIO = IO read write
where
	read :: ListIO -> (String, ListIO)
	read io=:{input} = (hd input, { io & input=tl input })

	write :: String ListIO -> ListIO
	write s io=:{output} = { io & output=output ++ [s] }

tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree
tree pgm st io iof
	# init              = (pgm, io.input, st)
	# (mbPgmSt, io)     = step pgm st io iof
	| isNothing mbPgmSt = empty
	# (pgm, st)         = fromJust mbPgmSt
	| isEmpty pgm       = pure [ init --> (io.input, io.output, st)
	                           , ([],io.input,st) --> (io.input,[],st)
	                           ]
	# mbTree            = tree pgm st io iof
	| isNothing mbTree  = empty
	# tree              = fromJust mbTree
	# [child=:(_ --> final):children] = fromJust mbTree
	= pure [init --> final:child:children]