-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathsmallstep0.hs
57 lines (45 loc) · 1.43 KB
/
smallstep0.hs
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
import Data.Map as M
import Data.Set as S
type Name = String
type Lam = (Name, Term)
data Term = Var Name
| App Term Term
| Lam Lam
| Val Value
deriving Show
type Clo = (Lam, Env)
data Value = Clo Clo
| Nada
deriving Show
type Env = M.Map Name Value
data Cont = Halt
| Eval Term Env Cont
| Apply Clo Cont
deriving Show
type Context = (Term, Cont, Env)
data State = Done Value
| Stuck Context String
| Active Context
deriving Show
inject term = Active (term, Halt, M.empty)
transit (Var nm, knt, env) =
case M.lookup nm env of
Just val -> Active (Val val, knt, env)
Nothing -> Stuck (Var nm, knt, env) $ "reference to unbound variable: " ++ nm
transit (App proc arg, knt, env) = Active (proc, Eval arg env knt, env)
transit (Lam lam, knt, env) = Active (Val $ Clo (lam, env), knt, env)
transit (Val (Clo clo), Eval arg aenv knt, env) = Active (arg, Apply clo knt, aenv)
transit (Val arg, Apply ((nm, body), lenv) knt, env) = Active (body, knt, benv)
where benv = M.insert nm arg lenv
transit (Val val, Halt, env) = Done val
transit ctx = Stuck ctx "invalid state"
tidl = ("x", Var "x")
tid = Lam tidl
tidid = App tid tid
runi (Active ctx) = transit ctx
runi st = st
run (Active ctx) = run $ transit ctx
run st = st
runlog st = runlog' [] st
where runlog' hist (Active ctx) = runlog' (ctx:hist) $ transit ctx
runlog' hist st = (st, reverse hist)