From d487e9f1da185d884d4da14a8194a3ecf883055f Mon Sep 17 00:00:00 2001
From: Evgenii Akentev <hi@ak3n.com>
Date: Sat, 7 Sep 2024 14:54:54 +0400
Subject: [PATCH] Add Virtual CEK and Krivine machines

---
 machines.cabal         |  5 +++-
 src/Virtual/CEK.hs     | 59 ++++++++++++++++++++++++++++++++++++++++++
 src/Virtual/Krivine.hs | 51 ++++++++++++++++++++++++++++++++++++
 3 files changed, 114 insertions(+), 1 deletion(-)
 create mode 100644 src/Virtual/CEK.hs
 create mode 100644 src/Virtual/Krivine.hs

diff --git a/machines.cabal b/machines.cabal
index b28c802..1d40bf5 100644
--- a/machines.cabal
+++ b/machines.cabal
@@ -17,7 +17,10 @@ library
                       Abstract.SECD,
                       Abstract.SEC,
                       Abstract.SE,
-                      Abstract.EC
+                      Abstract.EC,
+
+                      Virtual.CEK,
+                      Virtual.Krivine
     build-depends:    base ^>=4.18.2.1
     hs-source-dirs:   src
     default-language: Haskell2010
diff --git a/src/Virtual/CEK.hs b/src/Virtual/CEK.hs
new file mode 100644
index 0000000..ff1e9d5
--- /dev/null
+++ b/src/Virtual/CEK.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE LambdaCase #-}
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+module Virtual.CEK where
+
+data Term = Var String | Lam String Term | App Term Term
+  deriving (Show)
+
+data Inst = Access String | Close String [Inst] | Push [Inst]
+  deriving (Show)
+
+compile :: Term -> [Inst]
+compile = \case
+  (Var x) -> [Access x]
+  (Lam x t) -> [Close x (compile t)]
+  (App t0 t1) -> [Push (compile t1)] ++ compile t0
+
+type Env = [(String, Val)]
+data Val = Closure String [Inst] Env
+  deriving (Show)
+
+data Context = C0 | C1 [Inst] Env Context | C2 Val Context
+  deriving (Show)
+
+transition1 :: [Inst] -> Env -> Context -> (Context, Val)
+transition1 (Access x : _) e k = case lookup x e of
+  Just v -> transition2 k v
+  Nothing -> error "var not in scope"
+transition1 (Close x c' : _) e k = transition2 k (Closure x c' e)
+transition1 (Push c' : c) e k = transition1 c e (C1 c' e k)
+
+transition2 :: Context -> Val -> (Context, Val)
+transition2 (C1 c e k) v = transition1 c e (C2 v k)
+transition2 (C2 (Closure x c e) k) v = transition1 c ((x, v):e) k
+transition2 C0 v = (C0, v)
+
+run :: [Inst] -> Val
+run c =
+  let (C0, v) = transition1 c [] C0
+  in v
+
+eval :: Term -> Val
+eval t = run $ compile t
+
+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
diff --git a/src/Virtual/Krivine.hs b/src/Virtual/Krivine.hs
new file mode 100644
index 0000000..e23e1e8
--- /dev/null
+++ b/src/Virtual/Krivine.hs
@@ -0,0 +1,51 @@
+{-# language LambdaCase #-}
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+module Virtual.Krivine where
+
+data Term = Var Int | Lam String Term | App Term Term
+  deriving (Show)
+
+data Inst = Access Int | Grab String | Push [Inst]
+  deriving (Show)
+
+compile :: Term -> [Inst]
+compile = \case
+  (Var n) -> [Access n]
+  (Lam x t) -> Grab x : compile t
+  (App t0 t1) -> Push (compile t1) : compile t0
+
+type Env = [Val]
+data Val = Closure [Inst] Env
+  deriving (Show)
+data Res = Result String Env
+  deriving (Show)
+type Stack = [Val]
+
+step :: [Inst] -> Env -> Stack -> Res
+step (Access n : _) e s = let (Closure c' e') = e!!n in step c' e' s
+step (Grab _ : c) e (Closure c' e' :s) = step c (Closure c' e' :e) s
+step (Push c' : c) e s = step c e (Closure c' e : s)
+step (Grab l : c) e [] = Result l e
+
+run :: [Inst] -> Res
+run c = step c [] []
+
+eval :: Term -> Res
+eval t = run $ compile t
+
+t1 :: Term
+t1 = App (Lam "x" (App (Var 0) (Var 0))) (Lam "x" (Var 0))
+
+ex1 :: Res 
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = App (App (Lam "x" $ Var 0) (Lam "x" $ Var 0)) (Lam "x" $ Var 0)
+
+ex2 :: Res 
+ex2 = eval t2
-- 
2.34.1