From: Evgenii Akentev <hi@ak3n.com>
Date: Wed, 4 Sep 2024 12:22:00 +0000 (+0400)
Subject: Add Krivine, CEK & stubs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=2b5df2152143924ee55f80441cb22ca91b925464;p=machines.hs.git

Add Krivine, CEK & stubs
---

2b5df2152143924ee55f80441cb22ca91b925464
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4c9e245
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,23 @@
+dist
+dist-*
+cabal-dev
+*.o
+*.hi
+*.hie
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+.stack-work/
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..7cd2816
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2024 Evgenii Akentev
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/machines.cabal b/machines.cabal
new file mode 100644
index 0000000..59769e6
--- /dev/null
+++ b/machines.cabal
@@ -0,0 +1,18 @@
+cabal-version:      3.0
+name:               machines
+version:            0.1.0.0
+license:            MIT
+license-file:       LICENSE
+author:             Evgenii Akentev
+maintainer:         hi@ak3n.com
+build-type:         Simple
+
+common warnings
+    ghc-options: -Wall
+
+library
+    import:           warnings
+    exposed-modules:  Krivine, CEK
+    build-depends:    base ^>=4.18.2.1
+    hs-source-dirs:   src
+    default-language: Haskell2010
diff --git a/src/CEK.hs b/src/CEK.hs
new file mode 100644
index 0000000..6ee5a43
--- /dev/null
+++ b/src/CEK.hs
@@ -0,0 +1,55 @@
+module CEK where
+
+-- https://en.wikipedia.org/wiki/CEK_Machine
+-- https://legacy.cs.indiana.edu/ftp/techreports/TR202.pdf
+
+-- i'm fine with the defunctionalized version
+
+data V = Bound Int
+  deriving (Show, Eq)
+
+data Term = Appl Term Term | Var V | Abst Term
+  deriving (Show)
+
+data Val = Closure Term [Val]
+  deriving (Show)
+
+data Cont
+  = C2 Term [Val] Cont
+  | C1 Val Cont
+  | C0
+
+continue :: Cont -> Val -> Val 
+continue c v = case (c, v) of
+  (C2 t1 e k, v0) -> eval t1 e (C1 v0 k)
+  (C1 v0 k, v1) -> apply v0 v1 k
+  (C0, v') -> v'
+
+apply :: Val -> Val -> Cont -> Val
+apply v0 v1 k =
+  let (Closure t e) = v0
+  in eval t (v1 : e) k
+
+eval :: Term -> [Val] -> Cont -> Val
+eval t e k = case t of
+  Var (Bound n) -> continue k (e!!n)
+  Abst t' -> continue k (Closure t' e)
+  Appl t0 t1 -> eval t0 e (C2 t1 e k)
+
+run :: Term -> Val
+run t = eval t [] C0
+
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = Appl (Abst (Appl (Var $ Bound 0) (Var $ Bound 0))) (Abst (Var $ Bound 0))
+
+ex1 :: Val
+ex1 = run t1
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = Appl (Appl (Abst $ Var $ Bound 0) (Abst $ Var $ Bound 0)) (Abst $ Var $ Bound 0)
+
+ex2 :: Val
+ex2 = run t2
diff --git a/src/CESK.hs b/src/CESK.hs
new file mode 100644
index 0000000..7839227
--- /dev/null
+++ b/src/CESK.hs
@@ -0,0 +1,5 @@
+module CESK where
+
+-- https://cstheory.stackexchange.com/a/41257
+
+-- TODO: implement
diff --git a/src/CK.hs b/src/CK.hs
new file mode 100644
index 0000000..38b2948
--- /dev/null
+++ b/src/CK.hs
@@ -0,0 +1,3 @@
+module CK where
+
+-- TODO: implement
diff --git a/src/CS.hs b/src/CS.hs
new file mode 100644
index 0000000..919d26f
--- /dev/null
+++ b/src/CS.hs
@@ -0,0 +1,3 @@
+module CS where
+
+-- TODO: implement
diff --git a/src/Krivine.hs b/src/Krivine.hs
new file mode 100644
index 0000000..75c96c3
--- /dev/null
+++ b/src/Krivine.hs
@@ -0,0 +1,49 @@
+module Krivine where
+
+
+-- https://www.pls-lab.org/en/Krivine_machine
+-- https://en.wikipedia.org/wiki/Krivine_machine
+
+data V = Bound Int | Free String
+  deriving (Show, Eq)
+
+data Term = Appl Term Term | Var V | Abst Term
+  deriving (Show)
+
+newtype Closure = Closure (Term, [(V, Closure)])
+  deriving (Show)
+
+data State = State Term [Closure] [(V, Closure)]
+  deriving (Show)
+
+
+step :: State -> State
+step (State (Abst m) (c:s) e) = State m s ((Bound 0, c):e)
+step (State (Appl m n) s e) = State m (Closure (n,e):s) e
+step (State (Var x) s e) =
+  case lookup x e of
+    Just (Closure (m, e')) ->
+      State m s e'
+    Nothing -> error "variable is not found"
+step _ = error "bad state"
+
+eval :: State -> State
+eval s@(State (Abst _) [] _) = s
+eval s = let s' = step s in eval s'
+
+-- (\ 0 0) (\ 0)
+t1 :: Term
+t1 = Appl (Abst (Appl (Var $ Bound 0) (Var $ Bound 0))) (Abst (Var $ Bound 0))
+
+ex1 :: State
+ex1 =
+  let initState = State t1 [] []
+  in eval initState
+
+--((λ 0) (λ 0)) (λ 0)
+t2 :: Term
+t2 = Appl (Appl (Abst $ Var $ Bound 0) (Abst $ Var $ Bound 0)) (Abst $ Var $ Bound 0)
+
+ex2 :: State
+ex2 =
+  eval $ State t2 [] []
diff --git a/src/SECD.hs b/src/SECD.hs
new file mode 100644
index 0000000..5bcb3b8
--- /dev/null
+++ b/src/SECD.hs
@@ -0,0 +1,21 @@
+module SECD where
+
+-- https://en.wikipedia.org/wiki/SECD_machine
+
+data Inst
+  = Nil
+  | Ldc
+  | Ld
+  | Sel
+  | Join
+  | Ldf
+  | Ap
+  | Ret
+  | Dum
+  | Rap
+
+data State = State
+  -- Control
+  -- Environment
+  -- Stack
+  -- Dump