Crégut's strongly reducing Krivine abstract machine

Eval.hs

{-# LANGUAGE PatternSynonyms #-}

module Eval (eval) where

data Expr
  = Var {-# UNPACK #-} !Int
  | Lam Expr
  | App Expr Expr

type Level = Int

data Closure
  = Closure Expr Env
  | Level {-# UNPACK #-} !Level
  | Expr Expr {-# UNPACK #-} !Level

pattern Lambda :: Closure
pattern Lambda <- Level _
  where
  Lambda = Level 0

{-# COMPLETE Closure, Lambda, Expr #-}

type Env = [Closure]

type Stack = [Closure]

type State = (Closure, Stack, Level)

-- Crégut's strongly reducing Krivine abstract machine as described in Deriving
-- the Full-Reducing Krivine Machine from the Small-Step Operational Semantics
-- of Normal Order.
step :: State -> Maybe State
step (Closure e env, s, l) = Just $
  case e of
    -- Unbound variables throw exceptions.
    Var x -> (env !! x, s, l)
    Lam b ->
      case s of
        c@(Closure _ _) : s -> (Closure b (c : env), s, l)
        _ -> (Closure b (Level (l + 1) : env), Lambda : s, l + 1)
    App f a -> (Closure f env, Closure a env : s, l)
step (Level l', s, l) = Just (Expr (Var (l - l')) l, s, l)
step (Expr e l', c : s, l) = Just $
  case c of
    Closure _ _ -> (c, Expr e l' : s, l')
    Lambda -> (Expr (Lam e) l', s, l)
    Expr e' l' -> (Expr (App e' e) l', s, l)
-- Final state.
step (Expr _ _, [], _) = Nothing

-- https://hackage.haskell.org/package/zippers-0.3.2/docs/src/Control.Zipper.Internal.html#farthest
farthest :: forall a. (a -> Maybe a) -> a -> a
farthest f = go
  where
  go :: a -> a
  go x = maybe x go (f x)

{-# INLINE farthest #-}

eval :: Expr -> Expr
eval e =
  case farthest step (Closure e [], [], 0) of
    (Expr e _, _, _) -> e
    _ -> error "unreachable"