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

:: 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, [String], State) ([String], [String], 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

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