1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
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 // Literal string
| Var String // Variable
| ECat Expr Expr // e1 concatenated with e2
| EHead Expr // The head of e
| ETail Expr // The tail of e
| EQuotify Expr // e, quotified
:: 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)
|
