diff options
Diffstat (limited to 'prototypes')
-rw-r--r-- | prototypes/ShiftReducer.hs | 696 |
1 files changed, 696 insertions, 0 deletions
diff --git a/prototypes/ShiftReducer.hs b/prototypes/ShiftReducer.hs new file mode 100644 index 00000000..ae515b08 --- /dev/null +++ b/prototypes/ShiftReducer.hs | |||
@@ -0,0 +1,696 @@ | |||
1 | {-# language ScopedTypeVariables #-} | ||
2 | {-# language LambdaCase #-} | ||
3 | {-# language TypeOperators #-} | ||
4 | {-# language TypeFamilies #-} | ||
5 | {-# language ViewPatterns #-} | ||
6 | {-# language PatternGuards #-} | ||
7 | {-# language PatternSynonyms #-} | ||
8 | {-# language RankNTypes #-} | ||
9 | {-# language DataKinds #-} | ||
10 | {-# language KindSignatures #-} | ||
11 | {-# language GADTs #-} | ||
12 | {-# language DeriveFunctor #-} | ||
13 | {-# language DeriveGeneric #-} | ||
14 | {-# language DefaultSignatures #-} | ||
15 | {-# language FlexibleInstances #-} | ||
16 | {-# language FlexibleContexts #-} | ||
17 | {-# language TemplateHaskell #-} -- for testing | ||
18 | {-# language NoMonomorphismRestriction #-} | ||
19 | |||
20 | import Data.Monoid | ||
21 | import Data.Maybe | ||
22 | import Data.List | ||
23 | import Data.Map (Map) | ||
24 | import qualified Data.Map as Map | ||
25 | import qualified Data.Set as Set | ||
26 | import Control.Monad | ||
27 | import Control.Arrow hiding (app) | ||
28 | import Test.QuickCheck | ||
29 | import Test.QuickCheck.Function | ||
30 | import GHC.Generics | ||
31 | import Debug.Trace | ||
32 | |||
33 | ------------------------------------------------------------ utils | ||
34 | |||
35 | iterateN i f x = iterate f x !! i | ||
36 | |||
37 | (<&>) = flip (<$>) | ||
38 | |||
39 | data Void | ||
40 | |||
41 | instance Eq Void where (==) = error "(==) @Void" | ||
42 | instance Show Void where show = error "show @Void" | ||
43 | |||
44 | {- used later? | ||
45 | -- supplementary data: data with no semantic relevance | ||
46 | newtype SData a = SData a | ||
47 | instance Show (SData a) where show _ = "SData" | ||
48 | instance Eq (SData a) where _ == _ = True | ||
49 | instance Ord (SData a) where _ `compare` _ = EQ | ||
50 | -} | ||
51 | |||
52 | ------------------------------------------------------------ streams | ||
53 | |||
54 | -- streams with constant tails | ||
55 | -- invariant property: Repeat is used when possible (see cons) | ||
56 | data Stream a | ||
57 | = Cons a (Stream a) | ||
58 | | Repeat a | ||
59 | deriving (Eq, Show, Functor) -- Functor is not proper, may break invariant | ||
60 | |||
61 | -- smart constructor to construct normal form of streams | ||
62 | cons b (Repeat b') | b == b' = Repeat b' | ||
63 | cons b x = Cons b x | ||
64 | |||
65 | -- stream head | ||
66 | sHead (Cons a _) = a | ||
67 | sHead (Repeat a) = a | ||
68 | |||
69 | -- stream tail | ||
70 | sTail (Cons _ a) = a | ||
71 | sTail (Repeat a) = Repeat a | ||
72 | |||
73 | instance Applicative Stream where | ||
74 | pure a = Repeat a | ||
75 | -- (<*>) is not proper, may break invariant | ||
76 | Repeat f <*> Repeat a = Repeat $ f a | ||
77 | x <*> y = Cons{-should be cons-} (sHead x $ sHead y) (sTail x <*> sTail y) | ||
78 | |||
79 | foldStream :: (b -> a -> a) -> (b -> a) -> Stream b -> a | ||
80 | foldStream f g (Cons b u) = f b (foldStream f g u) | ||
81 | foldStream f g (Repeat b) = g b | ||
82 | |||
83 | -- final value in the stream | ||
84 | limes :: Stream a -> a | ||
85 | limes = foldStream const id | ||
86 | |||
87 | -- replace limes by given stream | ||
88 | sCont :: Eq a => Stream a -> (a -> Stream a) -> Stream a | ||
89 | sCont as f = foldStream cons f as | ||
90 | |||
91 | -- semantics of Stream | ||
92 | streamToList :: Stream a -> [a] | ||
93 | streamToList = foldStream (:) repeat | ||
94 | |||
95 | streamToFun :: Stream a -> Int -> a | ||
96 | streamToFun u i = streamToList u !! i | ||
97 | |||
98 | sFromList :: Eq a => [a] -> a -> Stream a | ||
99 | sFromList xs b = foldr cons (Repeat b) xs | ||
100 | |||
101 | instance (Arbitrary a, Eq a) => Arbitrary (Stream a) where | ||
102 | arbitrary = sFromList <$> arbitrary <*> arbitrary | ||
103 | |||
104 | -- iterate on stream | ||
105 | sIterate :: Eq a => (a -> a) -> a -> Stream a | ||
106 | sIterate f x | ||
107 | | y == x = Repeat x | ||
108 | | otherwise = Cons x $ sIterate f y | ||
109 | where | ||
110 | y = f x | ||
111 | |||
112 | sCatMaybes :: Stream (Maybe a) -> [a] | ||
113 | sCatMaybes = foldStream (\m s -> maybe s (:s) m) (maybe [] repeat) | ||
114 | |||
115 | ---------------------------------------------------------- operations involving Boolean streams | ||
116 | |||
117 | mergeStreams :: Eq a => Stream Bool -> Stream a -> Stream a -> Stream a | ||
118 | mergeStreams (Cons True u) as bs = cons (sHead as) $ mergeStreams u (sTail as) bs | ||
119 | mergeStreams (Cons False u) as bs = cons (sHead bs) $ mergeStreams u as (sTail bs) | ||
120 | mergeStreams (Repeat True) as bs = as | ||
121 | mergeStreams (Repeat False) as bs = bs | ||
122 | |||
123 | sFilter :: Stream Bool -> [a] -> [a] | ||
124 | sFilter (Cons True u) is = take 1 is ++ sFilter u (drop 1 is) | ||
125 | sFilter (Cons False u) is = sFilter u (drop 1 is) | ||
126 | sFilter (Repeat True) is = is | ||
127 | sFilter (Repeat False) is = [] | ||
128 | |||
129 | -- sFilter for streams | ||
130 | -- the first stream is used when no more element can pass the filter | ||
131 | filterStream :: Eq a => Stream a -> Stream Bool -> Stream a -> Stream a | ||
132 | filterStream d (Cons True s) as = cons (sHead as) $ filterStream d s $ sTail as | ||
133 | filterStream d (Cons False s) as = filterStream d s $ sTail as | ||
134 | filterStream d (Repeat True) as = as | ||
135 | filterStream d (Repeat False) as = d | ||
136 | |||
137 | sOr :: Stream Bool -> Stream Bool -> Stream Bool | ||
138 | sOr (Cons b u) (Cons b' u') = cons (b || b') $ sOr u u' | ||
139 | sOr (Repeat False) u = u | ||
140 | sOr (Repeat True) u = Repeat True | ||
141 | sOr u (Repeat False) = u | ||
142 | sOr u (Repeat True) = Repeat True | ||
143 | |||
144 | prop_sOr_idemp a = sOr a a == a | ||
145 | prop_sOr_comm a b = sOr a b == sOr b a | ||
146 | |||
147 | dbAnd a b = not <$> sOr (not <$> a) (not <$> b) | ||
148 | |||
149 | instance Monoid (Stream Bool) where | ||
150 | mempty = Repeat False | ||
151 | mappend = sOr | ||
152 | |||
153 | prop_StreamBool_monoid_left (a :: Stream Bool) = mempty <> a == a | ||
154 | prop_StreamBool_monoid_right (a :: Stream Bool) = a <> mempty == a | ||
155 | prop_StreamBool_monoid_assoc (a :: Stream Bool) b c = (a <> b) <> c == a <> (b <> c) | ||
156 | |||
157 | -- composition of (Stream Bool) values (by sFilter semantics) | ||
158 | sComp :: Stream Bool -> Stream Bool -> Stream Bool | ||
159 | sComp bs as = mergeStreams bs as $ Repeat False | ||
160 | |||
161 | prop_sComp a b xs = sFilter (sComp a b) xs == (sFilter b . sFilter a) xs | ||
162 | prop_sComp_trans a b (getNonNegative -> i) = indexTrans (sComp a b) i == (indexTrans a =<< indexTrans b i) | ||
163 | |||
164 | filterDBUsed :: Stream Bool -> Stream Bool -> Stream Bool | ||
165 | filterDBUsed = filterStream $ Repeat False | ||
166 | |||
167 | --prop_filterDBUsed bs = mergeStreams bs xs ys sOr b a `sComp` filterDBUsed (sOr b a) a == a | ||
168 | |||
169 | prop_filterDBUsed a b = sOr b a `sComp` filterDBUsed (sOr b a) a == a | ||
170 | |||
171 | compress s = filterDBUsed s s | ||
172 | |||
173 | |||
174 | --takeUps :: Int -> Stream Bool -> Stream Bool | ||
175 | --takeUps i = (`sComp` sFromList (replicate i True) False) | ||
176 | |||
177 | --prop_takeUps (getNonNegative -> n) u = streamToList (takeUps n u) == normSem (take n $ streamToList u) | ||
178 | |||
179 | --takeUps' :: Int -> Stream Bool -> Stream Bool | ||
180 | --takeUps' i = sComp $ sFromList (replicate i True) False | ||
181 | |||
182 | --prop_takeUps' u (getNonNegative -> n) = streamToList (takeUps' n u) == head (dropWhile ((< n) . length . filter id) (inits $ streamToList u) ++ [streamToList u]) | ||
183 | |||
184 | --------------------------------------------------------------- indices | ||
185 | |||
186 | -- index of the first appearance of the limes | ||
187 | limesIndex :: Stream a -> Int | ||
188 | limesIndex = foldStream (const (+1)) (const 0) | ||
189 | |||
190 | -- indices at which the stream value is True | ||
191 | trueIndices :: Stream Bool -> [Int] | ||
192 | trueIndices s = sFilter s [0..] | ||
193 | |||
194 | prop_trueIndices (getExpDB -> u) = all (streamToFun u) $ trueIndices u | ||
195 | |||
196 | invTrueIndices :: [Int] -> Stream Bool | ||
197 | invTrueIndices = f 0 where | ||
198 | f i [] = Repeat False | ||
199 | f i (k: ks) = iterateN (k - i) (cons False) $ cons True $ f (k + 1) ks | ||
200 | |||
201 | prop_invTrueIndices (map getNonNegative . Set.toList -> ks) = trueIndices (invTrueIndices ks) == ks | ||
202 | prop_invTrueIndices' (getExpDB -> u) = u == invTrueIndices (trueIndices u) | ||
203 | |||
204 | -- a Boolean stream can be seen as an index transformation function for indices 0..n | ||
205 | indexTrans :: Stream Bool -> Int -> Maybe Int | ||
206 | indexTrans s i = ((Just <$> sFilter s [0..]) ++ repeat Nothing) !! i | ||
207 | |||
208 | -- inverse of indexTrans | ||
209 | invIndexTrans :: Stream Bool -> Int -> Maybe Int | ||
210 | invIndexTrans s i = case dropWhile ((< i) . snd) $ zip [0..] $ sFilter s [0..] of | ||
211 | ((x, i'): _) | i' == i -> Just x | ||
212 | _ -> Nothing | ||
213 | |||
214 | prop_invIndexTrans u (getNonNegative -> i) = maybe True (==i) (indexTrans u i >>= invIndexTrans u) | ||
215 | |||
216 | diffDBs as = (u, filterDBUsed u <$> as) where u = mconcat as | ||
217 | |||
218 | |||
219 | ------------------------------------------------------------ used/unused de bruijn indices | ||
220 | |||
221 | -- which de bruijn indicies are used? | ||
222 | -- semantics of DBUsed is given by trueIndices | ||
223 | -- True: use index; False: skip index | ||
224 | type DBUsed = Stream Bool | ||
225 | |||
226 | -- invariant property: limes is False | ||
227 | -- finite indicies are used; lambda expressions are decorated with this | ||
228 | newtype ExpDB = ExpDB { getExpDB :: DBUsed } | ||
229 | deriving (Eq, Show) | ||
230 | |||
231 | instance Arbitrary ExpDB where | ||
232 | arbitrary = ExpDB . flip sFromList False <$> arbitrary | ||
233 | |||
234 | -- invariant property: limes is True | ||
235 | -- finite indicies are not used; good for index shifting transformations | ||
236 | newtype ShiftDB = ShiftDB { getShiftDB :: DBUsed } | ||
237 | deriving (Eq, Show) | ||
238 | |||
239 | instance Arbitrary ShiftDB where | ||
240 | arbitrary = ShiftDB . flip sFromList True <$> arbitrary | ||
241 | |||
242 | ------------------------------------------------------------ de bruijn index shifting layer | ||
243 | |||
244 | -- transformation on De-Bruijn indices | ||
245 | -- Shift s i ~ (fromJust . indexTrans s) <$> i | ||
246 | data Shift a = Shift DBUsed a | ||
247 | deriving (Eq, Functor) | ||
248 | |||
249 | instance Show a => Show (Shift a) where | ||
250 | show (Shift s a) = foldStream (:) (:":") ((\b -> if b then 'x' else '_') <$> s) ++ show a | ||
251 | |||
252 | strip (Shift _ x) = x | ||
253 | |||
254 | {- | ||
255 | instance Applicative Shift where | ||
256 | pure = Shift (Repeat False) | ||
257 | Shift uf f <*> Shift ua a = Shift (uf <> ua) (f a) | ||
258 | |||
259 | instance Monad Shift where | ||
260 | return = pure | ||
261 | Shift ux x >>= f = up ux $ f x | ||
262 | |||
263 | --prop_UExpmonadAssoc (x :: Shift ()) (apply -> f) (apply -> g) = ((x >>= f) >>= g) == (x >>= (\x' -> f x' >>= g)) | ||
264 | -} | ||
265 | |||
266 | class GetDBUsed a where | ||
267 | getDBUsed :: a -> DBUsed | ||
268 | |||
269 | instance GetDBUsed ExpDB where | ||
270 | getDBUsed = getExpDB | ||
271 | |||
272 | instance GetDBUsed (Shift a) where | ||
273 | getDBUsed (Shift u _) = u | ||
274 | |||
275 | mkShift :: GetDBUsed a => a -> Shift a | ||
276 | mkShift e = Shift (getDBUsed e) e | ||
277 | |||
278 | instance (Arbitrary a, GetDBUsed a) => Arbitrary (Shift a) where | ||
279 | arbitrary = upToShift <$> arbitrary | ||
280 | |||
281 | ---------------- | ||
282 | |||
283 | -- for testing | ||
284 | -- generate a DBUsed with a given number of used indicies | ||
285 | data Up a = Up DBUsed a | ||
286 | deriving (Show) | ||
287 | |||
288 | upToShift :: GetDBUsed a => Up a -> Shift a | ||
289 | upToShift (Up u x) = Shift (sComp u $ getDBUsed x) x | ||
290 | |||
291 | instance (Arbitrary a, GetDBUsed a) => Arbitrary (Up a) where | ||
292 | arbitrary = do | ||
293 | f <- arbitrary | ||
294 | u <- flip sFromList True . concatMap ((++ [True]) . (`replicate` False) . getNonNegative) | ||
295 | <$> replicateM (limesIndex $ getDBUsed f) arbitrary | ||
296 | return $ Up u f | ||
297 | |||
298 | class GetDBUsed a => ShiftLike a where | ||
299 | setDBUsed :: DBUsed -> a -> a | ||
300 | |||
301 | modDBUsed :: ShiftLike a => (DBUsed -> DBUsed) -> a -> a | ||
302 | modDBUsed f e = setDBUsed (f $ getDBUsed e) e | ||
303 | |||
304 | up :: ShiftLike a => DBUsed -> a -> a | ||
305 | up x = modDBUsed (sComp x) | ||
306 | |||
307 | down :: ShiftLike a => DBUsed -> a -> Maybe a | ||
308 | down a e = case filterDBUsed (not <$> a) (getDBUsed e) of | ||
309 | Repeat False -> Just $ modDBUsed (filterDBUsed a) e | ||
310 | _ -> Nothing | ||
311 | |||
312 | up_ :: ShiftLike a => Int -> Int -> a -> a | ||
313 | up_ i j = up (iterateN i (cons True) $ iterateN j (cons False) (Repeat True)) | ||
314 | |||
315 | down_ :: ShiftLike a => Int -> a -> Maybe a | ||
316 | down_ i = down (iterateN i (cons True) $ cons False (Repeat True)) | ||
317 | |||
318 | instance ShiftLike (Shift a) where | ||
319 | setDBUsed x (Shift _ a) = Shift x a | ||
320 | |||
321 | prop_upDown (Up u ((`Shift` ()) . getExpDB -> e)) | ||
322 | = down u (up u e) == Just e | ||
323 | prop_downNothing ((`Shift` ()) . getExpDB -> e) (getNonNegative -> i) | ||
324 | = if i `elem` trueIndices (getDBUsed e) then down_ i e == Nothing else isJust (down_ i e) | ||
325 | |||
326 | ------------------------------------------------------------ substitutions | ||
327 | |||
328 | type Substs a = Map Int a | ||
329 | |||
330 | substsKeys :: Substs a -> Stream Bool | ||
331 | substsKeys = invTrueIndices . Map.keys | ||
332 | |||
333 | substsStream :: Eq a => Substs a -> Stream (Maybe a) | ||
334 | substsStream = elemsUps . Map.toList | ||
335 | |||
336 | elemsUps :: Eq a => [(Int, a)] -> Stream (Maybe a) | ||
337 | elemsUps = f 0 where | ||
338 | f i [] = Repeat Nothing | ||
339 | f i ((k, a): ks) = iterateN (k - i) (cons Nothing) $ cons (Just a) $ f (k + 1) ks | ||
340 | |||
341 | streamSubsts :: Stream (Maybe a) -> Substs a | ||
342 | streamSubsts = Map.fromDistinctAscList . upsElems | ||
343 | |||
344 | upsElems :: Stream (Maybe a) -> [(Int, a)] | ||
345 | upsElems = f 0 where | ||
346 | f _ (Repeat Nothing) = [] | ||
347 | f i (Cons Nothing u) = f (i+1) u | ||
348 | f i (Cons (Just a) u) = (i, a): f (i+1) u | ||
349 | |||
350 | expandSubsts :: (Eq a, ShiftLike a) => Stream Bool -> Substs a -> Substs a | ||
351 | expandSubsts u m = streamSubsts $ (\x -> mergeStreams u x $ Repeat Nothing) $ substsStream $ up u <$> m | ||
352 | |||
353 | filterSubsts :: (Eq a, ShiftLike a) => Stream Bool -> Substs a -> Substs a | ||
354 | filterSubsts u m = streamSubsts $ filterStream (Repeat Nothing) u $ substsStream $ modDBUsed (filterDBUsed u) <$> m | ||
355 | |||
356 | ------------------------------------------------------------ let expressions (substitutions + expression) | ||
357 | |||
358 | data Let e a = Let (Substs e) a | ||
359 | deriving (Eq, Show, Functor) | ||
360 | |||
361 | instance (GetDBUsed e, GetDBUsed a) => GetDBUsed (Let e a) where | ||
362 | getDBUsed (Let m e) = getDBUsed $ ShiftLet (getDBUsed e <> mconcat (Map.elems $ getDBUsed <$> m)) m e | ||
363 | |||
364 | pattern ShiftLet :: DBUsed -> Substs a -> b -> Shift (Let a b) | ||
365 | pattern ShiftLet u m e <- (getShiftLet -> (u, m, e)) where ShiftLet u m e = Shift (filterDBUsed (not <$> substsKeys m) u) (Let m e) | ||
366 | |||
367 | getShiftLet (Shift u (Let m e)) = (mergeStreams (substsKeys m) (Repeat True) u, m, e) | ||
368 | |||
369 | -- TODO: remove Eq a | ||
370 | pattern PShiftLet :: () => (Eq a, ShiftLike a, ShiftLike b) => Substs a -> b -> Shift (Let a b) | ||
371 | pattern PShiftLet m e <- (pushShiftLet -> Let m e) where | ||
372 | PShiftLet m e = ShiftLet u (filterSubsts u m) $ modDBUsed (filterDBUsed u) e | ||
373 | where | ||
374 | u = getDBUsed e <> mconcat (Map.elems $ getDBUsed <$> m) | ||
375 | |||
376 | pushShiftLet (ShiftLet u m e) = Let (expandSubsts u m) (up u e) | ||
377 | |||
378 | mkLet :: (Eq a, ShiftLike a, ShiftLike b) => Substs a -> b -> Shift (Let a b) | ||
379 | mkLet m e = PShiftLet (Map.filterWithKey (\k _ -> streamToFun c k) m) e | ||
380 | where | ||
381 | -- determine which let expressions are used (garbage collection) | ||
382 | -- TODO: speed this up somehow | ||
383 | c = limes $ sIterate f $ getDBUsed e | ||
384 | where | ||
385 | f x = dbAnd ks $ x <> mconcat (sCatMaybes $ filterStream (Repeat Nothing) x us) | ||
386 | ks = substsKeys m | ||
387 | us = substsStream $ getDBUsed <$> m | ||
388 | |||
389 | transportIntoLet (Let m _) e = up (not <$> substsKeys m) e | ||
390 | |||
391 | ----------------------------------------------------------------- MaybeLet | ||
392 | |||
393 | data MaybeLet a b c | ||
394 | = HasLet (Let a (Shift c)) | ||
395 | | NoLet b | ||
396 | deriving (Show, Eq) | ||
397 | |||
398 | type MaybeLet' a b = MaybeLet a b b | ||
399 | |||
400 | maybeLet :: (Eq a, ShiftLike a) => Shift (Let a (Shift b)) -> Shift (MaybeLet' a b) | ||
401 | maybeLet l@(Shift u (Let m e)) | ||
402 | | Map.null m = up u $ NoLet <$> e | ||
403 | | otherwise = HasLet <$> l | ||
404 | |||
405 | joinLets :: (Eq a, ShiftLike a) => MaybeLet' a (MaybeLet' a b) -> MaybeLet' a b | ||
406 | joinLets (NoLet e) = e | ||
407 | joinLets (HasLet (Let m (Shift s' (NoLet e)))) = HasLet $ Let m $ Shift s' e | ||
408 | joinLets (HasLet (Let m (Shift s' (HasLet (Let m' e))))) | ||
409 | = HasLet $ Let (expandSubsts (not <$> substsKeys sm) m <> sm) se | ||
410 | where | ||
411 | (PShiftLet sm se) = Shift s' (Let m' e) | ||
412 | |||
413 | instance (GetDBUsed a, GetDBUsed b, GetDBUsed c) => GetDBUsed (MaybeLet a b c) where | ||
414 | getDBUsed = \case | ||
415 | NoLet a -> getDBUsed a | ||
416 | HasLet x -> getDBUsed x | ||
417 | |||
418 | -- used in testing | ||
419 | fromLet (Shift u (NoLet e)) = Shift u e | ||
420 | |||
421 | ------------------------------------------------------------ literals | ||
422 | |||
423 | data Lit | ||
424 | = LInt Int | ||
425 | | LChar Char | ||
426 | -- ... | ||
427 | deriving (Eq) | ||
428 | |||
429 | instance Show Lit where | ||
430 | show = \case | ||
431 | LInt i -> show i | ||
432 | LChar c -> show c | ||
433 | |||
434 | ------------------------------------------------------------ expressions | ||
435 | |||
436 | data Exp_ a b c d e | ||
437 | = ELit_ Lit | ||
438 | | EVar_ a -- a = () means that the variable de bruijn index is 0 (the only possible index if the exprssion is compact) | ||
439 | -- a = Int is the de bruijn index (in cases when the exprssion is not compactified) | ||
440 | | ELamD_ b -- lambda with unused argument | ||
441 | -- b is usually (Exp_ a b c d e) | ||
442 | | ELam_ c -- lambda with used argument | ||
443 | -- c usually contains a MaybeLet layer | ||
444 | | EApp_ d d -- application | ||
445 | -- d usually contains a Shift layer | ||
446 | | RHS_ e -- marks the beginning of right hand side (parts right to the equal sign) in fuction definitions | ||
447 | -- e is usually (Exp_ a b c d e) | ||
448 | -- e = Void means that this constructor cannot be used | ||
449 | deriving (Eq, Show) --, Generic) | ||
450 | |||
451 | -------------------------------------------------------- | ||
452 | |||
453 | type WithLet a = MaybeLet (Shift LHSExp) a a | ||
454 | |||
455 | -- right-hand-side expression (no RHS constructors inside) | ||
456 | newtype Exp = Exp (Exp_ () Exp (WithLet Exp) (Shift Exp) Void) | ||
457 | deriving (Eq) | ||
458 | |||
459 | pattern ELit l = Exp (ELit_ l) | ||
460 | pattern EApp a b = Exp (EApp_ a b) | ||
461 | pattern ELam i = Exp (ELam_ i) | ||
462 | pattern ELamD i = Exp (ELamD_ i) | ||
463 | pattern EVar i = Exp (EVar_ i) | ||
464 | |||
465 | pattern EInt i = ELit (LInt i) | ||
466 | |||
467 | -- left-hand-side expression (allows RHS constructor) | ||
468 | newtype LHSExp = LHSExp (Exp_ () LHSExp (WithLet LHSExp) (Shift LHSExp) Exp) | ||
469 | deriving (Eq, Show) | ||
470 | |||
471 | pattern RHS i = LHSExp (RHS_ i) | ||
472 | |||
473 | -------------------------------------------------------- | ||
474 | |||
475 | type SExp = Shift Exp | ||
476 | type LExp = WithLet Exp | ||
477 | |||
478 | -- SLExp is *the* expression type in the user API | ||
479 | type SLExp = Shift (WithLet Exp) | ||
480 | |||
481 | sFun p s xs c = parens $ \c -> s ++ foldr (\f c -> ' ': f c) c xs | ||
482 | where | ||
483 | parens x | ||
484 | | p < 10 = x c | ||
485 | | otherwise = '(': x (')': c) | ||
486 | |||
487 | instance Show Exp where | ||
488 | showsPrec p = \case | ||
489 | ELit i -> shows i | ||
490 | EApp a b -> sFun p "EApp" [showsPrec 10 a, showsPrec 10 b] | ||
491 | ELam a -> sFun p "ELam" [showsPrec 10 a] | ||
492 | ELamD a -> sFun p "ELamD" [showsPrec 10 a] | ||
493 | EVar () -> ("EVar" ++) | ||
494 | |||
495 | instance GetDBUsed Exp where | ||
496 | getDBUsed = \case | ||
497 | EApp (Shift ua a) (Shift ub b) -> ua <> ub | ||
498 | ELit{} -> mempty | ||
499 | EVar{} -> cons True mempty | ||
500 | ELamD e -> sTail $ getDBUsed e | ||
501 | ELam e -> sTail $ getDBUsed e | ||
502 | |||
503 | instance Arbitrary Exp where | ||
504 | arbitrary = (\(Shift _ (NoLet e)) -> e) . getSimpleExp <$> arbitrary | ||
505 | -- shrink = genericShrink | ||
506 | |||
507 | -- SLExp without let and shifting; for testing | ||
508 | newtype SimpleExp = SimpleExp { getSimpleExp :: SLExp } | ||
509 | deriving (Eq, Show) | ||
510 | |||
511 | instance Arbitrary SimpleExp where | ||
512 | arbitrary = fmap SimpleExp $ oneof | ||
513 | [ var . getNonNegative <$> arbitrary | ||
514 | , Int <$> arbitrary | ||
515 | , app <$> (getSimpleExp <$> arbitrary) <*> (getSimpleExp <$> arbitrary) | ||
516 | , lam <$> (getSimpleExp <$> arbitrary) | ||
517 | ] | ||
518 | |||
519 | getLit :: SLExp -> Maybe Lit | ||
520 | getLit (Shift _ (NoLet (ELit l))) = Just l | ||
521 | getLit (Shift _ (HasLet (Let _ (Shift _ (ELit l))))) = Just l | ||
522 | getLit _ = Nothing | ||
523 | |||
524 | pattern Int i <- (getLit -> Just (LInt i)) where Int = Shift mempty . NoLet . EInt | ||
525 | |||
526 | var :: Int -> SLExp | ||
527 | var i = fmap NoLet $ up_ 0 i $ mkShift $ EVar () | ||
528 | |||
529 | prop_upVar (getNonNegative -> k) (getNonNegative -> n) (getNonNegative -> i) = up_ k n (var i) == var (if k <= i then n + i else i) | ||
530 | prop_downVar (getNonNegative -> k) (getNonNegative -> i) = down_ k (var i) == case compare k i of LT -> Just (var $ i-1); EQ -> Nothing; GT -> Just (var i) | ||
531 | |||
532 | lam :: SLExp -> SLExp | ||
533 | lam (Shift u e) = Shift (sTail u) $ if sHead u then eLam e else eLamD e | ||
534 | where | ||
535 | eLam (NoLet e) = NoLet $ ELam $ NoLet e | ||
536 | -- TODO: improve this by let-floating | ||
537 | eLam x = NoLet $ ELam x | ||
538 | |||
539 | eLamD (NoLet e) = NoLet $ ELamD e | ||
540 | -- TODO: review | ||
541 | eLamD (HasLet (Let m (Shift u e))) = HasLet $ {-gc?-}Let (filterSubsts ul m) $ Shift (filterDBUsed ul u) $ ELamD e | ||
542 | where | ||
543 | ul = Cons False $ Repeat True | ||
544 | |||
545 | app :: SLExp -> SLExp -> SLExp | ||
546 | app (Shift ua (NoLet a)) (Shift ub (NoLet b)) | ||
547 | = Shift u $ NoLet $ EApp (Shift (filterDBUsed u ua) a) (Shift (filterDBUsed u ub) b) | ||
548 | where u = ua <> ub | ||
549 | app x y = f x y | ||
550 | where | ||
551 | f :: SLExp -> SLExp -> SLExp | ||
552 | f (Shift ula la) (Shift ulb (HasLet lb)) = g app ula la ulb lb | ||
553 | f (Shift ulb (HasLet lb)) (Shift ula la) = g (flip app) ula la ulb lb | ||
554 | |||
555 | g :: (SLExp -> SLExp -> SLExp) -> DBUsed -> LExp -> DBUsed -> Let (Shift LHSExp) (Shift Exp) -> SLExp | ||
556 | g app ula la ulb lb | ||
557 | = up u $ lets {-Shift u $-} | ||
558 | -- app (Shift ula' la) (Shift ulb' lb) | ||
559 | -- app (Shift ula' la) (Let mb eb) | ||
560 | mb {-HasLet $ Let mb $-} $ | ||
561 | app xa (fmap NoLet eb) | ||
562 | where | ||
563 | (u, [ula', ulb']) = diffDBs [ula, ulb] | ||
564 | lb'@(Let mb eb) = pushShiftLet $ Shift ulb' lb | ||
565 | xa = transportIntoLet lb' $ Shift ula' la | ||
566 | |||
567 | lets :: Substs (Shift LHSExp) -> SLExp -> SLExp | ||
568 | lets m e = fmap joinLets $ maybeLet $ mkLet m e | ||
569 | |||
570 | -- TODO | ||
571 | instance Arbitrary LExp where | ||
572 | arbitrary = NoLet <$> arbitrary | ||
573 | |||
574 | let1 :: Int -> SLExp -> SLExp -> SLExp | ||
575 | let1 i (Shift u (NoLet x)) = lets $ Map.singleton i $ Shift u $ RHS x | ||
576 | let1 i (Shift u (HasLet l)) = lets $ m <> Map.singleton i' (RHS <$> e) | ||
577 | where | ||
578 | (Let m e) = pushShiftLet $ Shift u l | ||
579 | (Just i') = indexTrans (not <$> substsKeys m) i | ||
580 | |||
581 | --------------------------------------------------------- | ||
582 | {- | ||
583 | newtype ExpS = ExpS (Exp_ Int ExpS (MaybeLet SExp ExpS Exp) SExp) | ||
584 | deriving (Eq, Show) | ||
585 | |||
586 | pushShift :: SExp -> ExpS | ||
587 | pushShift (Shift u e) = ExpS $ case e of | ||
588 | EApp a b -> EApp_ (up u a) (up u b) | ||
589 | ELit i -> ELit_ i | ||
590 | EVar{} -> EVar_ $ fromJust $ indexTrans u 0 | ||
591 | ELamD e -> ELamD_ $ pushShift $ Shift (cons False u) e | ||
592 | ELam (NoLet e) -> ELam_ $ NoLet $ pushShift $ Shift (cons True u) e | ||
593 | LHS a b -> LHS_ a (up u <$> b) -- ??? $ SData (pushShift $ Shift u c) | ||
594 | -- Delta x -> Delta_ $ SData x | ||
595 | |||
596 | prop_var (getNonNegative -> i) = case pushShift (fromLet $ var i) of | ||
597 | ExpS (EVar_ i') -> i == i' | ||
598 | _ -> False | ||
599 | |||
600 | prop_app (getSimpleExp -> a) (getSimpleExp -> b) = case pushShift $ fromLet $ app a b of | ||
601 | ExpS (EApp_ a' b') -> (a', b') == (fromLet a, fromLet b) | ||
602 | _ -> False | ||
603 | |||
604 | --prop_lam (getNonNegative -> i) = elimShift undefined undefined undefined (==i) (var i) | ||
605 | |||
606 | --prop_pushShift (Shift u e) = | ||
607 | |||
608 | --------------------------------------------------------- | ||
609 | |||
610 | newtype ExpL = ExpL (Exp_ Int SLExp SLExp SLExp) | ||
611 | deriving (Eq, Show) | ||
612 | {- | ||
613 | pushLet :: LExp -> ExpL | ||
614 | pushLet (NoLet e) = ExpL $ case e of | ||
615 | EInt i -> EInt_ i | ||
616 | EApp a b -> EApp_ (NoLet <$> a) (NoLet <$> b) | ||
617 | EVar{} -> EVar_ 0 | ||
618 | -- ELam a -> ELam_ $ mkShift a | ||
619 | ELamD a -> ELamD_ $ NoLet <$> mkShift a | ||
620 | pushLet (HasLet (Let m e)) = ExpL $ case pushShift e of | ||
621 | ExpS e' -> case e' of | ||
622 | EApp_ a b -> EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) | ||
623 | EInt_ i -> EInt_ i | ||
624 | EVar_ i -> EVar_ i | ||
625 | -} | ||
626 | pushLet' :: SLExp -> ExpL | ||
627 | pushLet' (Shift u l) = case l of | ||
628 | NoLet e -> {-case pushShift (Shift u e) of | ||
629 | ExpS e -> -} ExpL $ case e of | ||
630 | ELit i -> ELit_ i | ||
631 | EApp a b -> EApp_ (NoLet <$> up u a) (NoLet <$> up u b) | ||
632 | EVar () -> EVar_ $ fromJust $ indexTrans u 0 | ||
633 | ELam a -> ELam_ $ Shift (cons True u) a | ||
634 | -- ELamD_ a -> ELamD_ $ NoLet a | ||
635 | LHS a b -> LHS_ a ((fmap NoLet . up u) <$> b) | ||
636 | HasLet l -> case Shift u l of | ||
637 | PShiftLet m e -> case pushShift e of | ||
638 | ExpS e' -> case e' of | ||
639 | EApp_ a b -> ExpL $ EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b)) | ||
640 | ELit_ i -> ExpL $ ELit_ i | ||
641 | EVar_ i -> case Map.lookup i m of | ||
642 | Nothing -> ExpL $ EVar_ i | ||
643 | Just x -> pushLet' $ lets m $ NoLet <$> x | ||
644 | LHS_ a b -> error "efun" | ||
645 | -- Delta_ f -> ExpL $ Delta_ f | ||
646 | |||
647 | --------------------------------------------------------- | ||
648 | |||
649 | hnf :: SLExp -> ExpL | ||
650 | hnf e = case pushLet' e of | ||
651 | (ExpL (LHS_ "add" [_, _])) -> error "ok" | ||
652 | x@(ExpL (EApp_ a b)) -> case hnf a of | ||
653 | ExpL (ELam_ a) -> hnf $ let1 0 b a | ||
654 | ExpL (LHS_ n acc) -> hnf $ LHS n (_ b: acc) | ||
655 | _ -> x | ||
656 | x -> x | ||
657 | |||
658 | ----------------------------------------------------------------------------------- | ||
659 | |||
660 | idE :: SLExp | ||
661 | idE = lam $ var 0 | ||
662 | |||
663 | add :: SLExp | ||
664 | add = NoLet <$> mkShift (LHS "add" []) -- $ ELam $ NoLet $ ELam $ NoLet $ Delta f) | ||
665 | where | ||
666 | f [Int i, Int j] = Int $ i + j | ||
667 | |||
668 | example1 = app (idE) (Int 10) | ||
669 | |||
670 | example2 = app (app add (Int 10)) (Int 5) | ||
671 | |||
672 | |||
673 | -- = fun name args $ \x -> \y -> rhs e | ||
674 | |||
675 | |||
676 | ----------------------------------------------------------------- run all tests | ||
677 | -} | ||
678 | return [] | ||
679 | runTests = $quickCheckAll | ||
680 | |||
681 | {- | ||
682 | TODO | ||
683 | |||
684 | - primes example running | ||
685 | - speed up eliminators with caching | ||
686 | - write performance tests | ||
687 | - speed up Boolean streams with compression | ||
688 | - check that all operations is available and efficient | ||
689 | - up, down | ||
690 | - subst | ||
691 | - constructions | ||
692 | - lam, pi, app, var, lit, ... | ||
693 | - eliminations | ||
694 | - intergrate into the compiler | ||
695 | -} | ||
696 | |||