--- /dev/null
+{-# language LambdaCase #-}
+
+module Virtual.CLS where
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+data Term = Var Int | Lam Term | App Term Term
+data Inst = Access Int | ILam [Inst] | Ap | Push
+ deriving (Show)
+type Env = [Val]
+data Val = Closure [Inst] Env
+ deriving (Show)
+
+compile :: Term -> [Inst]
+compile = \case
+ (Var n) -> [Access n]
+ (Lam t) -> [ILam $ compile t]
+ (App t0 t1) -> Push : compile t0 ++ compile t1 ++ [Ap]
+
+
+step :: [Inst] -> [Env] -> [Val] -> Val
+step (Access 0 : c) ((v : _) : l) s = step c l (v : s)
+step (Access n : c) ((_ : e) : l) s = step (Access (n - 1) : c) (e : l) s
+step (ILam c : c') (e : l) s = step c' l (Closure c e : s)
+step (Ap : c) l (v : (Closure c' e) : s) = step (c' ++ c) ((v : e) : l) s
+step (Push : c) (e : l) s = step c (e : e : l) s
+step [] _ (v : _) = v
+
+eval :: Term -> Val
+eval t = step (compile t) [[]] []
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = App (Lam (App (Var 0) (Var 0))) (Lam (Var 0))
+
+ex1 :: Val
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = App (App (Lam $ Var 0) (Lam $ Var 0)) (Lam $ Var 0)
+
+ex2 :: Val
+ex2 = eval t2
--- /dev/null
+{-# language LambdaCase #-}
+
+module Virtual.SECD where
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+data Term = Var String | Lam String Term | App Term Term
+data Inst = Access String | Close String [Inst] | Call
+ deriving (Show)
+type Env = [(String, Val)]
+data Val = Closure String [Inst] Env
+ deriving (Show)
+
+compile :: Term -> [Inst]
+compile = \case
+ (Var x) -> [Access x]
+ (Lam x t) -> [Close x $ compile t]
+ (App t0 t1) -> compile t1 ++ compile t0 ++ [Call]
+
+
+step :: [Inst] -> Env -> [Val] -> Val
+step (Access x : c) e s = case lookup x e of
+ Just v -> step c e (v:s)
+ Nothing -> error "Var not in scope"
+step (Close x c' : c) e s = step c e (Closure x c' e : s)
+step (Call : c) e (Closure x c' e' : v : s) = step (c' ++ c) ((x, v):e') s
+step [] e (v:_) = v
+
+eval :: Term -> Val
+eval t = step (compile t) [] []
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (Var "x"))
+
+ex1 :: Val
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = App (App (Lam "x" $ Var "x") (Lam "x" $ Var "x")) (Lam "x" $ Var "x")
+
+ex2 :: Val
+ex2 = eval t2