Add SEC machine

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

diff --git a/src/SEC.hs b/src/SEC.hs
new file mode 100644 (file)
index 0000000..cf34f1c
--- /dev/null
+++ b/src/SEC.hs
@@ -0,0 +1,54 @@
+module SEC where
+
+-- https://www.brics.dk/RS/03/33/BRICS-RS-03-33.pdf
+
+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 = Stack -> Env -> Stack
+
+initEnv :: Env
+initEnv = [("succ", Succ)]
+
+eval :: Term -> Stack -> Env -> Control -> Stack
+eval (Lit n) s e c = c ((Num n):s) e
+eval (Var x) s e c = case lookup x e of
+  Just v -> c (v:s) e
+  Nothing -> error "var not in scope"
+eval (Abst x t) s e c = c ((Closure t x e):s) e
+eval (Appl t0 t1) s e c =
+  eval t1 s e $ \s' e' ->
+    eval t0 s' e' $ \s'' e'' -> 
+      apply s'' e'' c
+
+apply :: Stack -> Env -> Control -> Stack
+apply (Succ : (Num n):s) e c = c ((Num $ n + 1):s) e
+apply ((Closure t x e'):v':s) e c =
+  let [v] = eval t [] ((x, v'):e') (\s' _ -> s')
+  in c (v:s) e
+
+evaluate :: Term -> Val
+evaluate t =
+  let [v] = eval t [] initEnv (\s _ -> s)
+  in v
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = Appl (Abst "x" (Appl (Var "x") (Var "x"))) (Abst "x" (Appl (Var "succ") (Lit 1)))
+
+ex1 :: Val
+ex1 = evaluate t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = Appl (Appl (Abst "x" $ Var "x") (Abst "x" $ Var "x")) (Abst "x" $ Var "x")
+
+ex2 :: Val
+ex2 = evaluate t2