-- an implementation of the lambda calculus using higher-order abstract syntax

module Lambda (
  Lam (Abs,App),
  freevar,
  eval,
  evals,
  value,
  closed
  ) where

-- a typical data structure for implementing lambda expressions 
-- that we won't be using because we are lazy and don't want to
-- implement substitution:

data NotLam =
    NVar String            -- variables
  | NAbs String NotLam     -- \"x". e
  | NApp NotLam NotLam     -- e1 e2

-- HOAS (Higher-Order Abstract Syntax) Lambda Calculus data type follows.  
-- Notice there is no ordinary (bound) variable clause!
-- Only a clause for free variables!
-- Invariant:  all FreeVar Strings should start with "!"
-- To ensure this, only use function freevar to create free variable terms

data Lam =            
    Abs (Lam -> Lam)  -- \x.e
  | App Lam Lam       -- e1 e2
  | FreeVar String    -- a free variable named String  
    
freevar :: String -> Lam
freevar s = FreeVar ("!" ++ s)
    
-- zero or one step evaluation --
eval :: Lam -> Lam
eval (App (Abs f) (Abs g)) = f (Abs g) 
eval (App (Abs f) e)       = App (Abs f) (eval e)
eval (App e1 e2)           = App (eval e1) e2
eval (Abs f)               = Abs f
eval (FreeVar x)           = error "Stuck!"

-- is a value? --
value (Abs f)     = True
value (App e1 e2) = False
value (FreeVar s) = False

-- multi-step evaluation --
evals :: Lam -> Lam
evals e = if value e then e else evals (eval e)

-- closed --
boundname = "bound"

closed :: Lam -> Bool
closed (Abs f)     = closed (f (FreeVar boundname))
closed (App e1 e2) = closed e1 && closed e2
closed (FreeVar s) = s == boundname

-- printing --

may :: Bool -> String -> String
may b s = if b then s else ""

left, right :: Bool -> String
left b    = may b "("
right b   = may b ")"

-- Bool is true if expression is within an argument position
-- Int is the next variable name to use
showlam :: Bool -> Int -> Lam -> String
showlam b n (FreeVar s) = s 
showlam b n (Abs f) = 
  let var = "x" ++ show n in
  "(" ++ "\\" ++ var ++ "." ++ showlam False (n+1) (f (FreeVar var)) ++ ")"
showlam b n (App e1 e2) =
  left b ++ showlam False n e1 ++ " " ++ showlam True n e2 ++ right b
    
instance Show Lam where
  show x = showlam False 1 x