diff options
Diffstat (limited to 'prototypes')
-rw-r--r-- | prototypes/FreeVars.hs | 270 | ||||
-rw-r--r-- | prototypes/Inspector.hs | 44 | ||||
-rw-r--r-- | prototypes/LamMachine.hs | 432 |
3 files changed, 497 insertions, 249 deletions
diff --git a/prototypes/FreeVars.hs b/prototypes/FreeVars.hs index 4ee5eb35..eefea309 100644 --- a/prototypes/FreeVars.hs +++ b/prototypes/FreeVars.hs | |||
@@ -8,6 +8,11 @@ | |||
8 | {-# LANGUAGE FlexibleInstances #-} | 8 | {-# LANGUAGE FlexibleInstances #-} |
9 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | 9 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} |
10 | {-# LANGUAGE BangPatterns #-} | 10 | {-# LANGUAGE BangPatterns #-} |
11 | {-# LANGUAGE TypeFamilies #-} | ||
12 | {-# LANGUAGE DeriveFoldable #-} | ||
13 | {-# LANGUAGE DeriveTraversable #-} | ||
14 | {-# LANGUAGE DeriveFunctor #-} | ||
15 | {-# language TemplateHaskell #-} -- for testing | ||
11 | 16 | ||
12 | module FreeVars where | 17 | module FreeVars where |
13 | 18 | ||
@@ -17,11 +22,25 @@ import Data.Int | |||
17 | import Data.Monoid | 22 | import Data.Monoid |
18 | import Data.Maybe | 23 | import Data.Maybe |
19 | import Data.Bits | 24 | import Data.Bits |
25 | import Data.Foldable | ||
20 | import Control.Arrow | 26 | import Control.Arrow |
27 | import Control.Monad.State | ||
28 | import Control.Monad.Identity | ||
21 | import Control.Category hiding ((.), id) | 29 | import Control.Category hiding ((.), id) |
30 | import Test.QuickCheck hiding ((.&.)) | ||
31 | import Test.QuickCheck.Property.Monoid hiding ((.&&.), (.||.)) | ||
32 | import Test.QuickCheck.Property.Common.Internal (Equal(..)) | ||
22 | --import Debug.Trace | 33 | --import Debug.Trace |
23 | 34 | ||
24 | import LambdaCube.Compiler.Pretty | 35 | import LambdaCube.Compiler.Pretty hiding (expand) |
36 | |||
37 | instance (Eq a, Show a) => Testable (Equal a) where | ||
38 | property (Equal a b) = a === b | ||
39 | property (AndE a b) = a .&&. b | ||
40 | property (OrE a b) = a .||. b | ||
41 | property (NotE a) = expectFailure a | ||
42 | |||
43 | ---------------------------------------------------------------------------------- | ||
25 | 44 | ||
26 | newtype Nat = Nat_ Int --Word32 | 45 | newtype Nat = Nat_ Int --Word32 |
27 | deriving (Eq, Ord, Enum) | 46 | deriving (Eq, Ord, Enum) |
@@ -38,8 +57,73 @@ instance Num Nat where | |||
38 | abs _ = error "abs @Nat" | 57 | abs _ = error "abs @Nat" |
39 | signum _ = error "signum @Nat" | 58 | signum _ = error "signum @Nat" |
40 | 59 | ||
41 | instance PShow Nat where | 60 | instance PShow Nat where pShow (Nat i) = pShow i |
42 | pShow (Nat i) = pShow i | 61 | instance Show Nat where show = ppShow |
62 | |||
63 | ---------------------------------------------------------------------------------- | ||
64 | |||
65 | data D1 a = D1 a | ||
66 | deriving (Functor, Foldable, Traversable, Eq, Ord, Show) | ||
67 | |||
68 | data D2 a = D2 a a | ||
69 | deriving (Functor, Foldable, Traversable, Eq, Ord, Show) | ||
70 | |||
71 | data D3 a = D3 a a a | ||
72 | deriving (Functor, Foldable, Traversable, Eq, Ord, Show) | ||
73 | |||
74 | instance Arbitrary a => Arbitrary (D1 a) where arbitrary = D1 <$> arbitrary | ||
75 | instance Arbitrary a => Arbitrary (D2 a) where arbitrary = D2 <$> arbitrary <*> arbitrary | ||
76 | instance Arbitrary a => Arbitrary (D3 a) where arbitrary = D3 <$> arbitrary <*> arbitrary <*> arbitrary | ||
77 | |||
78 | ---------------------------------------------------------------------------------- | ||
79 | |||
80 | class Monoid a => Expandable a where | ||
81 | |||
82 | expandT :: Traversable t => a -> t a -> t a | ||
83 | expandT = fmap . expand | ||
84 | |||
85 | expand :: a -> a -> a | ||
86 | expand u = runIdentity . expandT u . Identity | ||
87 | |||
88 | primContractT :: Traversable t => a -> t a -> t a | ||
89 | primContractT = fmap . primContract | ||
90 | |||
91 | primContract :: a -> a -> a | ||
92 | primContract u = runIdentity . primContractT u . Identity | ||
93 | |||
94 | contract :: a -> a -> a | ||
95 | contract a b = primContract (a <> b) a | ||
96 | |||
97 | selfContract :: a -> a | ||
98 | selfContract a = primContract a a | ||
99 | |||
100 | diffT :: (Traversable t, Expandable a) => t a -> (a, t a) | ||
101 | diffT u = (s, primContractT s u) | ||
102 | where | ||
103 | s = fold u | ||
104 | |||
105 | diffTest u = u == uncurry expandT (diffT u) | ||
106 | |||
107 | assocTestL (D3 a b c) = (abc, D3 a'' b'' c'') == diffT (D3 a b c) | ||
108 | where | ||
109 | (ab, D2 a' b') = diffT $ D2 a b | ||
110 | (abc, D2 ab' c'') = diffT $ D2 ab c | ||
111 | D2 a'' b'' = expandT ab' $ D2 a' b' | ||
112 | |||
113 | assocTestR (D3 a b c) = (abc, D3 a'' b'' c'') == diffT (D3 a b c) | ||
114 | where | ||
115 | (bc, D2 b' c') = diffT $ D2 b c | ||
116 | (abc, D2 a'' bc') = diffT $ D2 a bc | ||
117 | D2 b'' c'' = expandT bc' $ D2 b' c' | ||
118 | |||
119 | class StreamLike a where | ||
120 | type StreamElem a | ||
121 | |||
122 | sDrop :: Nat -> a -> a | ||
123 | |||
124 | sIndex :: a -> Nat -> StreamElem a | ||
125 | |||
126 | ---------------------------------------------------------------------------------- | ||
43 | 127 | ||
44 | data FV | 128 | data FV |
45 | -- = FV !Nat !Nat !FV | 129 | -- = FV !Nat !Nat !FV |
@@ -54,8 +138,11 @@ pattern FV i j x <- FV_ (splitInt -> (i, j)) x | |||
54 | splitInt x = (Nat $ x `shiftR` 32, Nat $ x .&. 0xffffffff) | 138 | splitInt x = (Nat $ x `shiftR` 32, Nat $ x .&. 0xffffffff) |
55 | 139 | ||
56 | instance PShow FV where | 140 | instance PShow FV where |
57 | pShow FE = "0" | 141 | pShow = text . f where |
58 | pShow (FV i j x) = pShow i <> "|" <> pShow j <> "|" <> pShow x | 142 | f FE = "|" |
143 | f (FV (Nat i) (Nat j) x) = replicate i '_' ++ replicate j '.' ++ f x | ||
144 | |||
145 | instance Show FV where show = ppShow | ||
59 | 146 | ||
60 | {- | 147 | {- |
61 | newtype FV = FV_ Integer | 148 | newtype FV = FV_ Integer |
@@ -78,34 +165,18 @@ fv a 0 (FV b c xs) = FV (a+b) c xs | |||
78 | fv a b (FV 0 c xs) = FV a (b+c) xs | 165 | fv a b (FV 0 c xs) = FV a (b+c) xs |
79 | fv a b xs = FV a b xs | 166 | fv a b xs = FV a b xs |
80 | 167 | ||
81 | pattern VarFV i <- FV i _ _ | 168 | testNormalFV = f where |
82 | where VarFV i = FV i 1 FE | 169 | f FE = True |
83 | 170 | f (FV _ a xs) = a > 0 && g xs | |
84 | del1 :: FV -> FV | 171 | g FE = True |
85 | del1 FE = FE | 172 | g (FV a b xs) = a > 0 && b > 0 && g xs |
86 | del1 (FV 0 n us) = fv 0 (n-1) us | ||
87 | del1 (FV n i us) = FV (n-1) i us | ||
88 | |||
89 | compact :: FV -> FV | ||
90 | compact xs@(FV 0 _ _) = delUnused xs | ||
91 | compact xs = fv 1 0 $ delUnused xs | ||
92 | |||
93 | usedFVs :: FV -> [Nat] | ||
94 | usedFVs = f 0 | ||
95 | where | ||
96 | f _ FE = [] | ||
97 | f s (FV i a xs) = [s+i..(s+i+a)-1] ++ f (s+i+a) xs | ||
98 | 173 | ||
99 | usedFV :: Nat -> FV -> Bool | 174 | instance Arbitrary FV where |
100 | usedFV i FE = False | 175 | arbitrary = fromBools <$> arbitrary |
101 | usedFV i (FV n l us) = i >= n && (i < l || usedFV (i - l - n) us) | ||
102 | 176 | ||
103 | downFV :: Nat -> FV -> Maybe FV | 177 | fromBools [] = FE |
104 | downFV i FE = Just FE | 178 | fromBools (True: bs) = fv 0 1 $ fromBools bs |
105 | downFV i (FV n j us) | 179 | fromBools (False: bs) = fv 1 0 $ fromBools bs |
106 | | i < n = Just $ FV (n - 1) j us | ||
107 | | i - n < j = Nothing | ||
108 | | otherwise = fv n j <$> downFV (i - n - j) us | ||
109 | 180 | ||
110 | instance Monoid FV where | 181 | instance Monoid FV where |
111 | mempty = FE | 182 | mempty = FE |
@@ -120,31 +191,81 @@ instance Monoid FV where | |||
120 | where | 191 | where |
121 | c = min a a' | 192 | c = min a a' |
122 | 193 | ||
123 | delFV :: FV -> FV -> FV | 194 | prop_monoid_FV = prop_Monoid (T :: T FV) |
124 | delFV FE x = FE | 195 | prop_mappend_normal_FV (a :: FV) b = testNormalFV (a <> b) |
125 | delFV (FV a b us) (FV a' b' us') | 196 | |
126 | | a' + b' <= a = fv b' 0 $ delFV (FV (a - (a' + b')) b us) us' | 197 | instance Expandable FV where |
127 | | otherwise = fv (a - a') b $ delFV us (FV 0 ((a' + b') - (a + b)) us') | 198 | expand _ FE = FE |
199 | expand FE _ = FE | ||
200 | expand (FV a b xs) (FV c d ys) | ||
201 | | c + d <= b = fv (a + c) d $ expand (FV 0 (b - (c + d)) xs) ys | ||
202 | | c <= b = fv (a + c) (b - c) $ expand xs (FV 0 (d - (b - c)) ys) | ||
203 | | otherwise = fv (a + b) 0 $ expand xs (FV (c - b) d ys) | ||
128 | 204 | ||
129 | -- delUnused x = delFV x x | 205 | primContract x FE = FE |
130 | delUnused :: FV -> FV | 206 | primContract (FV a' b' us') (FV a b us) |
131 | delUnused xs = fv 0 (altersum xs) FE | 207 | | a' + b' <= a = fv b' 0 $ primContract us' (FV (a - (a' + b')) b us) |
208 | | otherwise = fv (a - a') b $ primContract (FV 0 ((a' + b') - (a + b)) us') us | ||
209 | |||
210 | selfContract xs = fv 0 (altersum xs) FE | ||
211 | where | ||
212 | altersum FE = 0 | ||
213 | altersum (FV _ a cs) = a + altersum cs | ||
214 | |||
215 | prop_expand_normal_FV (a :: FV) b = testNormalFV (expand a b) | ||
216 | prop_contract_normal_FV (a :: FV) b = testNormalFV (contract a b) | ||
217 | |||
218 | prop_diffTestFV1 = diffTest :: D1 FV -> Bool | ||
219 | prop_diffTestFV2 = diffTest :: D2 FV -> Bool | ||
220 | prop_diffTestFV3 = diffTest :: D3 FV -> Bool | ||
221 | |||
222 | prop_assocTestL_FV = assocTestL :: D3 FV -> Bool | ||
223 | prop_assocTestR_FV = assocTestR :: D3 FV -> Bool | ||
224 | |||
225 | instance StreamLike FV where | ||
226 | type StreamElem FV = Bool | ||
227 | |||
228 | sIndex FE i = False | ||
229 | sIndex (FV n l us) i = i >= n && (i < l || sIndex us (i - l - n)) | ||
230 | |||
231 | sDrop _ FE = FE | ||
232 | sDrop n (FV i j us) | ||
233 | | i + j <= n = sDrop (n - (i + j)) us | ||
234 | | n <= i = FV (i - n) j us | ||
235 | | otherwise = FV 0 (j - (n - i)) us | ||
236 | |||
237 | ------------------------------------------------ | ||
238 | |||
239 | onTail :: (FV -> FV) -> Nat -> FV -> FV | ||
240 | onTail f 0 u = f u | ||
241 | onTail f n FE = fv n 0 $ f FE | ||
242 | onTail f n (FV i j us) | ||
243 | | i + j <= n = fv i j $ onTail f (n - (i + j)) us | ||
244 | | n <= i = fv n 0 $ f $ FV (i - n) j us | ||
245 | | otherwise = fv i (n - i) $ f $ FV 0 (j - (n - i)) us | ||
246 | |||
247 | -- usedFVs s = filter (sIndex s) [0..] | ||
248 | -- TODO: remove | ||
249 | usedFVs :: FV -> [Nat] | ||
250 | usedFVs = f 0 | ||
132 | where | 251 | where |
133 | altersum FE = 0 | 252 | f _ FE = [] |
134 | altersum (FV _ a cs) = a + altersum cs | 253 | f s (FV i a xs) = [s+i..(s+i+a)-1] ++ f (s+i+a) xs |
135 | 254 | ||
136 | compFV :: FV -> FV -> FV | 255 | -- downFV i u = if sIndex u i then Just $ fv 0 i (FO 1) `contract` u else Nothing |
137 | compFV _ FE = FE | 256 | downFV :: Nat -> FV -> Maybe FV |
138 | compFV FE x = x | 257 | downFV i FE = Just FE |
139 | compFV (FV a b xs) (FV c d ys) | 258 | downFV i (FV n j us) |
140 | | c + d <= b = fv (a + c) d $ compFV (FV 0 (b - (c + d)) xs) ys | 259 | | i < n = Just $ FV (n - 1) j us |
141 | | c <= b = fv (a + c) (b - c) $ compFV xs (FV 0 (d - (b - c)) ys) | 260 | | i - n < j = Nothing |
142 | | otherwise = fv (a + b) 0 $ compFV xs (FV (c - b) d ys) | 261 | | otherwise = fv n j <$> downFV (i - n - j) us |
143 | 262 | ||
144 | incFV :: FV -> FV | 263 | -- TODO |
145 | incFV = FV{-ok-} 0 1 | 264 | fO i = FV i 10000 FE |
146 | 265 | ||
147 | --upFV l n = compFV (fv 0 l $ fv n 0{-buggy-} FE) | 266 | mkUp l n = fv 0 l $ fO n |
267 | |||
268 | --upFV l n = expand (fv 0 l $ FO n) | ||
148 | upFV :: Nat -> Nat -> FV -> FV | 269 | upFV :: Nat -> Nat -> FV -> FV |
149 | upFV l n FE = FE | 270 | upFV l n FE = FE |
150 | upFV l n (FV n' l' us) | 271 | upFV l n (FV n' l' us) |
@@ -152,5 +273,52 @@ upFV l n (FV n' l' us) | |||
152 | | l' <= l - n' = FV n' l' $ upFV (l - n' - l') n us | 273 | | l' <= l - n' = FV n' l' $ upFV (l - n' - l') n us |
153 | | otherwise = FV n' (l - n') $ FV n (l' - (l - n')) us | 274 | | otherwise = FV n' (l - n') $ FV n (l' - (l - n')) us |
154 | 275 | ||
276 | pattern VarFV i <- FV i _ _ | ||
277 | where VarFV i = FV i 1 FE | ||
278 | |||
279 | incFV :: FV -> FV | ||
280 | incFV = FV{-ok-} 0 1 | ||
281 | |||
282 | -- compact u = r where (_, D2 r _) = cDiffT $ D2 (SFV 0 u) (SFV 1 FE) | ||
283 | compact :: FV -> FV | ||
284 | compact xs@(FV 0 _ _) = selfContract xs | ||
285 | compact xs = fv 1 0 $ selfContract xs | ||
286 | |||
287 | ---------------------------------------------------------------------------------- skewed free vars set | ||
288 | |||
289 | -- skewed FV | ||
290 | data SFV = SFV !Nat !FV | ||
291 | deriving (Eq, Show) | ||
292 | |||
293 | padSFV (SFV n x) = SFV n $ fv 0 n $ sDrop n x | ||
294 | |||
295 | fromSFV (SFV n u) = sDrop n u | ||
296 | |||
297 | instance PShow SFV where pShow (SFV n x) = pShow n <> pShow x | ||
298 | |||
299 | instance Arbitrary SFV where | ||
300 | arbitrary = SFV <$> (Nat . getNonNegative <$> arbitrary) <*> arbitrary | ||
301 | |||
302 | instance Monoid SFV where | ||
303 | mempty = SFV 0 mempty | ||
304 | |||
305 | SFV m b `mappend` SFV n a = SFV (n + m) $ b <> fv m 0 a | ||
306 | |||
307 | prop_monoid_SFV = prop_Monoid (T :: T SFV) | ||
308 | |||
309 | instance Expandable SFV where | ||
310 | |||
311 | expandT (padSFV -> SFV n b) = flip evalState b . traverse (\(SFV n a) -> state $ \u -> (SFV n $ u `expand` a, sDrop n u)) | ||
312 | |||
313 | primContractT (padSFV -> SFV _ b) = flip evalState b . traverse (\(SFV n a) -> state $ \u -> (SFV n $ u `primContract` a, sDrop n u)) | ||
314 | |||
315 | prop_diffTest1_SFV = diffTest :: D1 SFV -> Bool | ||
316 | prop_diffTest2_SFV = diffTest :: D2 SFV -> Bool | ||
317 | prop_diffTest3_SFV = diffTest :: D3 SFV -> Bool | ||
318 | |||
319 | prop_assocTestL_SFV = assocTestL :: D3 SFV -> Bool | ||
320 | prop_assocTestR_SFV = assocTestR :: D3 SFV -> Bool | ||
155 | 321 | ||
322 | return [] | ||
323 | main = $quickCheckAll | ||
156 | 324 | ||
diff --git a/prototypes/Inspector.hs b/prototypes/Inspector.hs index b6be9562..af29c0cc 100644 --- a/prototypes/Inspector.hs +++ b/prototypes/Inspector.hs | |||
@@ -47,9 +47,13 @@ stepList (initSt -> st) = ("Start", st): f (stepTree st) | |||
47 | 47 | ||
48 | 48 | ||
49 | data Command = UpArrow | DownArrow | LeftArrow | RightArrow | 49 | data Command = UpArrow | DownArrow | LeftArrow | RightArrow |
50 | | IntArg Int | ProgramChange | 50 | | IntArg Int | ProgramChange | ViewChange |
51 | deriving (Eq, Show) | 51 | deriving (Eq, Show) |
52 | 52 | ||
53 | type MSt' = (String, MSt) | ||
54 | |||
55 | data St = St Bool ([MSt'], [MSt']) | ||
56 | |||
53 | getCommand pr msg = do | 57 | getCommand pr msg = do |
54 | putStr $ (if pr then "\n" else "\CR") ++ "-------------- " ++ msg ++ " --------> " | 58 | putStr $ (if pr then "\n" else "\CR") ++ "-------------- " ++ msg ++ " --------> " |
55 | getChar >>= \case | 59 | getChar >>= \case |
@@ -63,6 +67,7 @@ getCommand pr msg = do | |||
63 | c -> clear c | 67 | c -> clear c |
64 | d | '0' <= d && d <= '9' -> readI [d] | 68 | d | '0' <= d && d <= '9' -> readI [d] |
65 | 'n' -> ret ProgramChange | 69 | 'n' -> ret ProgramChange |
70 | 'v' -> ret ViewChange | ||
66 | c -> clear c | 71 | c -> clear c |
67 | where | 72 | where |
68 | ret a = {-putStr (" -- " ++ show a) >> -} return a | 73 | ret a = {-putStr (" -- " ++ show a) >> -} return a |
@@ -82,23 +87,28 @@ main = do | |||
82 | putStrLn $ ppShow $ hnf $ case b of | 87 | putStrLn $ ppShow $ hnf $ case b of |
83 | "lazy" -> t' $ read n | 88 | "lazy" -> t' $ read n |
84 | "seq" -> t'' $ read n | 89 | "seq" -> t'' $ read n |
85 | _ -> cycle True mempty | 90 | _ -> cycle_ True $ St False mempty |
91 | |||
92 | main' x = cycle' $ St False ([], stepList x) | ||
93 | |||
94 | cycle' st@(St vi (h, (_, x): _)) = do | ||
95 | putStr $ "\n" ++ show (viewShow vi x) | ||
96 | cycle_ True st | ||
97 | cycle' st = cycle_ True st | ||
98 | |||
99 | cycle_ (pr :: Bool) s@(St vi st) = do | ||
100 | n <- getCommand pr $ message st | ||
101 | case (n, st) of | ||
102 | (DownArrow, st@(_, _:_:_)) -> cycle' $ f s goLeft | ||
103 | (UpArrow, st@(_:_, _)) -> cycle' $ f s goRight | ||
104 | (LeftArrow, st@(_, _:_:_)) -> cycle' $ f s ((!! 100) . iterate goLeft) | ||
105 | (RightArrow, st@(_:_, _)) -> cycle' $ f s ((!! 100) . iterate goRight) | ||
106 | (IntArg n, _) -> cycle' $ f s $ const ([], stepList $ t' n) | ||
107 | (ProgramChange, _) -> cycle' $ f s $ const ([], stepList $ t'' 100) | ||
108 | (ViewChange, _) -> cycle' $ St (not vi) st | ||
109 | _ -> cycle_ False s | ||
86 | where | 110 | where |
87 | cycle (pr :: Bool) st = do | 111 | f (St a b) g = St a (g b) |
88 | n <- getCommand pr $ message st | ||
89 | case (n, st) of | ||
90 | (DownArrow, st@(_, _:_:_)) -> cycle' $ goLeft st | ||
91 | (UpArrow, st@(_:_, _)) -> cycle' $ goRight st | ||
92 | (LeftArrow, st@(_, _:_:_)) -> cycle' $ iterate goLeft st !! 100 | ||
93 | (RightArrow, st@(_:_, _)) -> cycle' $ iterate goRight st !! 100 | ||
94 | (IntArg n, _) -> cycle' ([], stepList $ t' n) | ||
95 | (ProgramChange, _) -> cycle' ([], stepList $ t'' 100) | ||
96 | _ -> cycle False st | ||
97 | |||
98 | cycle' st@(h, (_, x): _) = do | ||
99 | putStr $ "\n" ++ ppShow x | ||
100 | cycle True st | ||
101 | cycle' st = cycle True st | ||
102 | 112 | ||
103 | goLeft (xs, y: ys) = (y: xs, ys) | 113 | goLeft (xs, y: ys) = (y: xs, ys) |
104 | goLeft xs = xs | 114 | goLeft xs = xs |
diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs index 7cf997a5..efb0ffda 100644 --- a/prototypes/LamMachine.hs +++ b/prototypes/LamMachine.hs | |||
@@ -7,6 +7,7 @@ | |||
7 | {-# LANGUAGE TypeSynonymInstances #-} | 7 | {-# LANGUAGE TypeSynonymInstances #-} |
8 | {-# LANGUAGE FlexibleInstances #-} | 8 | {-# LANGUAGE FlexibleInstances #-} |
9 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | 9 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} |
10 | {-# LANGUAGE NoMonomorphismRestriction #-} | ||
10 | 11 | ||
11 | module LamMachine where | 12 | module LamMachine where |
12 | 13 | ||
@@ -20,7 +21,7 @@ import Control.Category hiding ((.), id) | |||
20 | import Control.Monad | 21 | import Control.Monad |
21 | import Debug.Trace | 22 | import Debug.Trace |
22 | 23 | ||
23 | import LambdaCube.Compiler.Pretty | 24 | import LambdaCube.Compiler.Pretty hiding (expand) |
24 | 25 | ||
25 | import FreeVars | 26 | import FreeVars |
26 | 27 | ||
@@ -31,12 +32,12 @@ data Exp_ | |||
31 | | Int_ !Int -- ~ constructor with 0 args | 32 | | Int_ !Int -- ~ constructor with 0 args |
32 | | Lam_ !Exp | 33 | | Lam_ !Exp |
33 | | Op1_ !Op1 !Exp | 34 | | Op1_ !Op1 !Exp |
34 | | Con_ String !Int [Exp] | 35 | | Con_ String{-for pretty print-} !Int [Exp] |
35 | | Case_ [String]{-for pretty print-} !Exp ![Exp] -- --> simplify | 36 | | Case_ [String]{-for pretty print-} !Exp ![Exp] -- TODO: simplify? |
36 | | Op2_ !Op2 !Exp !Exp | 37 | | Op2_ !Op2 !Exp !Exp |
37 | deriving Eq | 38 | deriving (Eq, Show) |
38 | 39 | ||
39 | data Op1 = HNF_ !Int | YOp | Round | 40 | data Op1 = HNF_ | YOp | Round |
40 | deriving (Eq, Show) | 41 | deriving (Eq, Show) |
41 | 42 | ||
42 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt | 43 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt |
@@ -44,52 +45,157 @@ data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt | |||
44 | 45 | ||
45 | -- cached and compressed free variables set | 46 | -- cached and compressed free variables set |
46 | data Exp = Exp_ !FV !Exp_ | 47 | data Exp = Exp_ !FV !Exp_ |
47 | deriving Eq | 48 | deriving (Eq, Show) |
49 | |||
50 | ------------------- | ||
51 | |||
52 | data EnvPiece | ||
53 | = ELet Exp | ||
54 | | EDLet1 DExp | ||
55 | | ECase_ FV [String] [Exp] | ||
56 | | EOp2_1 Op2 Exp | ||
57 | | EOp2_2 Op2 Exp | ||
58 | deriving (Eq, Show) | ||
59 | |||
60 | pattern ECase op e <- ECase_ u op (map (upp u) -> e) | ||
61 | where ECase op b = ECase_ u op bz where (u, bz) = deltas b | ||
62 | |||
63 | pattern EnvPiece sfv p <- (getEnvPiece -> (sfv, p)) | ||
64 | where EnvPiece sfv@(SFV n u') = \case | ||
65 | EOp2_1 op e -> EOp2_1 op (uppS sfv e) | ||
66 | EOp2_2 op e -> EOp2_2 op (uppS sfv e) | ||
67 | ECase_ u s es -> ECase_ (expand u' u) s es | ||
68 | ELet (Exp_ u e) -> ELet (Exp_ (sDrop 1 u' `expand` u) e) | ||
69 | EDLet1 z -> EDLet1 $ uppDE u' 1 z | ||
70 | |||
71 | getEnvPiece = \case | ||
72 | EOp2_1 op (Exp_ u e) -> (SFV 0 u, EOp2_1 op (Exp_ (selfContract u) e)) | ||
73 | EOp2_2 op (Exp_ u e) -> (SFV 0 u, EOp2_2 op (Exp_ (selfContract u) e)) | ||
74 | ECase_ u s es -> (SFV 0 u, ECase_ (selfContract u) s es) | ||
75 | ELet (Exp_ u e) -> (SFV 1 $ fv 1 0 u, ELet $ Exp_ (selfContract u) e) | ||
76 | EDLet1 DExpNil -> (mempty, EDLet1 DExpNil) | ||
77 | EDLet1 (DExpCons_ u x y) -> (SFV 0 $ sDrop 1 u, EDLet1 $ DExpCons_ (onTail selfContract 1 u) x y) | ||
78 | |||
79 | uppS (SFV _ x) (Exp_ u a) = Exp_ (expand x u) a | ||
80 | |||
81 | data DExp | ||
82 | = DExpNil -- variable | ||
83 | | DExpCons_ FV EnvPiece DExp | ||
84 | deriving (Eq, Show) | ||
85 | |||
86 | pattern DExpCons :: EnvPiece -> DExp -> DExp | ||
87 | pattern DExpCons a b <- (getDExpCons -> (a, b)) | ||
88 | where DExpCons (EnvPiece ux a) DExpNil = DExpCons_ (fromSFV s) (EnvPiece ux' a) DExpNil | ||
89 | where (s, D1 ux') = diffT $ D1 ux | ||
90 | DExpCons (ELet a) (dDown 0 -> Just d) = d | ||
91 | -- DExpCons (EDLet1 (dDown 0 -> Just a)) x = error "? ?" | ||
92 | DExpCons (EnvPiece ux a) (DExpCons_ u x y) = DExpCons_ (fromSFV s) (EnvPiece ux' a) (DExpCons_ u' x y) | ||
93 | where (s, D2 (SFV 0 u') ux') = diffT $ D2 (SFV 0 u) ux | ||
94 | |||
95 | getDExpCons (DExpCons_ u x@(EnvPiece (SFV n _) _) b) = (uppEP u x, uppDE u n b) | ||
96 | |||
97 | uppEP u (EnvPiece (SFV n x) y) = EnvPiece (SFV n $ onTail (u `expand`) n x) y -- ??? | ||
98 | |||
99 | upP i j = uppEP $ mkUp i j | ||
100 | |||
101 | incFV' (SFV n u) = SFV (n + 1) $ incFV u | ||
102 | |||
103 | --uppDE :: FV -> DExp -> DExp | ||
104 | uppDE a _ DExpNil = DExpNil | ||
105 | uppDE a n (DExpCons_ u x y) = DExpCons_ (onTail (expand a) n u) x y | ||
106 | |||
107 | data DEnv | ||
108 | = DEnvNil | ||
109 | | DEnvCons EnvPiece DEnv | ||
110 | deriving (Eq, Show) | ||
48 | 111 | ||
49 | -- state of the machine | 112 | -- state of the machine |
50 | data MSt = MSt Exp ![Env] | 113 | data MSt = MSt DEnv Exp |
51 | deriving Eq | 114 | deriving (Eq, Show) |
52 | 115 | ||
53 | data Env | 116 | infixr 4 `DEnvCons`, `DExpCons` |
54 | = ELet Exp | 117 | |
55 | | ELet1 Exp | 118 | mSt es e = MSt ({-gc u-} es) e |
56 | | EApp1 !Int Exp | 119 | |
57 | | ECase !Int [String] [Exp] | 120 | gc :: FV -> DEnv -> DEnv |
58 | | EOp2_1 !Int Op2 Exp | 121 | gc _ DEnvNil = DEnvNil |
59 | | EOp2_2 !Int Op2 Exp | 122 | gc u (e@(ELet x) `DEnvCons` es) |
60 | deriving Eq | 123 | | sIndex u 0 = e `DEnvCons` gc (sDrop 1 u) es |
124 | | otherwise = ELet (Int 111) `DEnvCons` gc (sDrop 1 u) es | ||
125 | --gc u (EDLet1 `DEnvCons` es) = e `DEnvCons` gc u es | ||
126 | gc u (e `DEnvCons` es) = e `DEnvCons` gc u es | ||
127 | |||
128 | dDown i DExpNil = Just DExpNil | ||
129 | dDown i (DExpCons_ u a b) = DExpCons_ <$> downFV i u <*> pure a <*> pure b | ||
130 | |||
131 | gc' :: Exp -> Exp | ||
132 | gc' (Let a b) = mkLet a $ gc' b | ||
133 | where | ||
134 | mkLet i (down 0 -> Just x) = x | ||
135 | mkLet i x = Let i x | ||
136 | gc' x = x | ||
61 | 137 | ||
62 | --------------------------------------------------------------------- toolbox: pretty print | 138 | --------------------------------------------------------------------- toolbox: pretty print |
63 | 139 | ||
64 | instance PShow Exp where | 140 | class ViewShow a where |
65 | pShow e@(Exp_ fv _) = --(("[" <> pShow fv <> "]") <+>) $ | 141 | viewShow :: Bool -> a -> Doc |
66 | case e of | 142 | |
143 | instance ViewShow Exp where | ||
144 | viewShow vi = pShow where | ||
145 | pShow e@(Exp_ fv x) = showFE green vi fv $ | ||
146 | case {-if vi then Exp_ (selfContract fv) x else-} e of | ||
67 | Var (Nat i) -> DVar i | 147 | Var (Nat i) -> DVar i |
68 | Let a b -> shLet (pShow a) $ pShow b | 148 | Let a b -> shLet (pShow a) $ pShow b |
69 | App a b -> DApp (pShow a) (pShow b) | ||
70 | Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) | 149 | Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) |
71 | Lam e -> shLam $ pShow e | 150 | Lam e -> shLam $ pShow e |
72 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs | 151 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs |
73 | Int i -> pShow i | 152 | Int i -> pShow' i |
74 | Y e -> "Y" `DApp` pShow e | 153 | Y e -> "Y" `DApp` pShow e |
75 | Op1 (HNF_ i) x -> DGlue (InfixL 40) (onred $ white $ if i == -1 then "this" else pShow i) $ DBrace (pShow x) | 154 | InHNF x -> DBrace (pShow x) |
76 | Op1 o x -> text (show o) `DApp` pShow x | 155 | Op1 o x -> text (show o) `DApp` pShow x |
77 | Op2 EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y) | 156 | Op2 o x y -> shOp2 o (pShow x) (pShow y) |
78 | Op2 Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y) | 157 | Case cn e xs -> shCase cn (pShow e) (pShow <$> xs) |
79 | Op2 o x y -> text (show o) `DApp` pShow x `DApp` pShow y | 158 | Exp_ u Var_ -> onblue $ pShow' u |
80 | Case cn e xs -> DPreOp (-20) (ComplexAtom "case" (-10) (pShow e) (SimpleAtom "of")) | 159 | e -> error $ "pShow @Exp: " ++ show e |
81 | $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- zip cn xs] | 160 | |
82 | 161 | glueTo = DGlue (InfixR 40) | |
83 | instance PShow MSt where | 162 | |
84 | pShow (MSt b bs) = pShow $ foldl f (HNF (-1) b) bs | 163 | shCase cn e xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of")) |
164 | $ foldr1 DSemi [DArr_ "->" (text a) b | (a, b) <- zip cn xs] | ||
165 | |||
166 | shOp2 AppOp x y = DApp x y | ||
167 | shOp2 EqInt x y = DOp "==" (Infix 4) x y | ||
168 | shOp2 Add x y = DOp "+" (InfixL 6) x y | ||
169 | shOp2 o x y = text (show o) `DApp` x `DApp` y | ||
170 | |||
171 | showFE c True fv | fv /= mempty = DGlue (InfixL 40) (c $ pShow' fv) | ||
172 | showFE _ _ _ = id | ||
173 | |||
174 | pShow' = pShow | ||
175 | |||
176 | instance ViewShow MSt where | ||
177 | viewShow vi (MSt env e) = g (onred $ white $ pShow e) env | ||
85 | where | 178 | where |
86 | f y = \case | 179 | pShow = viewShow vi |
87 | ELet x -> Let x y | 180 | |
88 | ELet1 x -> Let y x | 181 | g y DEnvNil = y |
89 | EApp1 i x -> HNF i $ App y x | 182 | g y z@(DEnvCons p env) = flip g env $ {-showFE red vi (case p of EnvPiece f _ -> f) $-} case p of |
90 | ECase i cns xs -> HNF i $ Case cns y xs | 183 | EDLet1 x -> shLet y (h x) |
91 | EOp2_1 i op x -> HNF i $ Op2 op y x | 184 | ELet x -> shLet (pShow x) y |
92 | EOp2_2 i op x -> HNF i $ Op2 op x y | 185 | ECase cns xs -> shCase cns y (pShow <$> xs) |
186 | EOp2_1 op x -> shOp2 op y (pShow x) | ||
187 | EOp2_2 op x -> shOp2 op (pShow x) y | ||
188 | |||
189 | h DExpNil = onred $ white "*" --TODO? | ||
190 | h z@(DExpCons p (h -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of | ||
191 | EDLet1 x -> shLet y (h x) | ||
192 | ELet x -> shLet (pShow x) y | ||
193 | ECase cns xs -> shCase cns y (pShow <$> xs) | ||
194 | EOp2_1 op x -> shOp2 op y (pShow x) | ||
195 | EOp2_2 op x -> shOp2 op (pShow x) y | ||
196 | |||
197 | instance PShow MSt where pShow = viewShow False | ||
198 | |||
93 | 199 | ||
94 | shUps a b = DPreOp (-20) (SimpleAtom $ show a) b | 200 | shUps a b = DPreOp (-20) (SimpleAtom $ show a) b |
95 | shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b | 201 | shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b |
@@ -114,75 +220,64 @@ pattern Int i <- Exp_ _ (Int_ i) | |||
114 | pattern Op2 op a b <- Exp_ u (Op2_ op (upp u -> a) (upp u -> b)) | 220 | pattern Op2 op a b <- Exp_ u (Op2_ op (upp u -> a) (upp u -> b)) |
115 | where Op2 op a b = Exp_ s $ Op2_ op az bz where (s, az, bz) = delta2 a b | 221 | where Op2 op a b = Exp_ s $ Op2_ op az bz where (s, az, bz) = delta2 a b |
116 | pattern Op1 op a <- Exp_ u (Op1_ op (upp u -> a)) | 222 | pattern Op1 op a <- Exp_ u (Op1_ op (upp u -> a)) |
117 | where Op1 op (Exp_ ab x) = Exp_ ab $ Op1_ op $ Exp_ (delUnused ab) x | 223 | where Op1 op (Exp_ ab x) = Exp_ ab $ Op1_ op $ Exp_ (selfContract ab) x |
118 | pattern Var' i = Exp_ (VarFV i) Var_ | 224 | pattern Var' i = Exp_ (VarFV i) Var_ |
119 | pattern Var i = Var' i | 225 | pattern Var i = Var' i |
120 | pattern Lam i <- Exp_ u (Lam_ (upp (incFV u) -> i)) | 226 | pattern Lam i <- Exp_ u (Lam_ (upp (incFV u) -> i)) |
121 | where Lam (Exp_ vs ax) = Exp_ (del1 vs) $ Lam_ $ Exp_ (compact vs) ax | 227 | where Lam (Exp_ vs ax) = Exp_ (sDrop 1 vs) $ Lam_ $ Exp_ (compact vs) ax |
122 | pattern Con a b i <- Exp_ u (Con_ a b (map (upp u) -> i)) | 228 | pattern Con a b i <- Exp_ u (Con_ a b (map (upp u) -> i)) |
123 | where Con a b x = Exp_ s $ Con_ a b bz where (s, bz) = deltas x | 229 | where Con a b x = Exp_ s $ Con_ a b bz where (s, bz) = deltas x |
124 | pattern Case a b c <- Exp_ u (Case_ a (upp u -> b) (map (upp u) -> c)) | 230 | pattern Case a b c <- Exp_ u (Case_ a (upp u -> b) (map (upp u) -> c)) |
125 | where Case cn a b = Exp_ s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b | 231 | where Case cn a b = Exp_ s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b |
126 | 232 | ||
127 | pattern Let i x = App (Lam x) i | 233 | pattern Let i x <- App (Lam x) i |
234 | where --Let i (down 0 -> Just x) = x -- exception with pakol | ||
235 | Let i x = App (Lam x) i | ||
128 | pattern Y a = Op1 YOp a | 236 | pattern Y a = Op1 YOp a |
129 | pattern HNF i a = Op1 (HNF_ i) a | 237 | pattern InHNF a = Op1 HNF_ a |
130 | pattern App a b = Op2 AppOp a b | 238 | pattern App a b = Op2 AppOp a b |
131 | pattern Seq a b = Op2 SeqOp a b | 239 | pattern Seq a b = Op2 SeqOp a b |
132 | 240 | ||
133 | infixl 4 `App` | 241 | infixl 4 `App` |
134 | 242 | ||
135 | initSt :: Exp -> MSt | 243 | delta2 (Exp_ ua a) (Exp_ ub b) = (s, Exp_ ua' a, Exp_ ub' b) |
136 | initSt e = MSt e [] | 244 | where |
137 | 245 | (s, ua', ub') = delta2' ua ub | |
138 | -- for statistics | ||
139 | size :: MSt -> Int | ||
140 | size (MSt _ ys) = length ys | ||
141 | 246 | ||
142 | delta2 (Exp_ ua a) (Exp_ ub b) = (s, Exp_ (delFV ua s) a, Exp_ (delFV ub s) b) | 247 | delta2' ua ub = (s, primContract s ua, primContract s ub) |
143 | where | 248 | where |
144 | s = ua <> ub | 249 | s = ua <> ub |
145 | 250 | ||
146 | deltas [] = (mempty, []) | 251 | deltas [] = (mempty, []) |
147 | deltas [Exp_ x e] = (x, [Exp_ (delUnused x) e]) | 252 | deltas [Exp_ x e] = (x, [Exp_ (selfContract x) e]) |
148 | deltas [Exp_ ua a, Exp_ ub b] = (s, [Exp_ (delFV ua s) a, Exp_ (delFV ub s) b]) | 253 | deltas [Exp_ ua a, Exp_ ub b] = (s, [Exp_ (primContract s ua) a, Exp_ (primContract s ub) b]) |
149 | where | 254 | where |
150 | s = ua <> ub | 255 | s = ua <> ub |
151 | deltas es = (s, [Exp_ (delFV u s) e | (u, Exp_ _ e) <- zip xs es]) | 256 | deltas es = (s, [Exp_ (primContract s u) e | (u, Exp_ _ e) <- zip xs es]) |
152 | where | 257 | where |
153 | xs = [ue | Exp_ ue _ <- es] | 258 | xs = [ue | Exp_ ue _ <- es] |
154 | 259 | ||
155 | s = mconcat xs | 260 | s = mconcat xs |
156 | 261 | ||
157 | upp :: FV -> Exp -> Exp | 262 | upp :: FV -> Exp -> Exp |
158 | upp a (Exp_ b e) = Exp_ (compFV a b) e | 263 | upp a (Exp_ b e) = Exp_ (expand a b) e |
159 | 264 | ||
160 | up l n (Exp_ us x) = Exp_ (upFV l n us) x | 265 | up l n (Exp_ us x) = Exp_ (upFV l n us) x |
161 | 266 | ||
162 | -- free variables set | 267 | -- free variables set |
163 | fvs (Exp_ us _) = usedFVs us | 268 | fvs (Exp_ us _) = usedFVs us |
164 | 269 | ||
165 | usedVar i (Exp_ us _) = usedFV i us | 270 | usedVar i (Exp_ us _) = sIndex us i |
271 | |||
272 | usedVar' i DExpNil = False | ||
273 | usedVar' i (DExpCons_ u _ _) = sIndex u i | ||
166 | 274 | ||
167 | down i (Exp_ us e) = Exp_ <$> downFV i us <*> pure e | 275 | down i (Exp_ us e) = Exp_ <$> downFV i us <*> pure e |
168 | 276 | ||
169 | --------------------------- | 277 | --------------------------- |
170 | 278 | ||
171 | tryRemoves xs = tryRemoves_ (Var' <$> xs) | 279 | initSt :: Exp -> MSt |
172 | 280 | initSt e = MSt DEnvNil e | |
173 | tryRemoves_ [] dt = dt | ||
174 | tryRemoves_ (Var' i: vs) dt = maybe (tryRemoves_ vs dt) (\(is, st) -> tryRemoves_ (is ++ catMaybes (down i <$> vs)) st) $ tryRemove_ i dt | ||
175 | where | ||
176 | tryRemove_ i (MSt e es) = (\b (is, c) -> (is, MSt b c)) <$> down i e <*> downDown i es | ||
177 | |||
178 | downDown i [] = Just ([], []) | ||
179 | downDown 0 (ELet x: xs) = Just (Var' <$> fvs x, xs) | ||
180 | downDown i (ELet x: xs) = (\x (is, xs) -> (up 0 1 <$> is, ELet x: xs)) <$> down (i-1) x <*> downDown (i-1) xs | ||
181 | downDown i (ELet1 x: xs) = (\x (is, xs) -> (is, ELet1 x: xs)) <$> down (i+1) x <*> downDown i xs | ||
182 | downDown i (EApp1 j x: xs) = (\x (is, xs) -> (is, EApp1 j x: xs)) <$> down i x <*> downDown i xs | ||
183 | downDown i (ECase j cns x: xs) = (\x (is, xs) -> (is, ECase j cns x: xs)) <$> traverse (down i) x <*> downDown i xs | ||
184 | downDown i (EOp2_1 j op x: xs) = (\x (is, xs) -> (is, EOp2_1 j op x: xs)) <$> down i x <*> downDown i xs | ||
185 | downDown i (EOp2_2 j op x: xs) = (\x (is, xs) -> (is, EOp2_2 j op x: xs)) <$> down i x <*> downDown i xs | ||
186 | 281 | ||
187 | ----------------------------------------------------------- machine code begins here | 282 | ----------------------------------------------------------- machine code begins here |
188 | 283 | ||
@@ -193,24 +288,32 @@ hnf = justResult . initSt | |||
193 | 288 | ||
194 | ---------------- | 289 | ---------------- |
195 | 290 | ||
291 | inHNF (InHNF a) = InHNF a | ||
292 | inHNF a = InHNF a | ||
293 | |||
196 | type GenSteps e | 294 | type GenSteps e |
197 | = (MSt -> e) | 295 | = (MSt -> e) |
198 | -- -> (StepTag -> e) | 296 | -> (StepTag -> (MSt -> e) -> MSt -> e) |
199 | -> (StepTag -> (MSt -> e) -> MSt -> e) | 297 | -> (StepTag -> (MSt -> e) -> (MSt -> e) -> MSt -> e) |
200 | -> (StepTag -> (MSt -> e) -> (MSt -> e) -> MSt -> e) | 298 | -> MSt -> e |
201 | -> MSt -> e | ||
202 | 299 | ||
203 | type StepTag = String | 300 | type StepTag = String |
204 | 301 | ||
302 | focusNotUsed (MSt (EDLet1 x `DEnvCons` _) _) = not $ usedVar' 0 x | ||
303 | focusNotUsed _ = True | ||
304 | |||
205 | steps :: forall e . Int -> GenSteps e | 305 | steps :: forall e . Int -> GenSteps e |
206 | steps lev nostep {-ready-} bind cont dt@(MSt e vs) = case e of | 306 | steps lev nostep bind cont st@(MSt DEnvNil (InHNF e)) = nostep st |
307 | steps lev nostep bind cont dt@(MSt vs e) = case e of | ||
207 | 308 | ||
208 | Int{} -> nostep dt --ready "hnf int" | 309 | InHNF{} -> goUp dt |
209 | Lam{} -> nostep dt --ready "hnf lam" | 310 | |
311 | Int{} -> ready "int" dt | ||
312 | Lam{} -> ready "lam" dt | ||
210 | 313 | ||
211 | Con cn i xs | 314 | Con cn i xs |
212 | | lz > 0 -> step "copy con" $ MSt (Con cn i xs') $ (ELet <$> zs) ++ vs -- share complex constructor arguments | 315 | | lz == 0 || focusNotUsed dt -> ready "con" dt |
213 | | otherwise -> nostep dt --ready "hnf con" | 316 | | otherwise -> ready "copy con" $ MSt (foldr DEnvCons vs $ ELet <$> zs) $ Con cn i xs' -- share complex constructor arguments |
214 | where | 317 | where |
215 | lz = Nat $ length zs | 318 | lz = Nat $ length zs |
216 | (xs', concat -> zs) = unzip $ f 0 xs | 319 | (xs', concat -> zs) = unzip $ f 0 xs |
@@ -218,122 +321,87 @@ steps lev nostep {-ready-} bind cont dt@(MSt e vs) = case e of | |||
218 | f i (x: xs) | simple x = (up 0 lz x, []): f i xs | 321 | f i (x: xs) | simple x = (up 0 lz x, []): f i xs |
219 | | otherwise = (Var' i, [up 0 (lz - i - 1) x]): f (i+1) xs | 322 | | otherwise = (Var' i, [up 0 (lz - i - 1) x]): f (i+1) xs |
220 | 323 | ||
221 | Var i -> lookupHNF i dt | 324 | -- TODO: handle recursive constants |
325 | Y x -> step "Y" $ MSt vs $ App x (Y x) | ||
326 | -- Y (Lam x) -> step "Y" $ MSt (ELet e `DEnvCons` vs) x | ||
222 | 327 | ||
223 | Seq a b -> hnf "seq hnf" focus $ MSt a $ EOp2_1 lev SeqOp b: vs | 328 | Var i -> step "var" $ zipDown i DExpNil vs |
224 | where | 329 | Seq a b -> step "seq" $ MSt (EOp2_1 SeqOp b `DEnvCons` vs) a |
225 | focus (MSt a xs) = case a of | 330 | Case cns a cs -> step "case" $ MSt (ECase cns cs `DEnvCons` vs) a |
226 | Int{} -> step "seq" $ MSt b vs | 331 | Op2 op a b -> step "op2_1" $ MSt (EOp2_1 op b `DEnvCons` vs) a |
227 | Lam{} -> step "seq" $ tryRemoves (fvs a) $ MSt b vs | ||
228 | Con{} -> step "seq" $ tryRemoves (fvs a) $ MSt b vs | ||
229 | _ -> nostep $ MSt (Seq a b) vs | ||
230 | where | ||
231 | (b, vs) = f xs | ||
232 | f (EOp2_1 _ SeqOp c: xs) = (c, xs) | ||
233 | f (ELet x: (f -> (c, xs))) = (up 0 1 c, ELet x: xs) | ||
234 | 332 | ||
235 | -- TODO: handle recursive constants | 333 | where |
236 | Y (Lam x) -> step "Y" $ MSt x $ ELet e: vs | 334 | bind' = bind -- _ f x = f x |
237 | 335 | ||
238 | App a b -> hnf "app hnf" focus $ MSt a $ EApp1 lev b: vs | 336 | ready :: StepTag -> MSt -> e |
239 | where | 337 | ready t (MSt vs e) = step (t ++ " ready") $ MSt vs $ inHNF e |
240 | focus (MSt a xs) = case a of | 338 | |
241 | Lam x | usedVar 0 x -> step "app" $ MSt x $ ELet b: vs | 339 | rec i = steps i nostep bind cont |
242 | | otherwise -> step "appdel" $ tryRemoves (fvs b) $ MSt x vs | 340 | |
243 | _ -> nostep $ MSt (App a b) vs | 341 | step :: StepTag -> MSt -> e |
244 | where | 342 | step t = bind t (rec lev) |
245 | (b, vs) = f xs | 343 | |
246 | f (EApp1 _ c: xs) = (c, xs) | 344 | zipDown 0 e (ELet z `DEnvCons` zs) = MSt (EDLet1 e `DEnvCons` zs) z |
247 | f (ELet x: (f -> (c, xs))) = (up 0 1 c, ELet x: xs) | 345 | zipDown j e (z@ELet{} `DEnvCons` zs) = zipDown (j-1) (z `DExpCons` e) zs |
248 | 346 | zipDown j e (z `DEnvCons` zs) = zipDown j (z `DExpCons` e) zs | |
249 | Case cns a cs -> hnf "case hnf" focus $ MSt a $ ECase lev cns cs: vs | 347 | |
250 | where | 348 | goUp = boot "." 0 |
251 | focus (MSt a xs) = case a of | 349 | |
252 | Con cn i es -> step "case" $ tryRemoves (nub $ foldMap fvs $ delElem i cs) $ MSt (foldl App (cs !! i) es) vs | 350 | boot t n (MSt (ELet x `DEnvCons` xs) e) = boot t (n+1) (MSt xs (Let x e)) |
253 | _ -> nostep $ MSt (Case cns a cs) vs | 351 | boot t n st@(MSt DEnvNil e) = ready "whnf" $ MSt DEnvNil $ gc' e -- $ iterate pakol' st !! n |
254 | where | 352 | boot t n st = bind' "boot half" (pakol n) st |
255 | ((cns, cs), vs) = f xs | 353 | |
256 | f (ECase _ cns cs: xs) = ((cns, cs), xs) | 354 | pakol 0 st = bind' "boot end" focus st |
257 | f (ELet x: (f -> (c, xs))) = (second (up 0 1 <$>) c, ELet x: xs) | 355 | pakol n (MSt (y `DEnvCons` xs) (Let x e)) = bind' "pakol" (pakol (n-1)) $ MSt (upP 0 1 y `DEnvCons` ELet x `DEnvCons` xs) e |
258 | 356 | pakol n st = error $ "pakol: " ++ show st | |
259 | Op2 op x y -> hnf "op2_1 hnf" focus1 $ MSt x $ EOp2_1 lev op y: vs | 357 | |
260 | where | 358 | pakol' (MSt xs (Let x e)) = MSt (ELet x `DEnvCons` xs) e |
261 | focus1 (MSt x xs) = hnf "op2_2 hnf" focus2 $ MSt y $ EOp2_2 lev op x: vs | 359 | |
262 | where | 360 | focus st@(MSt DEnvNil (InHNF a)) = ready "end" st -- TODO: a? |
263 | ((op, y), vs) = f xs | 361 | focus st@(MSt (DEnvCons x vs) (InHNF a)) = case x of |
264 | f (EOp2_1 _ op y: xs) = ((op, y), xs) | 362 | -- ELet{} -> focus $ MSt ( `DEnvCons` vs) e |
265 | f (ELet x: (f -> (c, xs))) = (second (up 0 1) c, ELet x: xs) | 363 | EOp2_1 SeqOp b -> case a of |
266 | 364 | Int{} -> step "seq" $ MSt vs b | |
267 | focus2 (MSt y xs) = case (x, y) of | 365 | Lam{} -> step "seq" $ MSt vs b -- remove a! |
268 | (Int e, Int f) -> step "op-done" $ MSt (int op e f) vs | 366 | Con{} -> step "seq" $ MSt vs b -- remove a! |
367 | _ -> ready "seq" $ MSt vs (Seq (InHNF a) b) | ||
368 | EOp2_1 AppOp b -> case a of | ||
369 | Lam x | usedVar 0 x -> step "app" $ MSt (ELet b `DEnvCons` vs) x | ||
370 | | otherwise -> step "appdel" $ MSt vs x -- remove b! | ||
371 | _ -> ready "app" $ MSt vs (App (InHNF a) b) | ||
372 | ECase cns cs -> case a of | ||
373 | Con cn i es -> step "case" $ MSt vs (foldl App (cs !! i) es) -- remove unused cases! | ||
374 | _ -> ready "case" $ MSt vs (Case cns (InHNF a) cs) | ||
375 | EOp2_1 op b -> step "op2_2 hnf" $ MSt (EOp2_2 op (InHNF a) `DEnvCons` vs) b | ||
376 | EOp2_2 op b -> case (b, a) of | ||
377 | (InHNF (Int e), Int f) -> step "op-done" $ MSt vs (int op e f) | ||
269 | where | 378 | where |
270 | int Add a b = Int $ a + b | 379 | int Add a b = Int $ a + b |
271 | int Sub a b = Int $ a - b | 380 | int Sub a b = Int $ a - b |
272 | int Mod a b = Int $ a `mod` b | 381 | int Mod a b = Int $ a `mod` b |
273 | int LessEq a b = if a <= b then T else F | 382 | int LessEq a b = if a <= b then T else F |
274 | int EqInt a b = if a == b then T else F | 383 | int EqInt a b = if a == b then T else F |
275 | _ -> nostep $ MSt (Op2 op x y) vs | 384 | _ -> ready "op2" $ MSt vs (Op2 op b (InHNF a)) |
276 | where | 385 | EDLet1 d | Just d' <- dDown 0 d -> zipUp a vs d' |
277 | ((op, x), vs) = f xs | 386 | EDLet1 d -> zipUp (up 0 1 a) (ELet (InHNF a) `DEnvCons` vs) d |
278 | f (EOp2_2 _ op x: xs) = ((op, x), xs) | ||
279 | f (ELet x: (f -> (c, xs))) = (second (up 0 1) c, ELet x: xs) | ||
280 | |||
281 | where | ||
282 | rec i = steps i nostep bind cont | ||
283 | |||
284 | step :: StepTag -> MSt -> e | ||
285 | step t = bind t (rec lev) | ||
286 | 387 | ||
388 | zipUp x xs DExpNil = ready "lookup" $ mSt xs x | ||
389 | zipUp x xs (DExpCons a@ELet{} as) = zipUp (up 0 1 x) (a `DEnvCons` xs) as | ||
390 | zipUp x xs (DExpCons a as) = zipUp x (a `DEnvCons` xs) as | ||
391 | {- | ||
287 | hnf :: StepTag -> (MSt -> e) -> MSt -> e | 392 | hnf :: StepTag -> (MSt -> e) -> MSt -> e |
288 | hnf t f = cont t f (rec $ 1 + lev) | 393 | hnf t f = bind ("hnf " ++ t) $ cont t f (rec (1 + lev)) |
289 | |||
290 | hnfTag (MSt b c) = MSt (HNF lev b) c | ||
291 | |||
292 | -- lookup var in head normal form | ||
293 | lookupHNF :: Nat -> MSt -> e | ||
294 | lookupHNF i@(Nat i') dt = hnf "var lookup" shiftLookup dt' | ||
295 | where | ||
296 | (path, dt') = shiftL [] i' $ hnfTag dt | ||
297 | |||
298 | shiftLookup st | ||
299 | = case boot (shiftR path . pakol') st of | ||
300 | (q, MSt HNF{} es) -> bind "remove" nostep $ tryRemoves [i] $ MSt (up 0 1 q) es | ||
301 | st -> error $ "sl: " ++ ppShow st | ||
302 | |||
303 | boot c (MSt e (ELet x: xs)) = boot (c . pakol) (MSt (Let x e) xs) | ||
304 | boot c st = c st | ||
305 | |||
306 | pakol (MSt (Let x e) (ELet1 y: xs)) = MSt e (ELet1 (up 1 1 y): ELet x: xs) | ||
307 | |||
308 | pakol' (MSt x (ELet1 y: xs)) = (x, MSt y (ELet x: xs)) | ||
309 | 394 | ||
310 | shiftL path 0 (MSt x (ELet e: es)) = (path, MSt e $ ELet1 x: es) | 395 | hnf' :: StepTag -> MSt -> e |
311 | shiftL path n (MSt x (ELet e: es)) = shiftL (TELet: path) (n-1) $ MSt (Let e x) es | 396 | hnf' t = hnf t $ bind ("focus " ++ t) $ boot t 0 |
312 | shiftL path n (MSt x (EApp1 i e: es)) = shiftL (TEApp1: path) n $ MSt (HNF i $ App x e) es | ||
313 | shiftL path n (MSt x (ECase i cns e: es)) = shiftL (TECase: path) n $ MSt (HNF i $ Case cns x e) es | ||
314 | shiftL path n (MSt x (EOp2_1 i op e: es)) = shiftL (TEOp2_1: path) n $ MSt (HNF i $ Op2 op x e) es | ||
315 | shiftL path n (MSt x (EOp2_2 i op e: es)) = shiftL (TEOp2_2: path) n $ MSt (HNF i $ Op2 op e x) es | ||
316 | shiftL path n (MSt x (ELet1 e: es)) = shiftL (TELet1: path) n $ MSt (Let x e) es | ||
317 | shiftL path n st = error $ "shiftL: " ++ show (path, n) ++ "\n" ++ ppShow st | ||
318 | 397 | ||
319 | shiftR [] st = st | 398 | -} |
320 | shiftR (TELet: n) (y, MSt (Let e x) es) = shiftR n (up 0 1 y, MSt x $ ELet e: es) | 399 | simple = \case |
321 | shiftR (TEApp1: n) (y, MSt (HNF l (App x e)) es) = shiftR n (y, MSt x $ EApp1 l e: es) | 400 | Var{} -> True |
322 | shiftR (TECase: n) (y, MSt (HNF l (Case cns x e)) es) = shiftR n (y, MSt x $ ECase l cns e: es) | 401 | Int{} -> True |
323 | shiftR (TEOp2_1: n) (y, MSt (HNF l (Op2 op x e)) es) = shiftR n (y, MSt x $ EOp2_1 l op e: es) | 402 | _ -> False |
324 | shiftR (TEOp2_2: n) (y, MSt (HNF l (Op2 op e x)) es) = shiftR n (y, MSt x $ EOp2_2 l op e: es) | ||
325 | shiftR (TELet1: n) (y, MSt (Let x e) es) = shiftR n (y, MSt x $ ELet1 e: es) | ||
326 | shiftR path x = error $ "shiftR: " ++ show path ++ "\n" ++ ppShow x | ||
327 | |||
328 | simple = \case | ||
329 | Var{} -> True | ||
330 | Int{} -> True | ||
331 | _ -> False | ||
332 | |||
333 | delElem i xs = take i xs ++ drop (i+1) xs | ||
334 | 403 | ||
335 | data TE = TELet | TELet1 | TEApp1 | TECase | TEOp2_1 | TEOp2_2 | 404 | delElem i xs = take i xs ++ drop (i+1) xs |
336 | deriving Show | ||
337 | 405 | ||
338 | ---------------------------------------------------------------------------------------- examples | 406 | ---------------------------------------------------------------------------------------- examples |
339 | 407 | ||
@@ -408,10 +476,12 @@ primes = 2:3: filter (\n -> and $ map (\p -> n `mod` p /= 0) (takeWhile (\x -> x | |||
408 | main = primes !! 3000 | 476 | main = primes !! 3000 |
409 | -} | 477 | -} |
410 | 478 | ||
479 | test'' = Lam (Int 4) `App` Int 3 | ||
480 | |||
411 | tests | 481 | tests |
412 | = hnf test == hnf (Int 13) | 482 | = hnf test == hnf (Int 13) |
413 | && hnf test' == hnf (Int 14) | 483 | && hnf test' == hnf (Int 14) |
414 | && hnf (Lam (Int 4) `App` Int 3) == hnf (Int 4) | 484 | && hnf test'' == hnf (Int 4) |
415 | && hnf (t' 10) == hnf (Int 55) | 485 | && hnf (t' 10) == hnf (Int 55) |
416 | && hnf (t'' 10) == hnf (Int 55) | 486 | && hnf (t'' 10) == hnf (Int 55) |
417 | 487 | ||