Ticket #2807: lamb.hs

--bug todo verify full lazy
--idea: try to take things out of V and use Fun instead
--how does running size optimizer first help speed if full lazy? makes env list smaller?
--investigate timeout on '5'
--expand \a.I = church 0
--make errors for apply inc,00 instead of succ,0
--does pattern matching rhs of app ruin some lazyness?
--untitled 619 slow why?
--cons pred not working
--remove unused vars from e list in eval
import System (getArgs)
import Char
import IO

chri :: Integer -> Char
chri i = chr (fromInteger i `mod` 256)
ordi :: Char -> Integer
ordi c = toInteger (ord c)
--monus a b = if a < b then 0 else a - b

data T = Var Int
       | Lam T
       | App T T
       | Num Integer
       | Succa
       | Adda
       | Composea
       | Preda
       deriving (Show)
data V = Fun (V -> V)
       | Church Integer
       | Succ
       | Pred
       | List [Integer]
       | Add Integer
       | Compose
       | Mult Integer
       | Add1

app :: V -> V -> V
app (Fun f) v = f v
app (List []) _ = Church 1
app (List (x:xs)) f = f `app` Church x `app` List xs
app (Church 0) _ = Church 1
app (Church 1) f = f
app (Church i) (Church j) = Church(j^i)
app (Church i) Succ = Add i
app (Church i) (Add j) = Add (i*j) --todo verify
app (Church i) f = Fun (\x -> f `app` (Church (i-1) `app` f `app` x))
app Succ (Church i) = Church (i+1) -- this check is not be lazy
app Succ a = Fun (\f-> Fun (\x->f `app` (a `app` f `app` x)))
app (Add i) (Church j) = Church(i+j)
app (Add n) m = Fun (\f -> Fun (\x -> (Church n) `app` f `app` (m `app` f `app` x)))
app Add1 (Church i) = Add i
app Add1 a = Fun (\b-> Fun (\f-> Fun (\x-> a `app` f `app` (b `app` f `app` x))))

--add cases for 0,1 so check for 2nd arg is lazy??
app Compose (Church i) = Mult i
app Compose n = Fun (\m -> Fun (\f -> n `app` (m `app` f)))
app (Mult i) (Church j) = Church (i*j)
app (Mult i) m = Fun (\f -> Church i `app` (m `app` f))

app Pred i = Fun (\n -> case n of
        -- (Church j) -> if j > 0 then i `app` Church (j-1) else Church 0
        _ -> Fun (\f -> Fun (\x -> n `app` Fun (\g -> Fun (\h -> h `app` (g `app` f))) `app` Fun (\u -> x) `app` i)))

eval :: T -> [V] -> V
eval (Num i) _ = Church i
eval Succa _ = Succ
eval Composea _ = Compose
eval Adda _ = Add1
eval Preda _ = Pred
eval (Var x) e = e !! x
eval (Lam t) e = Fun (\v -> eval t (v:e))
eval (App a b) e = eval a e `app` eval b e

clean :: T -> T
clean (Var x) = Var x
clean (Lam t) = clean' (Lam (clean t))
clean (App a b) = App (clean a) (clean b)
clean a = a

clean' (Lam (f `App` Var 0)) | free f 0 = unabs f
clean' a = a

numberize :: T -> T
numberize (Lam (Lam (App (App (App n (Lam (Lam (App (Var 0) (App (Var 1) (Var 3)))))) (Lam (Var 1))) i))) | free n 0 && free n 1 && free i 0 && free i 1 =
        Preda `App` numberize (clean (unabs (unabs i))) `App` numberize (clean (unabs (unabs n)))

numberize (Lam (n `App` (m `App` Var 0))) | free n 0 && free m 0 =
        Composea `App` numberize (unabs n) `App` numberize (unabs m)

numberize (Lam (Lam (Var 0))) = Num 0
numberize (Lam (Var 0)) = Num 1

numberize (Lam (Lam (Var 1 `App` f))) =
        Succa `App` numberize (clean (Lam (Lam f)))

numberize (Lam (Lam (n `App` Var 1 `App` f))) | free n 0 && free n 1 =
        Adda `App` numberize (unabs (unabs n)) `App` numberize (clean (Lam (Lam f)))

numberize (Var x) = Var x
numberize (Lam t) = Lam (numberize t)
numberize (App a b) = App (numberize a) (numberize b)

free :: T -> Int -> Bool
free (Var x) i = x /= i
free (Lam t) i = free t (i+1)
free (App a b) i = free a i && free b i
free _ _ = True

unabs :: T -> T
unabs = unabs' 0 where
        unabs' i (Var x) | x >= i = Var (x-1)
                         | otherwise = Var x
        unabs' i (Lam t) = Lam (unabs' (i+1) t)
        unabs' i (App a b) = App (unabs' i a) (unabs' i b)
        unabs' _ a = a

iToList :: V -> V
iToList i = Fun (\rhs -> tolist (show (unchurch i) ++ unlist rhs))

listToI :: V -> V
--listToI s = error (show (map (chri) (snd (digits (unlist' s))))) where
listToI s = List (read ('0':map chri a):b) where
        (a,b) = span digits (snd (break digits (unlist' s)))
        digits = isDigit . chri

unchurch :: V -> Integer
unchurch (Church i) = i
unchurch f = i where (Church i) = f `app` Succ `app` Church 0
tolist :: String -> V
tolist = List . map ordi
unlist :: V -> String
unlist = map chri . unlist'
unlist' (List i) = i
unlist' s = shedlist $ s `app` Fun (\a -> Fun (\b -> Fun (\i -> 
                List (unchurch a : unlist' b)))) `app` List [] where
        shedlist (List i) = i
        
type BitStream = ([Int], String)
stepBit :: BitStream -> (Int, BitStream)
stepBit (x:xs, ys) = (x, (xs, ys))
stepBit ([], y:ys) = ((ord y) `div` 128, (map (\p->(ord y) `div` 2^p `mod` 2) [6,5..0], ys))

parse :: BitStream -> (T, BitStream)
parse s =
        if a == 1 then getVar s2 0
        else
                if b == 0 then (Lam e1, r1)
                else (App e1 e2, r2)
        where
                (a,s2) = stepBit s
                (b,s3) = stepBit s2
                (e1,r1) = parse(s3)
                (e2,r2) = parse(r1)
                getVar s i = 
                        if a==1 then getVar s2 (i+1)
                        else (Var i, s2)
                        where (a,s2) = stepBit s

main = do
        sources <- mapM readFile =<< getArgs
        hSetBuffering stdout NoBuffering -- because haskell does not flush on error
        interact (\input -> 
                let stream = ([], concat sources ++ input)
                    (tree, (_, rest)) = parse stream
                    tree2 = clean (numberize tree)
                    builtin = [Fun iToList, Fun listToI]
                    output = unlist $ eval tree2 builtin `app` tolist rest
                in (show tree2) ++ "\n" ++ output)