
-- |
-- Description: General purpose Lambda Calculus with named variables.
--
-- This is the source language to be compiled and executed using the various
-- machines.
module Rossum.LC where

import           Data.List              (elemIndex)
import           Text.Parsec
import           Text.Parsec.Combinator (between, chainr1, sepBy1)

-- * Lambda terms

type Name = String

data Term a
  = Var { label :: a, varName :: Name }
  | Sym { label :: a, symName :: Name }
  | Abs { label :: a, absName :: Name, absBody :: Term a }
  | App { label :: a, appFun :: Term a, appArg :: Term a }
  deriving (Read, Show, Eq, Ord)

-- | Recursively modify the labels of a 'Term'.
relabel :: (a -> b) -> Term a -> Term b
relabel f (Var l n) = Var (f l) n
relabel f (Sym l n) = Sym (f l) n
relabel f (Abs l n t) = Abs (f l) n (relabel f t)
relabel f (App l m n) = App (f l) (relabel f m) (relabel f n)

-- * Parsing

data SrcLoc
  = SrcLoc
  { line :: Int
  , col  :: Int
  }
  deriving (Show)

loc :: SourcePos -> SrcLoc
loc pos = SrcLoc (sourceLine pos) (sourceColumn pos)

-- | Context of names known in the current scope.
type Ctx = ([Name], [Name])

type Parser = Parsec String Ctx (Term SrcLoc)

getScope :: Parsec String Ctx [Name]
getScope = fst <$> getState

modifyScope :: ([Name] -> [Name]) -> Parsec String Ctx ()
modifyScope f = modifyState (\(x,y) -> (f x, y))

parseName :: Parsec String u Name
parseName = many1 (letter <|> char '\'')

parseAbs :: Parser -> Parser
parseAbs parseTerm = do
  char '\\'
  v <- parseName
  modifyScope (v:)
  char '.'
  term <- parseTerm
  modifyScope tail
  pos <- getPosition
  return (Abs (loc pos) v term)

parseVar :: Parser
parseVar = do
  v <- parseName
  (scope, syms) <- getState
  case (elemIndex v scope, elemIndex v syms) of
    (Just n, _) -> do
      pos <- getPosition
      return (Var (loc pos) v)
    (Nothing, Just n) -> do
      pos <- getPosition
      return (Sym (loc pos) v)
    _ -> fail ("Variable `" ++ v ++ "' is not in scope.")

parseTerm :: Parser
parseTerm = chainl1 parts (space >> getPosition >>= (return . App . loc))
  where
    parens :: Parsec String u a -> Parsec String u a
    parens = between (char '(') (char ')')
    parts :: Parser
    parts = parens parseTerm <|> parseAbs parseTerm <|> parseVar

-- | Parse lambda calculus 'Term's.
parse :: String -> Either [String] (Term SrcLoc)
parse = parseWithSymbols []

-- | Parse lambda calculus 'Term's with given symbols.
parseWithSymbols :: [Name] -> String -> Either [String] (Term SrcLoc)
parseWithSymbols syms =
  either (Left . (:[]) . show) (Right . id) .
  runParser parseTerm ([], syms) "<INPUT>"

-- | Format a 'Term'.
format :: Term a -> String
format = fmt 0
  where
    fmt _ (Var _ n) = n
    fmt _ (Sym _ n) = n
    fmt p (Abs _ n t) =
      let b = mconcat ["\\", n, ".", fmt 1 t]
      in if p > 1 then "(" ++ b ++ ")" else b
    fmt p (App _ m n) =
      let b = mconcat [fmt 2 m, " ", fmt 2 n]
      in if p >= 2 then "(" ++ b ++ ")" else b
