import Numeric.Natural
import Data.Maybe
import Debug.Trace

data FBExpr = Bounded Int --Only used in an application
            | Free Int --Only used in an application
            | FBApp FBExpr FBExpr
            | FBLambda FBExpr
    deriving (Show)

data Expr = Var Int
          | App Expr Expr
          | Lambda Expr

--From wikipedia:
--    find the instances of the variables n1, n2, ..., nk in M that are bound by the λ in λ M,
--    decrement the free variables of M to match the removal of the outer λ-binder, and
 --   replace n1, n2, ..., nk with N, suitably incrementing the free variables occurring in N each time, to match the number of λ-binders, under which the corresponding variable occurs when N substitutes for one of the ni.
apply :: Expr -> Expr -> Expr
apply m n = unIdentifyBound $ replaceIncrFree m'' n' 0
  where
    m''= mapFree (\x -> x-1) m'
    m' = identifyBounded m
    n' = identifyBounded n
    identifyBounded = identifyBounded' 0
    identifyBounded' b (Var i) | i<=b = Bounded i
                               | i> b = Free i
    identifyBounded' b (App e1 e2) = FBApp (identifyBounded' b e1) (identifyBounded' b e2)
    identifyBounded' b (Lambda e) = FBLambda $ identifyBounded' (b+1) e
    
    replaceIncrFree (Free i) n j | i==j = mapFree (+j) n
                                 | otherwise = Free i
    replaceIncrFree b@(Bounded _) _ _ = b
    replaceIncrFree (FBApp e1 e2) n j = FBApp (replaceIncrFree e1 n j) (replaceIncrFree e2 n j)
    replaceIncrFree (FBLambda e) n j = FBLambda $ replaceIncrFree e n (j+1)

    mapFree f (Free i) = Free $ f i
    mapFree f b@(Bounded _) = b
    mapFree f (FBApp e1 e2) = FBApp (mapFree f e1) (mapFree f e2)
    mapFree f (FBLambda e) = FBLambda $ mapFree f e

    unIdentifyBound (Bounded i) = Var i
    unIdentifyBound (Free i) = Var i
    unIdentifyBound (FBApp e1 e2) = App (unIdentifyBound e1) (unIdentifyBound e2)
    unIdentifyBound (FBLambda e) = Lambda $ unIdentifyBound e

    
    


simplify :: Expr -> Expr
simplify v@(Var _) = v
simplify (App e1 e2) = case simplify e1 of
                          Lambda e1' -> simplify $ apply e1' $ simplify e2
                          e1' -> App e1' $ simplify e2
simplify (Lambda e) = Lambda (simplify e)

replace v@(Var i1) i2 e2 | i1==i2 = e2
                         | otherwise = v
replace (App e1 e2) i e3 = App (replace e1 i e3) (replace e2 i e3)
replace (Lambda e1) i e2 = Lambda (replace e1 (i+1) e2)



data Token = TLambda | TNum Int | TOpen | TClosed | Ident String
  deriving (Show)

table = [("true" ,read "\\\\2"),
         ("false",read "\\\\1"),
         ("and",  read "\\\\2 1 2"),
         ("or",  read "\\\\2 2 1"),
         ("zero", read "false"),
         ("one", read "inc zero"),
         ("two", read "inc one"),
         ("three", read "inc two"),
         ("four", read "inc three"),
         ("five", read "inc four"),
         ("six", read "inc five"),
         ("seven", read "inc six"),
         ("eight", read "inc seven"),
         ("inc", read "\\\\\\ 2 (3 2 1)"),
         ("plus", read "\\\\\\\\ 4 2 (3 2 1)"),
         ("mul", read "\\\\\\\\ 4 (3 2) 1"),
         ("tuple", read "\\\\\\ 1 3 2"),
         ("triple", read "\\\\\\ 1 4 3 2"),
         ("fst", read "\\1 true"),
         ("snd", read "\\1 false"),
         ("fstt", read "\\1 (\\\\\\ 3)"),
         ("sndt", read "\\1 (\\\\\\ 2)"),
         ("trdt", read "\\1 (\\\\\\ 1)"),
         ("dec", read "\\\\\\snd (3 (\\tuple (3 (fst 1)) (fst 1)) (tuple 1 1))"),
         ("min", read "\\\\1 dec 2"),
         ("isZero", read "\\\\\\3 (\\false) true"),
         ("ifThenElse", read "\\\\\\ 3 2 1"),
         ("power", read "\\\\ 1 (mul 2) (inc zero)"),
         ("empty", read "triple false false false"),
         ("cons", read "\\\\triple true 2 1"),
         ("isNotEmpty", read "\\fstt 1"),
         ("map", read "\\\\ifThenElse (isNotEmpty 1) (cons (2 (sndt 1)) (map 2 (trdt 1))) empty"),
         ("exampleList", read "cons one (cons five (cons eight empty))"),
         ("powerexample", read "map (power (inc (inc zero))) exampleList")]
-- Expr0 = (Expr2) | n | name
-- Expr1 =  Expr0*
-- Expr2 = \ Expr2 | Expr1

parse1 :: [Token] -> Maybe (Expr,[Token])
parse1 (Ident s:ts) = (\expr->(expr,ts)) <$> lookup s table
parse1 (TOpen:ts) = do
                      (expr,rest) <- parse3 ts
                      return (expr,tail rest)
parse1 (TNum i:ts) = Just (Var i,ts)
parse1 _ = Nothing
parseList :: [Token] -> ([Expr],[Token])
parseList ts = case parse1 ts of
                       Just (expr,rest) -> (expr:exprs, rest')
                                             where
                                               (exprs,rest') = parseList rest
                       Nothing -> ([],ts)
  where
parse2 ts = case parseList ts of
              ([],_) -> Nothing
              (xs,rest) -> Just $ (foldl1 App xs,rest)
parse3 (TLambda:ts) = do
                        (expr,rest) <- parse3 ts
                        Just (Lambda expr,rest)
parse3 ts = parse2 ts

parse :: [Token] -> Expr
parse ts = case parse3 ts of
              Just (expr,rest) -> expr
              Nothing -> error "parse error"


--parser :: [Token] -> Expr
--parser = fst . parser'
--
--parser' :: [Token] -> (Expr,[Token])
--parser' (TLambda:ts) = (Lambda e, remaining)
--  where (e,remaining) = parser' ts
--parser' (TNum i:ts) = (foldl App (Var i) args,remaining)
--  where (args,remaining) = getArgs ts
--
--getArgs :: [Token] -> ([Expr],[Token])
--getArgs [] = ([],[])
--getArgs (TClosed:ts) = ([],ts)
--getArgs ts = arg:(getArgs remaining)
--  where (arg,remaining) = parser' ts

isAlpha :: Char -> Bool
isAlpha c = 'a' <= c && c <= 'z' || 'A' <= c && c <= 'Z'



getWord :: String -> (String,String)
getWord (c:cs) = if isAlpha c then (c:after,rest) else ([],c:cs)
  where (after,rest) = getWord cs
getWord [] = ([],[])

lexer :: String -> [Token]
lexer ('\\':xs) = TLambda : lexer xs
lexer (' ':xs) = lexer xs
lexer ('(':xs) = TOpen : lexer xs
lexer (')':xs) = TClosed : lexer xs
lexer (x:xs) | '0'<=x && x<='9' = TNum (read num) : lexer rest
             | otherwise = Ident word:lexer rest'
  where (num,rest) = getNum (x:xs)
        (word,rest') = getWord (x:xs)
        getNum (x:xs) | '0'<=x && x<='9' = (x : (fst $ getNum xs),snd $ getNum xs)
                      | otherwise = ("",(x:xs))
        getNum [] = ([],[])
lexer [] = []

instance Read Expr where
  readsPrec _ str = [((parse . lexer) str,"")]
instance Show Expr where
  show (Var i) = show i
  show (App expr1 expr2) = "("++show expr1++" "++show expr2++")"
  show (Lambda expr) = "\\"++show expr