gistfile1.hs

{-# OPTIONS -Wall #-}
{-# LANGUAGE BangPatterns #-}

import Control.Monad (zipWithM)
import Data.List (elemIndex,intercalate)

data Term
  = Var String
  | Lam Scope
  | App Term Term
  | Con String [Term]
  | Case Term [Clause]

data Clause
  = Clause Pattern Scope

data Pattern
  = VarPat
  | ConPat String [Pattern]

data Scope
  = Scope { instantiate :: !([Term] -> Term) }

abstract :: [String] -> Term -> [Term] -> Term
abstract xs (Var y)
  = case elemIndex y xs of
      Nothing -> \_ -> Var y
      Just i  -> \vs -> vs !! i
abstract xs (Lam sc)
  = let !mksc = abstractScope xs sc
    in \vs -> Lam (mksc vs)
abstract xs (App f a)
  = let !mkf = abstract xs f
        !mka = abstract xs a
    in \vs -> App (mkf vs) (mka vs)
abstract xs (Con c as)
  = let !mkas = [ abstract xs a | a <- as ]
    in \vs -> Con c (map ($ vs) mkas)
abstract xs (Case a cs)
  = let !mka = abstract xs a
        !mkcs = [ abstractClause xs c | c <- cs ]
    in \vs -> Case (mka vs) (map ($ vs) mkcs)

abstractScope :: [String] -> Scope -> [Term] -> Scope
abstractScope xs (Scope f)
  = \vs -> Scope (\vs' -> abstract xs (f vs') vs)

abstractClause :: [String] -> Clause -> [Term] -> Clause
abstractClause xs (Clause p sc)
  = let !mksc = abstractScope xs sc
    in \vs -> Clause p (mksc vs)



pretty :: Int -> Term -> String
pretty _ (Var x)  = x
pretty i (Lam sc) = "lam(" ++ prettyScope i sc ++ ")"
pretty i (App f a) = "app(" ++ pretty i f ++ ";" ++ pretty i a ++ ")"
pretty i (Con c as) = c ++ "(" ++ intercalate ";" (map (pretty i) as) ++ ")"
pretty i (Case a cs) = "case(" ++ pretty i a ++ "){" ++ intercalate ";" (map (prettyClause i) cs) ++ "}"

prettyScope :: Int -> Scope -> String
prettyScope i (Scope f) = let v = "v" ++ show i
                          in v ++ "." ++ pretty (i+1) (f [Var v])

prettyClause :: Int -> Clause -> String
prettyClause i (Clause p sc)
  = prettyPattern p ++ " -> " ++ prettyScope i sc

prettyPattern :: Pattern -> String
prettyPattern VarPat = "_"
prettyPattern (ConPat c ps) = c ++ "(" ++ intercalate ";" (map prettyPattern ps) ++ ")"


eval :: Term -> Term
eval (Var x) = Var x
eval (Lam sc) = Lam (Scope $ \vs -> eval (instantiate sc vs))
eval (App f a) = case (eval f, eval a) of
                   (Lam sc,a') -> eval (instantiate sc [a'])
                   (f',a')      -> App f' a'
eval (Con c as) = Con c (map eval as)
eval (Case a cs) = let ea = (eval a)
                   in case matchClauses ea cs of
                        Nothing -> Case ea cs
                        Just b  -> eval b

matchClauses :: Term -> [Clause] -> Maybe Term
matchClauses _ [] = Nothing
matchClauses m (Clause p sc:cs)
  = case match m p of
      Nothing -> matchClauses m cs
      Just ms  -> Just (instantiate sc ms)

match :: Term -> Pattern -> Maybe [Term]
match m VarPat = Just [m]
match (Con c as) (ConPat c' ps) | c == c' && length as == length ps
  = fmap concat (zipWithM match as ps)
match _ _ = Nothing

main :: IO ()
main = do putStrLn $ pretty 0 tm
          putStrLn $ pretty 0 (eval tm)
          putStrLn $ pretty 0 tm'
          putStrLn $ pretty 0 (eval tm')
          putStrLn $ pretty 0 tm''
          putStrLn $ pretty 0 (eval tm'')
  where
    tm = (App (Lam (Scope $ \[x] -> x)) (Var "x"))
    tm' = Case (Con "foo" [Con "bar" []])
               [Clause (ConPat "foo" [VarPat]) (Scope $ \[x] -> x)]
    tm'' = Lam (Scope $ \[y] -> App (Lam (Scope $ \[x] -> x)) y)