diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-06-02 20:11:30 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-06-02 20:11:30 +0200 |
commit | d68e8b537283ac97c9c0c6fda14e9de2fe36f980 (patch) | |
tree | 4e5b5e314d693877b0007d8ecee641a13dd76492 /prototypes/LamMachine.hs | |
parent | 6b4235b3ec5af4b60a89383ecda5d35269f9d9a0 (diff) |
refactoring
Diffstat (limited to 'prototypes/LamMachine.hs')
-rw-r--r-- | prototypes/LamMachine.hs | 432 |
1 files changed, 251 insertions, 181 deletions
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 | ||