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

from LaTeX import class toLaTeX

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

:: Program :== [Stm]

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

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

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

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

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

derive gEq Stm

instance == Stm
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)

listIO :: IO ListIO
tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree