repos / machines.hs.git

CEK.hs

 1{-# LANGUAGE LambdaCase #-}
 2
 3-- From Interpreter to Compiler and
 4-- Virtual Machine: A Functional Derivation
 5-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
 6
 7module Virtual.CEK where
 8
 9data Term = Var String | Lam String Term | App Term Term
10  deriving (Show)
11
12data Inst = Access String | Close String [Inst] | Push [Inst]
13  deriving (Show)
14
15compile :: Term -> [Inst]
16compile = \case
17  (Var x) -> [Access x]
18  (Lam x t) -> [Close x (compile t)]
19  (App t0 t1) -> [Push (compile t1)] ++ compile t0
20
21type Env = [(String, Val)]
22data Val = Closure String [Inst] Env
23  deriving (Show)
24
25data Context = C0 | C1 [Inst] Env Context | C2 Val Context
26  deriving (Show)
27
28transition1 :: [Inst] -> Env -> Context -> (Context, Val)
29transition1 (Access x : _) e k = case lookup x e of
30  Just v -> transition2 k v
31  Nothing -> error "var not in scope"
32transition1 (Close x c' : _) e k = transition2 k (Closure x c' e)
33transition1 (Push c' : c) e k = transition1 c e (C1 c' e k)
34
35transition2 :: Context -> Val -> (Context, Val)
36transition2 (C1 c e k) v = transition1 c e (C2 v k)
37transition2 (C2 (Closure x c e) k) v = transition1 c ((x, v):e) k
38transition2 C0 v = (C0, v)
39
40run :: [Inst] -> Val
41run c =
42  let (C0, v) = transition1 c [] C0
43  in v
44
45eval :: Term -> Val
46eval t = run $ compile t
47
48t1 :: Term
49t1 = App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (Var "x"))
50
51ex1 :: Val
52ex1 = eval t1
53
54--((λ 0) (λ 0)) (λ 0)
55t2 :: Term
56t2 = App (App (Lam "x" $ Var "x") (Lam "x" $ Var "x")) (Lam "x" $ Var "x")
57
58ex2 :: Val
59ex2 = eval t2