module Lambda where

{- 
   Ez a cikkben megadott lambda kalkulus egy implementacioja + redukcio + peldak.

   Hasznalat: lasd Lambda_proof.hs

 -}
import Data.List
import qualified Data.Set as Set
import Data.Char

data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L
    | Shift L L L | Unsized | Bottom 
    deriving (Eq, Ord)

showVar x = if x>28 
    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
    else showChar $ chr $ ord 'a' + x

getPrec :: Char -> (Int,Int,Int)
getPrec '+' = (4,4,5)
getPrec '-' = (4,4,5)
getPrec '*' = (5,5,6)
getPrec '/' = (5,5,6)
getPrec c   = error $ "Unknown operator "++[c]

instance Show L where
    showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . shows l
    showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . shows l
    showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n
    showsPrec _ (Var s) = showVar s
    showsPrec _ (Num i) = shows i
    showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n
        where (prec,lprec,rprec)=getPrec op
    showsPrec p (List s f) = showParen (p>0) $ showString "List " . showsPrec 9 s . showChar ' ' . showsPrec 9 f
    showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 .
        showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2
    showsPrec _ Bottom = showChar '┴'
    showsPrec _ Unsized = showChar 'U'

t3s = Abs 1 $ Abs 0 $ App t (App t (App t x))
    where t = Var 1
          x = Var 0

subs (App x z)   var exp = App (subs x var exp) (subs z var exp)
subs (List s f)  var exp = List (subs s var exp) (subs f var exp)
subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp)
subs (Op x c z)  var exp = Op (subs x var exp) c (subs z var exp)
subs e@(Var v)   var exp | v==var    = exp
                         | otherwise = e
subs x@(Abs v e) var exp | v==var    = x
                         | otherwise = Abs v (subs e var exp)
subs x@(AAbs s f e) var exp | s==var||f==var = x
                            | otherwise = AAbs s f (subs e var exp)
subs x@(Num _)   _ _ = x
subs x@Bottom    _ _ = x
subs x@Unsized   _ _ = x


alpha (App x z)   from to = App (alpha x from to) (alpha z from to)
alpha (List x z)  from to = List (alpha x from to) (alpha z from to)
alpha (Op x c z)  from to = Op (alpha x from to) c (alpha z from to)
alpha (Shift x y z) from to = Shift (alpha x from to) (alpha y from to) (alpha z from to)
alpha e@(Var _)   _    _  = e
alpha e@(Num _)   _    _  = e
alpha e@Bottom   _    _  = e
alpha e@Unsized   _    _  = e
alpha (Abs v e) from to | v==from   = Abs to (alpha' e from to)
                        | otherwise = Abs v (alpha e from to)
alpha (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
                             | v2==from  = AAbs v1 to (alpha' e from to)
                             | otherwise = AAbs v1 v2 (alpha e from to)

alpha' (App x z)   from to = App (alpha' x from to) (alpha' z from to)
alpha' (List x z)  from to = List (alpha' x from to) (alpha' z from to)
alpha' (Op x c z)  from to = Op (alpha' x from to) c (alpha' z from to)
alpha' (Shift x y z) from to = Shift (alpha' x from to) (alpha' y from to) (alpha' z from to)
alpha' e@(Var v)   from to | v==from   = Var to
                           | otherwise = e
alpha' (Abs v e) from to | v==from   = Abs to (alpha' e from to)
                         | otherwise = Abs v (alpha' e from to)
alpha' (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
                              | v2==from  = AAbs v1 to (alpha' e from to)
                              | otherwise = AAbs v1 v2 (alpha' e from to)
alpha' x@(Num _)   _    _  = x
alpha' x@Bottom   _    _  = x
alpha' x@Unsized   _    _  = x

fv (Var x) = Set.singleton x
fv (App x y) = fv x `Set.union` fv y
fv (Op x _ y) = fv x `Set.union` fv y
fv (Abs v e) = v `Set.delete` fv e 
fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e)
fv (List s e) = fv s `Set.union` fv e
fv (Num _) = Set.empty
fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3
fv Unsized = Set.empty
fv Bottom = Set.empty

bv (Var _) = Set.empty
bv (App x y) = bv x `Set.union` bv y
bv (Op x _ y) = bv x `Set.union` bv y
bv (List x y) = bv x `Set.union` bv y
bv (Abs v e) = v `Set.insert` bv e
bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e)
bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3
bv (Num _)   = Set.empty
bv Unsized = Set.empty
bv Bottom = Set.empty

maxv (Var x)   = x
maxv (Num _)   = 0
maxv Unsized = 0
maxv Bottom = 0
maxv (App x y) = maxv x `max` maxv y
maxv (Op x _ y) = maxv x `max` maxv y
maxv (Shift x y z) = maxv x `max` maxv y `max` maxv z
maxv (List x y) = maxv x `max` maxv y
maxv (Abs v e) = v `max` maxv e
maxv (AAbs v1 v2 e) = v1 `max` v2 `max` maxv e

rsubs oexp var exp = subs renamed var exp
    where
    dvar = fv exp `Set.intersection` bv oexp
    m = maxv exp `max` maxv oexp
    renames = zip (Set.toList dvar) [m+1..]
    renamed = foldr rename oexp renames
    rename (from,to) _ = alpha oexp from to


reduce (App (Abs var exp) z) = return $ rsubs exp var z
reduce (App (AAbs s f exp) (List s' f')) = return $ rsubs (App (Abs f exp) f') s s'
reduce (App e f) = case reduce e of
        Just e' -> return $ App e' f
        _       -> reduce f >>= \f' -> return $ App e f'
reduce (Abs v e) = reduce e >>= \e' -> return $ Abs v e'
reduce (Var _) = Nothing
reduce (Num _) = Nothing
reduce (List e f) = case reduce e of
        Just e' -> return $ List e' f
        _       -> reduce f >>= \f' -> return $ List e f'
reduce (AAbs v1 v2 e) = reduce e >>= \e' -> return $ AAbs v1 v2 e'
reduce Unsized = Nothing
reduce Bottom  = Nothing
reduce (Shift e1 e2 e3) = case reduce e1 of
        Just e' -> return $ Shift e' e2 e3
        _       -> case reduce e2 of
            Just e' -> return $ Shift e1 e' e3
            _       -> reduce e3 >>= \e' -> return $ Shift e1 e2 e'
reduce (Op m c n) = case c of
    '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j
    '-' | (Num i, Num j) <- (m,n) -> return $ Num $ i-j
    '*' | (Num i, Num j) <- (m,n) -> return $ Num $ i*j
    '+' | (Num 0) <- m            -> reduce n
    '+' | (Num 0) <- n            -> reduce m
    '*' | (Num 0) <- m            -> return $ Num 0
    '*' | (Num 0) <- n            -> return $ Num 0
    '*' | (Num 1) <- m            -> reduce n
    '*' | (Num 1) <- n            -> reduce m
    '-' | (Num 0) <- n            -> reduce m
    _ ->  case reduce m of
        Just m' -> return $ Op m' c n
        _       -> reduce n >>= \n' -> return $ Op m c n'

r :: Maybe L -> Maybe L
r x = x >>= reduce 

it f x = it' f (Just x)
    where
    it' _ Nothing  = []
    it' f (Just x) = x:it' f (f x)

rchain :: L -> [L]
rchain = it reduce

pchain = putStrLn . intercalate "\n-> " . map show . rchain

lplus = Abs m $ Abs n $ Abs f $ Abs x $ App (App (Var m) (Var f)) $ App (App (Var n) (Var f)) (Var x)
    where [m,n,f,x] = [0..3]
lzero = Abs f $ Abs x $ Var x
    where [f,x] = [0,1]
lsucc = Abs n $ Abs f $ Abs x $ App (Var f) $ App (App (Var n) (Var f)) (Var x)
    where [n,f,x] = [0..2]
lone = last $ it reduce $ App lsucc lzero
ltwo = last $ it reduce $ App lsucc lone

lpred = Abs n $ Abs f $ Abs x $ App (App (App (Var n) u1) (Abs u $ Var x)) (Abs u $ Var u)
    where 
    u1 = Abs g $ Abs h $ App (Var h) $ App (Var g) (Var f)
    [n,f,x,g,h,u] = [0..5]
    
lsub = Abs m $ Abs n $ App (App (Var n) lpred) (Var m)
    where (m,n) = (0,1)

ltrue = Abs 0 $ Abs 1 $ Var 0
lfalse = Abs 0 $ Abs 1 $ Var 1

liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue
    where (n,x) = (0,1)

land = Abs 0 $ Abs 1 $ App (App (Var 0) (Var 1)) (Var 1)
lleq = Abs 0 $ Abs 1 $ App liszero $ App (App lsub (Var 0)) (Var 1)
leq = Abs 0 $ Abs 1 $ App (App land l1) l2
    where
    l1 = App (App lleq (Var 0)) (Var 1)
    l2 = App (App lleq (Var 1)) (Var 0)

test = Abs 0 $ Abs 1 $ App (App leq xpy) ypx
xpy = App (App lplus (Var 0)) (Var 1)
ypx = App (App lplus (Var 1)) (Var 0)

smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
conss = Abs 23 $ AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Var 19)  (Abs 8 $ Var 23)
addones = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) (Abs 8 Unsized)
nils = List (Num 0) (Abs 8 Bottom)
lz n = List (Num n) (Abs 8 Unsized)
srep n x = List (Num n) (Abs 8 x)
dupfst = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Op (Var 19) '-' (Num 1)) 
    $ Abs 8 $ App (Var 5) (Op (Var 19) '-' (Num 1))
yComb = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22)))
-- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i))
reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) )
reverse' l = case l of
    [] -> []
    (x:xs) -> x:reverse' xs
appends = AAbs 18 5 $ AAbs 19 6 $ List (Op (Var 18) '+' (Var 19)) $ Shift (Var 6) (Var 19) (Var 5)

headc = AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))
tailc = AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)
rall = last . it reduce 

sheads = rall $ App smap headc
stails = rall $ App smap tailc