repos / machines.hs.git

CEK.hs

 1module Abstract.CEK where
 2
 3-- https://en.wikipedia.org/wiki/CEK_Machine
 4-- https://legacy.cs.indiana.edu/ftp/techreports/TR202.pdf
 5-- https://cstheory.stackexchange.com/a/41257
 6
 7-- i'm fine with the defunctionalized version
 8
 9data V = Bound Int
10  deriving (Show, Eq)
11
12data Term = Appl Term Term | Var V | Abst Term
13  deriving (Show)
14
15data Val = Closure Term [Val]
16  deriving (Show)
17
18data Cont
19  = C2 Term [Val] Cont
20  | C1 Val Cont
21  | C0
22
23continue :: Cont -> Val -> Val 
24continue c v = case (c, v) of
25  (C2 t1 e k, v0) -> eval t1 e (C1 v0 k)
26  (C1 v0 k, v1) -> apply v0 v1 k
27  (C0, v') -> v'
28
29apply :: Val -> Val -> Cont -> Val
30apply v0 v1 k =
31  let (Closure t e) = v0
32  in eval t (v1 : e) k
33
34eval :: Term -> [Val] -> Cont -> Val
35eval t e k = case t of
36  Var (Bound n) -> continue k (e!!n)
37  Abst t' -> continue k (Closure t' e)
38  Appl t0 t1 -> eval t0 e (C2 t1 e k)
39
40run :: Term -> Val
41run t = eval t [] C0
42
43
44-- (\ 0 0) (\ 0)
45t1 :: Term
46t1 = Appl (Abst (Appl (Var $ Bound 0) (Var $ Bound 0))) (Abst (Var $ Bound 0))
47
48ex1 :: Val
49ex1 = run t1
50
51--((λ 0) (λ 0)) (λ 0)
52t2 :: Term
53t2 = Appl (Appl (Abst $ Var $ Bound 0) (Abst $ Var $ Bound 0)) (Abst $ Var $ Bound 0)
54
55ex2 :: Val
56ex2 = run t2