A family of SECD variants

SECD.hs

-- Based on "A Rational Deconstruction of Landin's SECD Machine" by Olivier Danvy
-- (BRICS-RS-03-33)

module SECD where
import Data.Maybe

type Ident = String

type Env a = [(Ident, a)]

empty' :: Env a
empty' = []

extend' :: Ident -> a -> Env a -> Env a
extend' ident value env = (ident, value) : env

lookup' :: Ident -> Env a -> Maybe a
lookup' ident [] = Nothing
lookup' ident ((ident',value):xs)
  | ident == ident' = Just value
  | otherwise       = lookup' ident xs

data SourceTerm = Literal Int
                | Variable Ident
                | Lambda Ident SourceTerm
                | Application SourceTerm SourceTerm
                deriving (Show)
            
type Program = SourceTerm

data Value = Int' Int
           | Succ
           | Closure (Env Value) Ident SourceTerm
           deriving (Show)

data Directive = Term SourceTerm
               | Apply
                 
type S = [Value]
type E = Env Value
type C = [Directive]
type D = [(S, E, C)]

initial_env = (extend' "succ" Succ empty')

run :: S -> E -> C -> D -> Value
run (v : []) _ [] []                            = v
run (v : []) _ [] ((s, e, c) : d)               = run (v : s) e c d
run s e ((Term (Literal n)) : c) d              = run ((Int' n) : s) e c d
run s e ((Term (Variable x)) : c) d             = run ((fromJust $ lookup' x e) : s) e c d
run s e ((Term (Lambda x t)) : c) d             = run ((Closure e x t) : s) e c d
run s e ((Term (Application t1 t2)) : c) d      = run s e ((Term t2) : (Term t1) : Apply : c) d
run (Succ : (Int' n) : s) e (Apply : c) d       = run ((Int' (n + 1)) : s) e c d
run ((Closure e' x t) : v' : s) e (Apply : c) d = run [] (extend' x v' e') ((Term t) : []) ((s, e, c) : d)

evaluate0 :: Program -> Value
evaluate0 term = run [] initial_env ((Term term) : []) []


run_c :: S -> E -> C -> D -> Value
run_c s _ [] d             = run_d s d
run_c s e ((Term t) : c) d = run_t t s e c d
run_c s e (Apply : c) d    = run_a s e c d

run_d :: S -> D -> Value
run_d (v : []) []              = v
run_d (v : []) ((s, e, c) : d) = run_c (v : s) e c d

run_t :: SourceTerm -> S -> E -> C -> D -> Value
run_t (Literal n) s e c d         = run_c ((Int' n) : s) e c d
run_t (Variable x) s e c d        = run_c ((fromJust $ lookup' x e) : s) e c d
run_t (Lambda x t) s e c d        = run_c ((Closure e x t) : s) e c d
run_t (Application t1 t2) s e c d = run_t t2 s e ((Term t1) : Apply : c) d

run_a :: S -> E -> C -> D -> Value
run_a (Succ : (Int' n) : s) e c d       = run_c ((Int' (n + 1)) : s) e c d
run_a ((Closure e' x t) : v' : s) e c d = run_t t [] (extend' x v' e') [] ((s, e, c) : d)

evaluate1 :: Program -> Value
evaluate1 term = run_t term [] initial_env [] []


type C' = S -> E -> D' -> Value
type D' = S -> Value

run_t' :: SourceTerm -> S -> E -> C' -> D' -> Value
run_t' (Literal n) s e c d = c ((Int' n) : s) e d
run_t' (Variable x) s e c d = c ((fromJust $ lookup' x e) : s) e d
run_t' (Lambda x t) s e c d = c ((Closure e x t) : s) e d
run_t' (Application t1 t2) s e c d = run_t' t2 s e (\ s e d -> run_t' t1 s e (\ s e d -> run_a' s e c d) d) d

run_a' :: S -> E -> C' -> D' -> Value
run_a' (Succ : (Int' n) : s) e c d = c ((Int' (n + 1)) : s) e d
run_a' ((Closure e' x t) : v' : s) e c d = run_t' t [] (extend' x v' e') (\s _ d -> d s) (\(v:[]) -> c (v:s) e d)

evaluate2 :: Program -> Value
evaluate2 term = run_t' term [] initial_env (\s _ d -> d s) (\(v:[])-> v)


type C'' = S -> E -> S

eval :: SourceTerm -> S -> E -> C'' -> S
eval (Literal n) s e c = c ((Int' n) : s) e
eval (Variable x) s e c = c ((fromJust $ lookup' x e) : s) e
eval (Lambda x t) s e c = c ((Closure e x t) : s) e
eval (Application t1 t2) s e c = eval t2 s e (\ s e -> eval t1 s e (\ s e -> apply s e c))

apply :: S -> E -> C'' -> S
apply (Succ : (Int' n) : s) e c = c ((Int' (n + 1)) : s) e
apply ((Closure e' x t) : v' : s) e c =
  let (v : []) = eval t [] (extend' x v' e') (\s _ -> s) in c (v:s) e

evaluate3 :: Program -> Value
evaluate3 term = let (v : []) = eval term [] initial_env (\s _ -> s) in v


reset thunk = thunk ()

eval' :: SourceTerm -> (S, E) -> (S, E)
eval' (Literal n) (s, e) = (((Int' n) : s), e)
eval' (Variable x) (s, e) = (((fromJust $ lookup' x e) : s), e)
eval' (Lambda x t) (s, e) = (((Closure e x t) : s), e)
eval' (Application t1 t2) (s, e) =
  let (s',e') = eval' t2 (s, e) in
  let (s'', e'') = eval' t1 (s', e') in
  apply' (s'', e'')

apply' :: (S, E) -> (S, E)
apply' ((Succ : (Int' n) : s), e) = (((Int' (n + 1)) : s), e)
apply' (((Closure e' x t) : v' : s), e) =
  let (v : [], _) = reset (\ _ -> eval' t ([], (extend' x v' e'))) in
  ((v : s), e)

evaluate4 :: Program -> Value
evaluate4 term = let (v : [], _) = reset (\ _ -> eval' term ([], initial_env)) in v


eval'' :: SourceTerm -> E -> (Value, E)
eval'' (Literal n) e = ((Int' n) , e)
eval'' (Variable x) e = ((fromJust $ lookup' x e), e)
eval'' (Lambda x t) e = ((Closure e x t), e)
eval'' (Application t1 t2)  e =
  let (v2, e') = eval'' t2 e in
  let (v1, e'') = eval'' t1 e' in
  apply'' v1 (v2, e'')

apply'' :: Value -> (Value, E) -> (Value, E)
apply'' Succ ((Int' n), e) = ((Int' (n + 1)), e)
apply'' (Closure e' x t) (v', e) =
  let (v, _) = reset (\ _ -> eval'' t (extend' x v' e')) in
  (v, e)

evaluate5 :: Program -> Value
evaluate5 term = let (v, _) = reset (\ _ -> eval'' term initial_env) in v