definition module Smurf

from StdOverloaded import
	class zero,
	class toString,
	class toChar, class fromChar,
	class ==

from GenEq import generic gEq

from Data.Maybe import ::Maybe(Nothing)

from LaTeX import class toLaTeX

:: Expr = Lit String
        | Var String
        | ECat Expr Expr
        | EHead Expr
        | ETail Expr
        | EQuotify Expr

:: Stm = Push Expr
       | Input | Output
       | Cat | Head | Tail | Quotify
       | Put | Get | Exec

:: Program :== [Stm]

:: Stack :== [Expr]
:: Store :== [(Expr, Expr)]

:: State = { stack :: Stack
           , store :: Store
           }

:: IO io = IO (io -> .(Expr, io)) (Expr io -> io)

:: ListIO = { input  :: [Expr]
            , output :: [Expr]
            }

:: Transition = (-->) infix 1 (Program, Stack, State) (Stack, Stack, State)
:: DerivationTree :== [Transition]

derive gEq Stm, Expr, State

instance == Stm
instance == Expr
instance == State

instance toString Stm
instance toChar Stm
instance fromChar Stm

instance zero State
instance toString State

instance zero ListIO

instance toString Transition
instance toString DerivationTree

instance toLaTeX Transition
instance toLaTeX DerivationTree

step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io)
run :: !Program State io (IO io) -> (Maybe State, io)

quotify :: Expr -> Expr

listIO :: IO ListIO
prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
	Program State ListIO (IO ListIO) -> Maybe DerivationTree
tree :== prover (\_ -> Nothing)