implementation module Smurf

from StdFunc import o, flip
import StdArray
import StdDebug
import StdList
import StdMisc
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, Expr, State
derive gPrint (,), Expr, VarChar

instance == Stm where == a b = a === b
instance == Expr where == a b = a === b
instance == State where == a b = a === b

instance zero [a] where zero = []

/// Utilities ...

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

instance toString Expr
where
	toString (Lit s)      = s
	toString (Var v)      = "$" <+ v
	toString (ECat a b)   = a <+ b
	toString (EHead a)    = "hd(" <+ a <+ ")"
	toString (ETail a)    = "tl(" <+ a <+ ")"
	toString (EQuotify a) = "q(" <+ a <+ ")"

instance toString Stm
where
    toString (Push s) = toString $ 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 $ Lit ""
	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 "~", eToLaTeX 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 :: (Expr,Expr) -> LaTeX
		assToLaTeX (var,val)
			= List
				[ eToLaTeX var
				, Command "mapsto" []
				, eToLaTeX 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 :: Stack -> LaTeX
stackToLaTeX es
	= List $ intersperse (Text ":") (map eToLaTeX es ++ [Command "Nil" []])

eToLaTeX :: Expr -> LaTeX
eToLaTeX e = Command "texttt" [List [Raw "\"", etl e, Raw "\""]]
where
	etl :: Expr -> LaTeX
	etl (Lit s)      = Text s
	etl (Var v)      = Math False [Raw v]
	etl (ECat a b)   = List [etl a, etl b]
	etl (EHead e)    = List [Command "textit" [Text "hd"], Raw "(", etl e, Raw ")"]
	etl (ETail e)    = List [Command "textit" [Text "tl"], Raw "(", etl e, Raw ")"]
	etl (EQuotify e) = List [Command "textit" [Text "q"], Raw "(", etl e, Raw ")"]

instance toLaTeX DerivationTree
where
	toLaTeX ts = toL ts
	where
		toL :: DerivationTree -> LaTeX
		toL []  = List []
		toL [t]
			= List
				[ Command "axjustifies" []
				, toLaTeX t
				, Command "using" [rule]
				]
		where
			rule = case t of
				(([], _, _) --> (_, _, _)) = Command "rlambdans" []
				_ = Command "rule" [Text "assumption", Text ""]
		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"

/// End utilities

instance +++ Expr
where
	(+++) (Lit s) (Lit t) = Lit $ s +++ t
	(+++) a b             = ECat a b

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 >>= \(pgm,_) -> pure (let vcs = eToVarChars pgm in fromJust $ parsev $ trace (printToString vcs +++ "\n") vcs, zero), io)

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

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

head :: Expr -> Maybe Expr
head (Lit "") = empty
head (Lit s) = pure $ Lit $ s % (0,0)
head e = pure $ EHead e

tail :: Expr -> Maybe Expr
tail (Lit "") = empty
tail (Lit s) = pure $ Lit $ s % (1, size s - 1)
tail e = pure $ ETail e

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

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

quotify :: Expr -> Expr
quotify (Lit s) = Lit $ flip (+++) "\"" $ (+++)"\"" $ toString $ quot $ fromString s
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]
quotify (ECat a b) = ECat (quotify a) (quotify b)
quotify (EHead a)  = EHead (quotify a)
quotify (ETail a)  = ETail (quotify a)
quotify (Var v)    = EQuotify (Var v)

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

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

prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
	Program State ListIO (IO ListIO) -> Maybe DerivationTree
prover assumptions pgm st io iof
# init              = (pgm, io.input, st)
# mbAssumption      = assumptions init
| isJust mbAssumption
	= Just [init --> fromJust mbAssumption]
# (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            = prover assumptions pgm st io iof
| isNothing mbTree  = empty
# [child=:(_ --> final):children] = fromJust mbTree
= pure [init --> final:child:children]