Add SECD

diff --git a/machines.cabal b/machines.cabal
index 59769e6936efabeafcd30c3185f5bcf94b84b27f..7b6f76bd8573a7ded17095713233d1658c0d023d 100644 (file)
--- a/machines.cabal
+++ b/machines.cabal
@@ -12,7 +12,7 @@ common warnings
 
 library
     import:           warnings
-    exposed-modules:  Krivine, CEK
+    exposed-modules:  Krivine, CEK, SECD
     build-depends:    base ^>=4.18.2.1
     hs-source-dirs:   src
     default-language: Haskell2010

diff --git a/src/SECD.hs b/src/SECD.hs
index 5bcb3b8ef6bce171c563ab0516e15aeb94c65d69..6355e4d1ff884abaa0e51fbfd8aa072c0c466080 100644 (file)
--- a/src/SECD.hs
+++ b/src/SECD.hs
@@ -1,21 +1,62 @@
 module SECD where
 
 -- https://en.wikipedia.org/wiki/SECD_machine
+-- https://www.brics.dk/RS/03/33/BRICS-RS-03-33.pdf
 
-data Inst
-  = Nil
-  | Ldc
-  | Ld
-  | Sel
-  | Join
-  | Ldf
-  | Ap
-  | Ret
-  | Dum
-  | Rap
-
-data State = State
-  -- Control
-  -- Environment
-  -- Stack
-  -- Dump
+data Term = Appl Term Term | Var String | Abst String Term | Lit Int
+  deriving (Show)
+
+data Val = Num Int | Succ | Closure Term String Env
+  deriving (Show)
+
+data Directive = DTerm Term | DApply
+
+type Stack = [Val]
+type Env = [(String, Val)]
+type Control = [Directive]
+type Dump = [(Stack, Env, Control)]
+
+initEnv :: Env
+initEnv = [("succ", Succ)]
+
+-- S, E, C, D -> val
+run :: Stack -> Env -> Control -> Dump -> Val
+run (v:[]) _ [] [] = v
+-- ret
+run (v:[]) _ [] ((s, e, c):d) = run (v:s) e c d
+-- ldc 
+run s e ((DTerm (Lit n)):c) d = run ((Num n):s) e c d
+
+run s e ((DTerm (Var x)):c) d = case lookup x e of
+  Just v' -> run (v':s) e c d 
+  Nothing -> error "Var is undefined"
+
+run s e ((DTerm (Abst x t)):c) d = run ((Closure t x e):s) e c d
+
+run s e ((DTerm (Appl t0 t1)):c) d =
+  run s e ((DTerm t1):(DTerm t0):DApply:c) d
+
+run (Succ:(Num n):s) e (DApply:c) d = run ((Num $ n + 1):s) e c d
+
+-- ap
+run ((Closure t x e'):v':s) e (DApply:c) d =
+  run [] ((x, v'):e') [DTerm t] ((s, e, c):d)
+
+run _ _ _ _ = error "impossible"
+
+eval :: Term -> Val
+eval t = run [] initEnv [DTerm t] []
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = Appl (Abst "x" (Appl (Var "x") (Var "x"))) (Abst "x" (Appl (Var "succ") (Lit 1)))
+
+ex1 :: Val
+ex1 = eval t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = Appl (Appl (Abst "x" $ Var "x") (Abst "x" $ Var "x")) (Abst "x" $ Var "x")
+
+ex2 :: Val
+ex2 = eval t2