diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-16 12:47:34 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-16 12:47:34 +0200 |
commit | c3bf9728ba74fbb363dcd00941419602568d645b (patch) | |
tree | b8ef15c74538974ff5b311c8ced3a8b2e49f9a3b | |
parent | 1df9d442261cd7ad9b889ca48b23ee34cf6121e9 (diff) |
refactoring
-rw-r--r-- | prototypes/LamMachine.hs | 308 |
1 files changed, 143 insertions, 165 deletions
diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs index 59342a58..b869285e 100644 --- a/prototypes/LamMachine.hs +++ b/prototypes/LamMachine.hs | |||
@@ -27,6 +27,7 @@ data Exp_ | |||
27 | | Y_ Exp | 27 | | Y_ Exp |
28 | | Int_ Int | 28 | | Int_ Int |
29 | | Lam_ Exp | 29 | | Lam_ Exp |
30 | | Let_ Exp Exp | ||
30 | 31 | ||
31 | | App_ Exp Exp | 32 | | App_ Exp Exp |
32 | | Seq_ Exp Exp | 33 | | Seq_ Exp Exp |
@@ -35,9 +36,6 @@ data Exp_ | |||
35 | | Op1_ Op1 Exp | 36 | | Op1_ Op1 Exp |
36 | | Op2_ Op2 Exp Exp | 37 | | Op2_ Op2 Exp Exp |
37 | 38 | ||
38 | | Ups_ [Up] Exp | ||
39 | -- deriving (Eq) | ||
40 | |||
41 | data Op1 = Round | 39 | data Op1 = Round |
42 | deriving (Eq, Show) | 40 | deriving (Eq, Show) |
43 | 41 | ||
@@ -45,14 +43,7 @@ data Op2 = Add | Sub | Mod | LessEq | EqInt | |||
45 | deriving (Eq, Show) | 43 | deriving (Eq, Show) |
46 | 44 | ||
47 | -- cached free variables set | 45 | -- cached free variables set |
48 | data Exp = Exp' FreeVars Exp_ | 46 | data Exp = Exp {dbUps :: [Up], maxFreeVars :: Int, expexp :: Exp_ } |
49 | |||
50 | pattern Exp a b <- Exp' a b | ||
51 | where Exp a b = compact a b | ||
52 | |||
53 | compact a b@Ups_{} = Exp' a b | ||
54 | compact a b | a == FreeVars (2^maxFreeVar a - 1) = Exp' a b | ||
55 | | otherwise = tracePShow (a, Exp' undefined b) $ Exp' a b | ||
56 | 47 | ||
57 | -- state of the machine | 48 | -- state of the machine |
58 | data MSt = MSt [(FreeVars, Exp)] -- TODO: use finger tree instead of list | 49 | data MSt = MSt [(FreeVars, Exp)] -- TODO: use finger tree instead of list |
@@ -62,20 +53,23 @@ data MSt = MSt [(FreeVars, Exp)] -- TODO: use finger tree instead of list | |||
62 | --------------------------------------------------------------------- toolbox: pretty print | 53 | --------------------------------------------------------------------- toolbox: pretty print |
63 | 54 | ||
64 | instance PShow Exp where | 55 | instance PShow Exp where |
65 | pShow x = case pushUps x of | 56 | pShow e@(Exp u t x) = case e of -- shUps' u t $ case Exp [] t x of |
66 | Var_ i -> DVar i | 57 | Var i -> DVar i |
67 | App_ a b -> DApp (pShow a) (pShow b) | 58 | App a b -> DApp (pShow a) (pShow b) |
68 | Seq_ a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) | 59 | Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b) |
69 | Lam_ e -> shLam_ True $ pShow e | 60 | Lam e -> shLam_ True $ pShow e |
70 | Con_ s i xs -> foldl DApp (text s) $ pShow <$> xs | 61 | Let a b -> shLet_ (pShow a) $ pShow b |
71 | Int_ i -> pShow i | 62 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs |
72 | Op1_ o x -> text (show o) `DApp` pShow x | 63 | Int i -> pShow i |
73 | Op2_ EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y) | 64 | Op1 o x -> text (show o) `DApp` pShow x |
74 | Op2_ Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y) | 65 | Op2 EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y) |
75 | Op2_ o x y -> text (show o) `DApp` pShow x `DApp` pShow y | 66 | Op2 Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y) |
76 | Y_ e -> "Y" `DApp` pShow e | 67 | Op2 o x y -> text (show o) `DApp` pShow x `DApp` pShow y |
77 | Case_ e xs -> DPreOp (-20) (ComplexAtom "case" (-10) (pShow e) (SimpleAtom "of")) $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- xs] | 68 | Y e -> "Y" `DApp` pShow e |
78 | Ups_ u xs -> DPreOp (-20) (SimpleAtom $ show u) $ pShow xs | 69 | Case e xs -> DPreOp (-20) (ComplexAtom "case" (-10) (pShow e) (SimpleAtom "of")) $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- xs] |
70 | |||
71 | shUps a b = DPreOp (-20) (SimpleAtom $ show a) b | ||
72 | shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b | ||
79 | 73 | ||
80 | shLam_ usedVar b = DFreshName usedVar $ showLam (DVar 0) b | 74 | shLam_ usedVar b = DFreshName usedVar $ showLam (DVar 0) b |
81 | 75 | ||
@@ -98,83 +92,112 @@ instance PShow MSt where | |||
98 | 92 | ||
99 | --------------------------------------------------------------------- toolbox: free variables | 93 | --------------------------------------------------------------------- toolbox: free variables |
100 | 94 | ||
101 | --instance Eq Exp where Exp _ a == Exp _ b = a == b | 95 | maxFreeVars' (Exp u k _) = upsFreeVars' u k |
96 | |||
97 | upsFreeVars xs s = foldr rearr s xs | ||
98 | |||
99 | upsFreeVars' xs s = foldr rearr' s xs | ||
100 | where | ||
101 | rearr' (Up l n) m | ||
102 | | l >= m = m -- TODO: remove | ||
103 | | otherwise = n + m | ||
104 | |||
105 | upVarIndex xs s = foldr rearr' s xs | ||
106 | where | ||
107 | rearr' (Up l n) i | ||
108 | | l > i = i | ||
109 | | otherwise = n + i | ||
110 | |||
102 | 111 | ||
112 | -- TODO: remove | ||
103 | instance HasFreeVars Exp where | 113 | instance HasFreeVars Exp where |
104 | getFreeVars (Exp fv _) = fv | 114 | getFreeVars (Exp us fv e) = upsFreeVars us $ FreeVars $ 2^fv - 1 |
105 | 115 | ||
106 | upss [] (getUs -> (_, e)) = e | 116 | fvs (Exp us fv _) = gen 0 $ foldr f [fv] us where |
107 | upss u (getUs -> (_, e)) = Ups u e | 117 | f (Up l n) xs = l: l+n: map (+n) xs |
118 | gen i (a: xs) = [i..a-1] ++ gen' xs | ||
119 | gen' [] = [] | ||
120 | gen' (a: xs) = gen a xs | ||
108 | 121 | ||
109 | upss_ [] (Exp _ e) = e | 122 | upss u (Exp _ i e) = Exp u i e |
110 | upss_ u e = Ups_ u e | ||
111 | 123 | ||
112 | dup2 f ax bx = upss_ s $ Exp (getFreeVars az <> getFreeVars bz) $ f az bz where | 124 | dup2 f ax bx = Exp s (maxFreeVars' az `max` maxFreeVars' bz) $ f az bz where |
113 | (s, [a', b']) = deltaUps [ax, bx] | 125 | (s, [a', b']) = deltaUps [ax, bx] |
114 | az = upss a' ax | 126 | az = upss a' ax |
115 | bz = upss b' bx | 127 | bz = upss b' bx |
116 | 128 | ||
117 | dup1 f (Ups a ax) = upss_ a $ Exp (getFreeVars ax) $ f ax | 129 | dup1 :: (Exp -> Exp_) -> Exp -> Exp |
118 | dup1 f x = f x | 130 | dup1 f (Exp a b x) = Exp a b $ f $ Exp [] b x |
119 | 131 | ||
120 | getUs (Ups x y) = (x, y) | 132 | dupCon f [] = Exp [] 0 $ f [] |
121 | getUs y = ([], y) | 133 | dupCon f bx = Exp s (maximum $ maxFreeVars' <$> bz) $ f bz where |
122 | |||
123 | dupCon f [] = f [] | ||
124 | --dupCon f [Ups a ax] = Ups_ a $ Exp (getFreeVars ax) $ f [ax] | ||
125 | dupCon f bx = upss_ s $ Exp (foldMap getFreeVars bz) $ f bz where | ||
126 | (s, b') = deltaUps bx | 134 | (s, b') = deltaUps bx |
127 | bz = zipWith upss b' bx | 135 | bz = zipWith upss b' bx |
128 | 136 | ||
129 | dupCase f ax (unzip -> (ss, bx)) | 137 | dupCase f ax (unzip -> (ss, bx)) |
130 | = upss_ s $ Exp (getFreeVars az <> foldMap getFreeVars bz) $ f az $ zip ss bz | 138 | = Exp s (maxFreeVars' az `max` maximum (maxFreeVars' <$> bz)) $ f az $ zip ss bz |
131 | where | 139 | where |
132 | (s, a': b') = deltaUps $ ax: bx | 140 | (s, a': b') = deltaUps $ ax: bx |
133 | az = upss a' ax | 141 | az = upss a' ax |
134 | bz = zipWith upss b' bx | 142 | bz = zipWith upss b' bx |
135 | 143 | ||
136 | dupLam f (Ups a ax) = upss_ (ff a) $ Exp (shiftFreeVars (-1) $ getFreeVars ax') $ f ax' | 144 | dupLam f e@(Exp a fv ax) = Exp (ff a) (max 0 $ fv - 1) $ f $ Exp (gg a) fv ax |
137 | where | 145 | where |
138 | ax' = case a of | 146 | gg (Up 0 n: _) = [Up 0 1] |
139 | Up 0 n: _ -> up (Up 0 1) ax | 147 | gg _ = [] |
140 | _ -> ax | 148 | |
141 | ff (Up 0 n: us) = insertUp (Up 0 $ n - 1) $ incUp (-1) <$> us | 149 | ff (Up 0 n: us) = insertUp (Up 0 $ n - 1) $ incUp (-1) <$> us |
142 | ff us = incUp (-1) <$> us | 150 | ff us = incUp (-1) <$> us |
143 | dupLam f x = f x | 151 | |
144 | 152 | -- (\x -> e) f x = f in e | |
145 | 153 | dupLet f z w = case Lam w `App` z of | |
146 | pattern Int i <- Exp _ (Int_ i) | 154 | Exp a fv (App_ (Exp b fv' (Lam_ c)) d) -> Exp a fv $ Let_ d c |
147 | where Int i = Exp mempty $ Int_ i | 155 | |
148 | pattern App a b <- Exp _ (App_ a b) | 156 | |
149 | where App a b = Exp (getFreeVars a <> getFreeVars b) $ dup2 App_ a b | 157 | pattern Int i <- Exp _ _ (Int_ i) |
150 | pattern Seq a b <- Exp _ (Seq_ a b) | 158 | where Int i = Exp [] 0 $ Int_ i |
151 | where Seq a b = Exp (getFreeVars a <> getFreeVars b) $ dup2 Seq_ a b | 159 | pattern App a b <- Exp u _ (App_ (upp u -> a) (upp u -> b)) |
152 | pattern Op2 op a b <- Exp _ (Op2_ op a b) | 160 | where App a b = dup2 App_ a b |
153 | where Op2 op a b = Exp (getFreeVars a <> getFreeVars b) $ dup2 (Op2_ op) a b | 161 | pattern Seq a b <- Exp u _ (Seq_ (upp u -> a) (upp u -> b)) |
154 | pattern Op1 op a <- Exp _ (Op1_ op a) | 162 | where Seq a b = dup2 Seq_ a b |
155 | where Op1 op a = Exp (getFreeVars a) $ dup1 (Op1_ op) a | 163 | pattern Op2 op a b <- Exp u _ (Op2_ op (upp u -> a) (upp u -> b)) |
156 | pattern Var i <- Exp _ (Var_ i) | 164 | where Op2 op a b = dup2 (Op2_ op) a b |
157 | where Var 0 = Exp (freeVar 0) $ Var_ 0 | 165 | pattern Op1 op a <- Exp u _ (Op1_ op (upp u -> a)) |
158 | Var i = Ups [Up 0 i] $ Exp (freeVar 0) $ Var_ 0 | 166 | where Op1 op a = dup1 (Op1_ op) a |
159 | pattern Lam i <- Exp _ (Lam_ i) | 167 | pattern Var i <- Exp u _ (Var_ (upVarIndex u -> i)) |
160 | where Lam i = Exp (shiftFreeVars (-1) $ getFreeVars i) $ dupLam Lam_ i | 168 | where Var 0 = Exp [] 1 $ Var_ 0 |
161 | pattern Y i <- Exp _ (Y_ i) | 169 | Var i = Exp [Up 0 i] 1 $ Var_ 0 |
162 | where Y i = Exp (getFreeVars i) $ dup1 Y_ i | 170 | pattern Lam i <- Exp u _ (Lam_ (upp (incUp 1 <$> u) -> i)) |
163 | pattern Con a b i <- Exp _ (Con_ a b i) | 171 | where Lam i = dupLam Lam_ i |
164 | where Con a b i = Exp (foldMap getFreeVars i) $ dupCon (Con_ a b) i | 172 | pattern Let i x <- Exp u _ (Let_ (upp u -> i) (upp (incUp 1 <$> u) -> x)) |
165 | pattern Case a b <- Exp _ (Case_ a b) | 173 | where Let i x = dupLet Let_ i x |
166 | where Case a b = Exp (getFreeVars a <> foldMap (getFreeVars . snd) b) $ dupCase Case_ a b | 174 | pattern Y i <- Exp u _ (Y_ (upp u -> i)) |
167 | pattern Ups op a <- Exp _ (Ups_ op a) | 175 | where Y i = dup1 Y_ i |
168 | where Ups op a = Exp (upsFreeVars op $ getFreeVars a) $ Ups_ op a | 176 | pattern Con a b i <- Exp u _ (Con_ a b (map (upp u) -> i)) |
177 | where Con a b i = dupCon (Con_ a b) i | ||
178 | pattern Case a b <- Exp u _ (Case_ (upp u -> a) (map (second $ upp u) -> b)) | ||
179 | where Case a b = dupCase Case_ a b | ||
180 | --pattern Ups op a <- Exp _ (Ups_ op a) | ||
181 | -- where Ups op a = Exp ( | ||
182 | |||
183 | upp u x = foldr up x u | ||
184 | |||
185 | up :: Up -> Exp -> Exp | ||
186 | up u@(Up i num) e@(Exp us s x) | ||
187 | | dbGE'' i e = e | ||
188 | | otherwise = addUp u e | ||
189 | |||
169 | 190 | ||
170 | infixl 4 `App` | 191 | infixl 4 `App` |
171 | 192 | ||
172 | --------------------------------------------------------------------- toolbox: de bruijn index shifting | 193 | --------------------------------------------------------------------- toolbox: de bruijn index shifting |
173 | -- TODO: speedup these with reification | ||
174 | 194 | ||
175 | rearr (Up l n) = rearrangeFreeVars (RFUp n) l | 195 | data Up = Up !Int{-level-} !Int{-num-} |
196 | deriving (Eq, Show) | ||
176 | 197 | ||
177 | upsFreeVars xs s = foldr rearr s xs | 198 | incUp t (Up l n) = Up (l+t) n |
199 | |||
200 | rearr (Up l n) = rearrangeFreeVars (RFUp n) l | ||
178 | 201 | ||
179 | showUps us n = foldr f (replicate n True) us where | 202 | showUps us n = foldr f (replicate n True) us where |
180 | f (Up l n) is = take l is ++ replicate n False ++ drop l is | 203 | f (Up l n) is = take l is ++ replicate n False ++ drop l is |
@@ -219,17 +242,13 @@ mkUps = f 0 | |||
219 | f i [] = [] | 242 | f i [] = [] |
220 | f i (x: xs) = insertUp (Up (x-i) 1) $ f (i+1) xs | 243 | f i (x: xs) = insertUp (Up (x-i) 1) $ f (i+1) xs |
221 | 244 | ||
222 | deltaUps = deltaUps_ . map (crk . getUs) | 245 | deltaUps = deltaUps_ . map crk |
223 | 246 | ||
224 | deltaUps_ (map $ uncurry showUps -> us) = (mkUps $ back s, [mkUps $ u `diffUps` s | u <- us]) | 247 | deltaUps_ (map $ uncurry showUps -> us) = (mkUps $ back s, [mkUps $ u `diffUps` s | u <- us]) |
225 | where | 248 | where |
226 | s = foldr1 sect $ us | 249 | s = foldr1 sect $ us |
227 | 250 | ||
228 | crk (s, e) = (s, maxFreeVar $ getFreeVars e) | 251 | crk (Exp u e _) = (u, e) |
229 | |||
230 | maxFreeVar (FreeVars i) = f 0 i where | ||
231 | f i 0 = i | ||
232 | f i n = f (i+1) (n `div` 2) | ||
233 | 252 | ||
234 | joinUps a b = foldr insertUp b a | 253 | joinUps a b = foldr insertUp b a |
235 | 254 | ||
@@ -249,38 +268,7 @@ insertUp u@(Up l n) us_@(u'@(Up l' n'): us) | |||
249 | | l >= l' && l <= l' + n' = Up l' (n' + n): us | 268 | | l >= l' && l <= l' + n' = Up l' (n' + n): us |
250 | | otherwise = u': insertUp (Up (l-n') n) us | 269 | | otherwise = u': insertUp (Up (l-n') n) us |
251 | 270 | ||
252 | addUp (Up _ 0) e = e | 271 | addUp u (Exp us k e) = Exp (insertUp u us) k e -- TODO: remove excess ups? |
253 | addUp u (Exp s (Ups_ us e)) = Exp (rearr u s) $ Ups_ (insertUp u us) e | ||
254 | addUp u e = Ups [u] e | ||
255 | |||
256 | pushUps :: Exp -> Exp_ | ||
257 | pushUps (Ups us (Exp _ e)) = foldr pushUp e us | ||
258 | pushUps (Exp _ e) = e | ||
259 | |||
260 | pushUp u@(Up i num) x | ||
261 | -- | dbGE i s = e | ||
262 | | otherwise = case x of | ||
263 | App_ a b -> App_ (f a) (f b) | ||
264 | Seq_ a b -> Seq_ (f a) (f b) | ||
265 | Con_ cn s xs -> Con_ cn s (f <$> xs) | ||
266 | Case_ s xs -> Case_ (f s) (second f <$> xs) | ||
267 | Lam_ e -> Lam_ (up (Up (i+1) num) e) | ||
268 | Var_ k | i <= k -> Var_ (k + num) | ||
269 | | otherwise -> Var_ k | ||
270 | x@Int_{} -> x | ||
271 | Y_ a -> Y_ $ f a | ||
272 | Op1_ op a -> Op1_ op (f a) | ||
273 | Op2_ op a b -> Op2_ op (f a) (f b) | ||
274 | where | ||
275 | f = up u | ||
276 | |||
277 | data Up = Up !Int{-level-} !Int{-num-} | ||
278 | deriving (Eq, Show) | ||
279 | |||
280 | up :: Up -> Exp -> Exp | ||
281 | up u@(Up i num) e@(Exp s x) | ||
282 | | dbGE i s = e | ||
283 | | otherwise = addUp u e | ||
284 | 272 | ||
285 | ups' a b = ups $ Up a b | 273 | ups' a b = ups $ Up a b |
286 | 274 | ||
@@ -290,8 +278,6 @@ ups l@(Up i _) xs@((s, e): es) | |||
290 | | dbGE i s = xs | 278 | | dbGE i s = xs |
291 | | otherwise = eP (up l e) $ ups (incUp 1 l) es | 279 | | otherwise = eP (up l e) $ ups (incUp 1 l) es |
292 | 280 | ||
293 | incUp t (Up l n) = Up (l+t) n | ||
294 | |||
295 | eP x [] = [(getFreeVars x, x)] | 281 | eP x [] = [(getFreeVars x, x)] |
296 | eP x xs@((s, _):_) = (getFreeVars x <> lowerFreeVars s, x): xs | 282 | eP x xs@((s, _):_) = (getFreeVars x <> lowerFreeVars s, x): xs |
297 | 283 | ||
@@ -302,30 +288,22 @@ pattern EPP x <- (_, x) | |||
302 | down i x | usedVar i x = Nothing | 288 | down i x | usedVar i x = Nothing |
303 | down i x = Just $ down_ i x | 289 | down i x = Just $ down_ i x |
304 | 290 | ||
305 | down_ i e@(Exp s x) | 291 | dbGE' l m = l >= m |
306 | | dbGE i s = e | 292 | |
307 | down_ i0 e0@(Ups us e) = f i0 us e where | 293 | dbGE'' l m = dbGE' l $ maxFreeVars' m |
308 | f i [] e = error $ "-- - - -- " ++ show (i0, i) ++ " " ++ ppShow e0 ++ "\n" ++ ppShow e --(pushUps e) --"show down_ i e | 294 | |
295 | down_ i e | ||
296 | | dbGE'' i e = e | ||
297 | down_ i0 e0@(Exp us ii e) = f i0 us e where | ||
298 | f i [] e = error $ "-- - - -- " ++ show (i0, i) ++ " " ++ ppShow e0 --(pushUps e) --"show down_ i e | ||
309 | f i (u@(Up j n): us) e | 299 | f i (u@(Up j n): us) e |
310 | | i < j = addUp (Up (j-1) n) $ f i us e | 300 | | i < j = addUp (Up (j-1) n) $ f i us e |
311 | | i >= j + n = addUp u $ f (i-n) us e | 301 | | i >= j + n = addUp u $ f (i-n) us e |
312 | | otherwise = addUp (Up j $ n-1) $ Ups us e | 302 | | otherwise = addUp (Up j $ n-1) $ Exp us ii e |
313 | down_ i e@(Exp s x) = Exp (delVar i s) $ case x of | 303 | |
314 | Var_ j | j > i -> Var_ $ j - 1 | 304 | tryRemoves xs = tryRemoves_ (Var <$> xs) |
315 | | otherwise -> Var_ j | ||
316 | Lam_ e -> Lam_ $ down_ (i+1) e | ||
317 | Y_ e -> Y_ $ down_ i e | ||
318 | App_ a b -> App_ (down_ i a) (down_ i b) | ||
319 | Seq_ a b -> Seq_ (down_ i a) (down_ i b) | ||
320 | Con_ s k es -> Con_ s k $ (down_ i <$> es) | ||
321 | Case_ e es -> Case_ (down_ i e) $ map (second $ down_ i) es | ||
322 | Int_ i -> Int_ i | ||
323 | Op1_ o e -> Op1_ o $ down_ i e | ||
324 | Op2_ o e f -> Op2_ o (down_ i e) (down_ i f) | ||
325 | |||
326 | tryRemoves xs = tryRemoves_ (Var <$> freeVars xs) | ||
327 | tryRemoves_ [] dt = dt | 305 | tryRemoves_ [] dt = dt |
328 | tryRemoves_ ((pushUps -> Var_ i): vs) dt | 306 | tryRemoves_ (Var i: vs) dt |
329 | | Just dt' <- tryRemove_ i dt | 307 | | Just dt' <- tryRemove_ i dt |
330 | = tryRemoves_ (catMaybes $ down i <$> vs) dt' | 308 | = tryRemoves_ (catMaybes $ down i <$> vs) dt' |
331 | | otherwise = tryRemoves_ vs dt | 309 | | otherwise = tryRemoves_ vs dt |
@@ -397,13 +375,13 @@ runMachinePure e = putStr $ unlines $ ppShow t: [] | |||
397 | 375 | ||
398 | -- big step | 376 | -- big step |
399 | step :: MachineMonad m => MSt -> m MSt | 377 | step :: MachineMonad m => MSt -> m MSt |
400 | step dt@(MSt t e vs) = case pushUps e of | 378 | step dt@(MSt t e vs) = case e of |
401 | 379 | ||
402 | Int_{} -> return dt | 380 | Int{} -> return dt |
403 | 381 | ||
404 | Lam_{} -> return dt | 382 | Lam{} -> return dt |
405 | 383 | ||
406 | Con_ cn i xs | 384 | Con cn i xs |
407 | | lz /= 0 -> return $ MSt (ups' 1 lz t) (Con cn i xs') $ zs ++ vs -- share complex constructor arguments | 385 | | lz /= 0 -> return $ MSt (ups' 1 lz t) (Con cn i xs') $ zs ++ vs -- share complex constructor arguments |
408 | | otherwise -> return dt | 386 | | otherwise -> return dt |
409 | where | 387 | where |
@@ -413,43 +391,43 @@ step dt@(MSt t e vs) = case pushUps e of | |||
413 | f i (x: xs) | simple x = (up (Up 0 lz) x, []): f i xs | 391 | f i (x: xs) | simple x = (up (Up 0 lz) x, []): f i xs |
414 | | otherwise = (Var i, [up (Up 0 (lz - i - 1)) x]): f (i+1) xs | 392 | | otherwise = (Var i, [up (Up 0 (lz - i - 1)) x]): f (i+1) xs |
415 | 393 | ||
416 | Var_ i -> lookupHNF "var" (\e _ -> e) i dt | 394 | Var i -> lookupHNF "var" (\e _ -> e) i dt |
417 | 395 | ||
418 | Seq_ a b -> case pushUps a of | 396 | Seq a b -> case a of |
419 | Int_{} -> stepMsg "seq" $ MSt t b vs | 397 | Int{} -> stepMsg "seq" $ MSt t b vs |
420 | Lam_{} -> stepMsg "seq" $ tryRemoves (getFreeVars a) $ MSt t b vs | 398 | Lam{} -> stepMsg "seq" $ tryRemoves (fvs a) $ MSt t b vs |
421 | Con_{} -> stepMsg "seq" $ tryRemoves (getFreeVars a) $ MSt t b vs | 399 | Con{} -> stepMsg "seq" $ tryRemoves (fvs a) $ MSt t b vs |
422 | Var_ i -> lookupHNF' "seqvar" (\e (pushUps -> Seq_ _ b) -> b) i dt | 400 | Var i -> lookupHNF' "seqvar" (\e (Seq _ b) -> b) i dt |
423 | _ -> stepMsg "seqexp" $ MSt (ups' 1 1 t) (Seq (Var 0) $ up (Up 0 1) b) $ a: vs | 401 | _ -> stepMsg "seqexp" $ MSt (ups' 1 1 t) (Seq (Var 0) $ up (Up 0 1) b) $ a: vs |
424 | 402 | ||
425 | -- TODO: handle recursive constants | 403 | -- TODO: handle recursive constants |
426 | Y_ (pushUps -> Lam_ x) -> stepMsg "Y" $ MSt (ups' 1 1 t) x $ e: vs | 404 | Y (Lam x) -> stepMsg "Y" $ MSt (ups' 1 1 t) x $ e: vs |
427 | 405 | ||
428 | App_ a b -> case pushUps a of | 406 | App a b -> case a of |
429 | Lam_ x | usedVar 0 x | 407 | Lam x | usedVar 0 x |
430 | -> stepMsg "app" $ MSt (ups' 1 1 t) x $ b: vs | 408 | -> stepMsg "app" $ MSt (ups' 1 1 t) x $ b: vs |
431 | Lam_ x -> stepMsg "appdel" $ tryRemoves (getFreeVars b) $ MSt t x vs | 409 | Lam x -> stepMsg "appdel" $ tryRemoves (fvs b) $ MSt t x vs |
432 | Var_ i -> lookupHNF' "appvar" (\e (pushUps -> App_ _ y) -> App e y) i dt | 410 | Var i -> lookupHNF' "appvar" (\e (App _ y) -> App e y) i dt |
433 | _ -> stepMsg "appexp" $ MSt (ups' 1 1 t) (App (Var 0) $ up (Up 0 1) b) $ a: vs | 411 | _ -> stepMsg "appexp" $ MSt (ups' 1 1 t) (App (Var 0) $ up (Up 0 1) b) $ a: vs |
434 | 412 | ||
435 | Case_ a cs -> case pushUps a of | 413 | Case a cs -> case a of |
436 | Con_ cn i es -> stepMsg "case" $ tryRemoves (foldMap (getFreeVars . snd) $ delElem i cs) $ (MSt t (foldl App (snd $ cs !! i) es) vs) | 414 | Con cn i es -> stepMsg "case" $ tryRemoves (nub $ foldMap (fvs . snd) $ delElem i cs) $ (MSt t (foldl App (snd $ cs !! i) es) vs) |
437 | Var_ i -> lookupHNF' "casevar" (\e (pushUps -> Case_ _ cs) -> Case e cs) i dt | 415 | Var i -> lookupHNF' "casevar" (\e (Case _ cs) -> Case e cs) i dt |
438 | _ -> stepMsg "caseexp" $ MSt (ups' 1 1 t) (Case (Var 0) $ second (up (Up 0 1)) <$> cs) $ a: vs | 416 | _ -> stepMsg "caseexp" $ MSt (ups' 1 1 t) (Case (Var 0) $ second (up (Up 0 1)) <$> cs) $ a: vs |
439 | 417 | ||
440 | Op2_ op x y -> case (pushUps x, pushUps y) of | 418 | Op2 op x y -> case (x, y) of |
441 | (Int_ e, Int_ f) -> return $ MSt t (int op e f) vs | 419 | (Int e, Int f) -> return $ MSt t (int op e f) vs |
442 | where | 420 | where |
443 | int Add a b = Int $ a + b | 421 | int Add a b = Int $ a + b |
444 | int Sub a b = Int $ a - b | 422 | int Sub a b = Int $ a - b |
445 | int Mod a b = Int $ a `mod` b | 423 | int Mod a b = Int $ a `mod` b |
446 | int LessEq a b = if a <= b then T else F | 424 | int LessEq a b = if a <= b then T else F |
447 | int EqInt a b = if a == b then T else F | 425 | int EqInt a b = if a == b then T else F |
448 | (Var_ i, _) -> lookupHNF' "op2-1var" (\e (pushUps -> Op2_ op _ y) -> Op2 op e y) i dt | 426 | (Var i, _) -> lookupHNF' "op2-1var" (\e (Op2 op _ y) -> Op2 op e y) i dt |
449 | (_, Var_ i) -> lookupHNF' "op2-2var" (\e (pushUps -> Op2_ op x _) -> Op2 op x e) i dt | 427 | (_, Var i) -> lookupHNF' "op2-2var" (\e (Op2 op x _) -> Op2 op x e) i dt |
450 | (Int_{}, _) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op x (Var 0)) $ y: vs | 428 | (Int{}, _) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op x (Var 0)) $ y: vs |
451 | (_, Int_{}) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op (Var 0) y) $ x: vs | 429 | (_, Int{}) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op (Var 0) y) $ x: vs |
452 | _ -> stepMsg "op2" $ MSt (ups' 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs | 430 | _ -> stepMsg "op2" $ MSt (ups' 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs |
453 | 431 | ||
454 | stepMsg :: MachineMonad m => String -> MSt -> m MSt | 432 | stepMsg :: MachineMonad m => String -> MSt -> m MSt |
455 | stepMsg msg dt = do | 433 | stepMsg msg dt = do |