From: Evgenii Akentev <hi@ak3n.com>
Date: Sat, 7 Sep 2024 15:16:54 +0000 (+0400)
Subject: Add Virtual VEC machine
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7ae50abd80cbcb6aab4b3a5103a6b9623b59de68;p=machines.hs.git

Add Virtual VEC machine
---

diff --git a/machines.cabal b/machines.cabal
index d889307..d35fc01 100644
--- a/machines.cabal
+++ b/machines.cabal
@@ -22,6 +22,7 @@ library
                       Virtual.CEK,
                       Virtual.Krivine,
                       Virtual.CAM,
+                      Virtual.VEC,
     build-depends:    base ^>=4.18.2.1
     hs-source-dirs:   src
     default-language: Haskell2010
diff --git a/src/Virtual/VEC.hs b/src/Virtual/VEC.hs
new file mode 100644
index 0000000..45a7448
--- /dev/null
+++ b/src/Virtual/VEC.hs
@@ -0,0 +1,64 @@
+{-# language LambdaCase #-}
+
+module Virtual.VEC where
+
+-- From Interpreter to Compiler and
+-- Virtual Machine: A Functional Derivation
+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
+
+data Term = App Term Term | CBNLam String Term | CBVLam String Term | Var String | Lit Literal | Succ Term | IfThenElse Term Term Term 
+data Literal = BoolLit Bool | NumLit Int
+  deriving (Show)
+data Inst = Pushclosure [Inst] | Pushconst Literal | Call | Return | Push String | Bind String | Incr | Test [Inst] [Inst]
+  deriving (Show)
+type Env = [(String, Val)]
+data Val = Closure [Inst] Env | Primitive Literal
+  deriving (Show)
+
+compile :: Term -> [Inst]
+compile = \case
+  (App t0 t1) -> Pushclosure (compile t1 ++ [Return]) : compile t0 ++ [Call] 
+  (CBNLam x t) -> [Pushclosure (Bind x : compile t ++ [Return])]
+  (CBVLam x t) -> [Pushclosure (Call : Bind x : compile t ++ [Return])]
+  (Var x) -> [Push x]
+  (Lit l) -> [Pushconst l]
+  (Succ t) -> compile t ++ [Incr]
+  (IfThenElse t0 t1 t2) -> compile t0 ++ [Test (compile t1) (compile t2)]
+
+run :: [Val] -> [Env] -> [Inst] -> Val
+run vs (e : es) (Pushclosure c':cs) = run (Closure c' e : vs) (e : es) cs
+run vs es (Pushconst l : cs) = run (Primitive l:vs) es cs
+run (Closure c' e : vs) es (Call : cs) = run vs (e : es) (c' ++ cs)
+run vs (_:es) (Return : cs) = run vs es cs
+run vs (e:es) (Push x : cs) = case lookup x e of
+  Just v@(Primitive _) -> run (v : vs) (e : es) cs
+  Just (Closure c' e') -> run vs (e' : e : es) (c' ++ cs) 
+  Nothing -> error "var not in scope"
+run (v : vs) (e : es) (Bind x : cs) = run vs (((x, v):e) : es) cs
+run (Primitive (NumLit n) : vs) es (Incr : cs) = run (Primitive (NumLit $ n + 1) : vs) es cs
+run (Primitive (BoolLit True) : vs) es (Test c1 _ : cs) = run vs es (c1 ++ cs)
+run (Primitive (BoolLit False) : vs) es (Test _ c2 : cs) = run vs es (c2 ++ cs)
+run (v:_) _ [] = v 
+run _ _ _ = error "Impossible"
+
+eval :: Term -> Val
+eval t = run [] [[]] $ compile t
+
+t1 :: Term
+t1 = Succ $ (Lit $ NumLit 2)
+
+ex1 :: Val 
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = App (App (CBNLam "x" $ Var "x") (CBNLam "x" $ Var "x")) (CBNLam "x" $ Var "x")
+
+ex2 :: Val 
+ex2 = eval t2
+
+t3 :: Term
+t3 = App (App (App (CBNLam "x" $ CBNLam "y" $ CBNLam "z" $ IfThenElse (Var "x") (Succ $ Var "y") (Var "z")) (Lit $ BoolLit True)) (Lit $ NumLit 2)) (Lit $ NumLit 7)
+
+ex3 :: Val
+ex3 = eval t3