Ticket #2807: lamb.hs

File lamb.hs, 5.2 KB (added by celes, 6 years ago)
Line 
1--bug todo verify full lazy
2--idea: try to take things out of V and use Fun instead
3--how does running size optimizer first help speed if full lazy? makes env list smaller?
4--investigate timeout on '5'
5--expand \a.I = church 0
6--make errors for apply inc,00 instead of succ,0
7--does pattern matching rhs of app ruin some lazyness?
8--untitled 619 slow why?
9--cons pred not working
10--remove unused vars from e list in eval
11import System (getArgs)
12import Char
13import IO
14
15chri :: Integer -> Char
16chri i = chr (fromInteger i `mod` 256)
17ordi :: Char -> Integer
18ordi c = toInteger (ord c)
19--monus a b = if a < b then 0 else a - b
20
21data T = Var Int
22       | Lam T
23       | App T T
24       | Num Integer
25       | Succa
26       | Adda
27       | Composea
28       | Preda
29       deriving (Show)
30data V = Fun (V -> V)
31       | Church Integer
32       | Succ
33       | Pred
34       | List [Integer]
35       | Add Integer
36       | Compose
37       | Mult Integer
38       | Add1
39
40app :: V -> V -> V
41app (Fun f) v = f v
42app (List []) _ = Church 1
43app (List (x:xs)) f = f `app` Church x `app` List xs
44app (Church 0) _ = Church 1
45app (Church 1) f = f
46app (Church i) (Church j) = Church(j^i)
47app (Church i) Succ = Add i
48app (Church i) (Add j) = Add (i*j) --todo verify
49app (Church i) f = Fun (\x -> f `app` (Church (i-1) `app` f `app` x))
50app Succ (Church i) = Church (i+1) -- this check is not be lazy
51app Succ a = Fun (\f-> Fun (\x->f `app` (a `app` f `app` x)))
52app (Add i) (Church j) = Church(i+j)
53app (Add n) m = Fun (\f -> Fun (\x -> (Church n) `app` f `app` (m `app` f `app` x)))
54app Add1 (Church i) = Add i
55app Add1 a = Fun (\b-> Fun (\f-> Fun (\x-> a `app` f `app` (b `app` f `app` x))))
56
57--add cases for 0,1 so check for 2nd arg is lazy??
58app Compose (Church i) = Mult i
59app Compose n = Fun (\m -> Fun (\f -> n `app` (m `app` f)))
60app (Mult i) (Church j) = Church (i*j)
61app (Mult i) m = Fun (\f -> Church i `app` (m `app` f))
62
63app Pred i = Fun (\n -> case n of
64        -- (Church j) -> if j > 0 then i `app` Church (j-1) else Church 0
65        _ -> Fun (\f -> Fun (\x -> n `app` Fun (\g -> Fun (\h -> h `app` (g `app` f))) `app` Fun (\u -> x) `app` i)))
66
67eval :: T -> [V] -> V
68eval (Num i) _ = Church i
69eval Succa _ = Succ
70eval Composea _ = Compose
71eval Adda _ = Add1
72eval Preda _ = Pred
73eval (Var x) e = e !! x
74eval (Lam t) e = Fun (\v -> eval t (v:e))
75eval (App a b) e = eval a e `app` eval b e
76
77clean :: T -> T
78clean (Var x) = Var x
79clean (Lam t) = clean' (Lam (clean t))
80clean (App a b) = App (clean a) (clean b)
81clean a = a
82
83clean' (Lam (f `App` Var 0)) | free f 0 = unabs f
84clean' a = a
85
86numberize :: T -> T
87numberize (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 =
88        Preda `App` numberize (clean (unabs (unabs i))) `App` numberize (clean (unabs (unabs n)))
89
90numberize (Lam (n `App` (m `App` Var 0))) | free n 0 && free m 0 =
91        Composea `App` numberize (unabs n) `App` numberize (unabs m)
92
93numberize (Lam (Lam (Var 0))) = Num 0
94numberize (Lam (Var 0)) = Num 1
95
96numberize (Lam (Lam (Var 1 `App` f))) =
97        Succa `App` numberize (clean (Lam (Lam f)))
98
99numberize (Lam (Lam (n `App` Var 1 `App` f))) | free n 0 && free n 1 =
100        Adda `App` numberize (unabs (unabs n)) `App` numberize (clean (Lam (Lam f)))
101
102numberize (Var x) = Var x
103numberize (Lam t) = Lam (numberize t)
104numberize (App a b) = App (numberize a) (numberize b)
105
106free :: T -> Int -> Bool
107free (Var x) i = x /= i
108free (Lam t) i = free t (i+1)
109free (App a b) i = free a i && free b i
110free _ _ = True
111
112unabs :: T -> T
113unabs = unabs' 0 where
114        unabs' i (Var x) | x >= i = Var (x-1)
115                         | otherwise = Var x
116        unabs' i (Lam t) = Lam (unabs' (i+1) t)
117        unabs' i (App a b) = App (unabs' i a) (unabs' i b)
118        unabs' _ a = a
119
120iToList :: V -> V
121iToList i = Fun (\rhs -> tolist (show (unchurch i) ++ unlist rhs))
122
123listToI :: V -> V
124--listToI s = error (show (map (chri) (snd (digits (unlist' s))))) where
125listToI s = List (read ('0':map chri a):b) where
126        (a,b) = span digits (snd (break digits (unlist' s)))
127        digits = isDigit . chri
128
129unchurch :: V -> Integer
130unchurch (Church i) = i
131unchurch f = i where (Church i) = f `app` Succ `app` Church 0
132tolist :: String -> V
133tolist = List . map ordi
134unlist :: V -> String
135unlist = map chri . unlist'
136unlist' (List i) = i
137unlist' s = shedlist $ s `app` Fun (\a -> Fun (\b -> Fun (\i -> 
138                List (unchurch a : unlist' b)))) `app` List [] where
139        shedlist (List i) = i
140       
141type BitStream = ([Int], String)
142stepBit :: BitStream -> (Int, BitStream)
143stepBit (x:xs, ys) = (x, (xs, ys))
144stepBit ([], y:ys) = ((ord y) `div` 128, (map (\p->(ord y) `div` 2^p `mod` 2) [6,5..0], ys))
145
146parse :: BitStream -> (T, BitStream)
147parse s =
148        if a == 1 then getVar s2 0
149        else
150                if b == 0 then (Lam e1, r1)
151                else (App e1 e2, r2)
152        where
153                (a,s2) = stepBit s
154                (b,s3) = stepBit s2
155                (e1,r1) = parse(s3)
156                (e2,r2) = parse(r1)
157                getVar s i = 
158                        if a==1 then getVar s2 (i+1)
159                        else (Var i, s2)
160                        where (a,s2) = stepBit s
161
162main = do
163        sources <- mapM readFile =<< getArgs
164        hSetBuffering stdout NoBuffering -- because haskell does not flush on error
165        interact (\input -> 
166                let stream = ([], concat sources ++ input)
167                    (tree, (_, rest)) = parse stream
168                    tree2 = clean (numberize tree)
169                    builtin = [Fun iToList, Fun listToI]
170                    output = unlist $ eval tree2 builtin `app` tolist rest
171                in (show tree2) ++ "\n" ++ output)