diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-06-03 22:35:02 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-06-03 22:35:02 +0200 |
commit | 57fd497f487b83d6eab1e2ca05e6ff5722af6938 (patch) | |
tree | 3df37ab7bc6bd1eaaef8647e1c4332aa40d2f557 /prototypes/LamMachine.hs | |
parent | 85dbc0c083fef4801c64a2810dd8021bdd8fa2ac (diff) |
refactoring
Diffstat (limited to 'prototypes/LamMachine.hs')
-rw-r--r-- | prototypes/LamMachine.hs | 253 |
1 files changed, 137 insertions, 116 deletions
diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs index a3e620e7..d878bcb4 100644 --- a/prototypes/LamMachine.hs +++ b/prototypes/LamMachine.hs | |||
@@ -27,31 +27,44 @@ import FreeVars | |||
27 | 27 | ||
28 | --------------------------------------------------------------------- data structures | 28 | --------------------------------------------------------------------- data structures |
29 | 29 | ||
30 | data Lit | ||
31 | = LInt !Int | ||
32 | | LChar !Char | ||
33 | | LFloat !Double | ||
34 | deriving Eq | ||
35 | |||
30 | data Exp_ | 36 | data Exp_ |
31 | = Var_ | 37 | = Var_ |
32 | | Int_ !Int -- ~ constructor with 0 args | 38 | | Lam_ VarInfo !Exp |
33 | | Lam_ String{-for pretty print-} !Exp | 39 | | Let_ VarInfo !Exp !Exp |
34 | | Let_ String{-for pretty print-} !Exp !Exp | 40 | | Con_ ConInfo !Int [Exp] |
41 | | Case_ CaseInfo !Exp ![Exp] | ||
42 | | Lit_ !Lit | ||
35 | | Op1_ !Op1 !Exp | 43 | | Op1_ !Op1 !Exp |
36 | | Con_ String{-for pretty print-} !Int [Exp] | ||
37 | | Case_ [String]{-for pretty print-} !Exp ![Exp] -- TODO: simplify? | ||
38 | | Op2_ !Op2 !Exp !Exp | 44 | | Op2_ !Op2 !Exp !Exp |
39 | deriving (Eq, Show) | 45 | deriving (Eq, Show) |
40 | 46 | ||
41 | data Op1 = HNF_ | YOp | Round | 47 | data Op1 = HNFMark | YOp | Round |
42 | deriving (Eq, Show) | 48 | deriving (Eq, Show) |
43 | 49 | ||
44 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt | 50 | data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt |
45 | deriving (Eq, Show) | 51 | deriving (Eq, Show) |
46 | 52 | ||
53 | pattern Y a = Op1 YOp a | ||
54 | pattern App a b = Op2 AppOp a b | ||
55 | pattern Seq a b = Op2 SeqOp a b | ||
56 | pattern Int i = Lit (LInt i) | ||
57 | |||
58 | infixl 4 `App` | ||
59 | |||
47 | -- cached and compressed free variables set | 60 | -- cached and compressed free variables set |
48 | data Exp = Exp_ !FV !Exp_ | 61 | data Exp = Exp !FV !Exp_ |
49 | deriving (Eq, Show) | 62 | deriving (Eq, Show) |
50 | 63 | ||
51 | data EnvPiece | 64 | data EnvPiece |
52 | = ELet String{-for pretty print-} !Exp | 65 | = ELet VarInfo !Exp |
53 | | EDLet1 String{-for pretty print-} !DExp | 66 | | EDLet1 VarInfo !DExp |
54 | | ECase_ !FV ![String] ![Exp] | 67 | | ECase_ CaseInfo !FV ![Exp] |
55 | | EOp2_1 !Op2 !Exp | 68 | | EOp2_1 !Op2 !Exp |
56 | | EOp2_2 !Op2 !Exp | 69 | | EOp2_2 !Op2 !Exp |
57 | deriving (Eq, Show) | 70 | deriving (Eq, Show) |
@@ -70,30 +83,36 @@ data DEnv | |||
70 | data MSt = MSt !DEnv !Exp | 83 | data MSt = MSt !DEnv !Exp |
71 | deriving (Eq, Show) | 84 | deriving (Eq, Show) |
72 | 85 | ||
86 | --------- pretty print info | ||
87 | |||
88 | type VarInfo = String | ||
89 | type ConInfo = String | ||
90 | type CaseInfo = [(String, [String])] | ||
91 | |||
73 | --------------------------------------------------------------------- pattern synonyms | 92 | --------------------------------------------------------------------- pattern synonyms |
74 | 93 | ||
75 | infixr 4 `DEnvCons`, `DExpCons` | 94 | infixr 4 `DEnvCons`, `DExpCons` |
76 | 95 | ||
77 | pattern ECase op e <- ECase_ u op (map (upp u) -> e) | 96 | pattern ECase op e <- ECase_ op u (map (upp u) -> e) |
78 | where ECase op b = ECase_ u op bz where (u, bz) = deltas b | 97 | where ECase op b = ECase_ op u bz where (u, bz) = deltas b |
79 | 98 | ||
80 | pattern EnvPiece sfv p <- (getEnvPiece -> (sfv, p)) | 99 | pattern EnvPiece sfv p <- (getEnvPiece -> (sfv, p)) |
81 | where EnvPiece sfv@(SFV n u') = \case | 100 | where EnvPiece sfv@(SFV n u') = \case |
82 | EOp2_1 op e -> EOp2_1 op (uppS sfv e) | 101 | EOp2_1 op e -> EOp2_1 op (uppS sfv e) |
83 | EOp2_2 op e -> EOp2_2 op (uppS sfv e) | 102 | EOp2_2 op e -> EOp2_2 op (uppS sfv e) |
84 | ECase_ u s es -> ECase_ (expand u' u) s es | 103 | ECase_ s u es -> ECase_ s (expand u' u) es |
85 | ELet n (Exp_ u e) -> ELet n (Exp_ (sDrop 1 u' `expand` u) e) | 104 | ELet n (Exp u e) -> ELet n (Exp (sDrop 1 u' `expand` u) e) |
86 | EDLet1 n z -> EDLet1 n $ uppDE u' 1 z | 105 | EDLet1 n z -> EDLet1 n $ uppDE u' 1 z |
87 | 106 | ||
88 | getEnvPiece = \case | 107 | getEnvPiece = \case |
89 | EOp2_1 op (Exp_ u e) -> (SFV 0 u, EOp2_1 op (Exp_ (selfContract u) e)) | 108 | EOp2_1 op (Exp u e) -> (SFV 0 u, EOp2_1 op (Exp (selfContract u) e)) |
90 | EOp2_2 op (Exp_ u e) -> (SFV 0 u, EOp2_2 op (Exp_ (selfContract u) e)) | 109 | EOp2_2 op (Exp u e) -> (SFV 0 u, EOp2_2 op (Exp (selfContract u) e)) |
91 | ECase_ u s es -> (SFV 0 u, ECase_ (selfContract u) s es) | 110 | ECase_ s u es -> (SFV 0 u, ECase_ s (selfContract u) es) |
92 | ELet n (Exp_ u e) -> (SFV 1 $ fv 1 0 u, ELet n $ Exp_ (selfContract u) e) | 111 | ELet n (Exp u e) -> (SFV 1 $ fv 1 0 u, ELet n $ Exp (selfContract u) e) |
93 | EDLet1 n DExpNil -> (mempty, EDLet1 n DExpNil) | 112 | EDLet1 n DExpNil -> (mempty, EDLet1 n DExpNil) |
94 | EDLet1 n (DExpCons_ u x y) -> (SFV 0 $ sDrop 1 u, EDLet1 n $ DExpCons_ (onTail selfContract 1 u) x y) | 113 | EDLet1 n (DExpCons_ u x y) -> (SFV 0 $ sDrop 1 u, EDLet1 n $ DExpCons_ (onTail selfContract 1 u) x y) |
95 | 114 | ||
96 | uppS (SFV _ x) (Exp_ u a) = Exp_ (expand x u) a | 115 | uppS (SFV _ x) (Exp u a) = Exp (expand x u) a |
97 | 116 | ||
98 | pattern DExpCons :: EnvPiece -> DExp -> DExp | 117 | pattern DExpCons :: EnvPiece -> DExp -> DExp |
99 | pattern DExpCons a b <- (getDExpCons -> (a, b)) | 118 | pattern DExpCons a b <- (getDExpCons -> (a, b)) |
@@ -120,44 +139,38 @@ dDown i (DExpCons_ u a b) = DExpCons_ <$> downFV i u <*> pure a <*> pure b | |||
120 | 139 | ||
121 | --------------------------------------------------------------------- | 140 | --------------------------------------------------------------------- |
122 | 141 | ||
123 | pattern Int i <- Exp_ _ (Int_ i) | 142 | pattern Lit i <- Exp _ (Lit_ i) |
124 | where Int i = Exp_ mempty $ Int_ i | 143 | where Lit i = Exp mempty $ Lit_ i |
125 | pattern Op2 op a b <- Exp_ u (Op2_ op (upp u -> a) (upp u -> b)) | 144 | pattern Op2 op a b <- Exp u (Op2_ op (upp u -> a) (upp u -> b)) |
126 | where Op2 op a b = Exp_ s $ Op2_ op az bz where (s, az, bz) = delta2 a b | 145 | where Op2 op a b = Exp s $ Op2_ op az bz where (s, az, bz) = delta2 a b |
127 | pattern Op1 op a <- Exp_ u (Op1_ op (upp u -> a)) | 146 | pattern Op1 op a <- Exp u (Op1_ op (upp u -> a)) |
128 | where Op1 op (Exp_ ab x) = Exp_ ab $ Op1_ op $ Exp_ (selfContract ab) x | 147 | where Op1 op (Exp ab x) = Exp ab $ Op1_ op $ Exp (selfContract ab) x |
129 | pattern Var' i = Exp_ (VarFV i) Var_ | 148 | pattern Var' i = Exp (VarFV i) Var_ |
130 | pattern Var i = Var' i | 149 | pattern Var i = Var' i |
131 | pattern Lam n i <- Exp_ u (Lam_ n (upp (incFV u) -> i)) | 150 | pattern Lam n i <- Exp u (Lam_ n (upp (incFV u) -> i)) |
132 | where Lam n (Exp_ vs ax) = Exp_ (sDrop 1 vs) $ Lam_ n $ Exp_ (compact vs) ax | 151 | where Lam n (Exp vs ax) = Exp (sDrop 1 vs) $ Lam_ n $ Exp (compact vs) ax |
133 | pattern Con a b i <- Exp_ u (Con_ a b (map (upp u) -> i)) | 152 | pattern Con a b i <- Exp u (Con_ a b (map (upp u) -> i)) |
134 | where Con a b x = Exp_ s $ Con_ a b bz where (s, bz) = deltas x | 153 | where Con a b x = Exp s $ Con_ a b bz where (s, bz) = deltas x |
135 | pattern Case a b c <- Exp_ u (Case_ a (upp u -> b) (map (upp u) -> c)) | 154 | pattern Case a b c <- Exp u (Case_ a (upp u -> b) (map (upp u) -> c)) |
136 | where Case cn a b = Exp_ s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b | 155 | where Case cn a b = Exp s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b |
137 | 156 | ||
138 | pattern Let n i x <- Exp_ u (Let_ n (upp u -> i) (upp (incFV u) -> x)) | 157 | pattern Let n i x <- Exp u (Let_ n (upp u -> i) (upp (incFV u) -> x)) |
139 | where Let _ _ (down 0 -> Just x) = x | 158 | where Let _ _ (down 0 -> Just x) = x |
140 | Let n a b = Exp_ s (Let_ n a' b') where (s, a', Lam _ b') = delta2 a $ Lam n b | 159 | Let n a b = Exp s (Let_ n a' b') where (s, a', Lam _ b') = delta2 a $ Lam n b |
141 | 160 | ||
142 | pattern InHNF a <- (getHNF -> Just a) | 161 | pattern InHNF a <- (getHNF -> Just a) |
143 | where InHNF a@Int{} = a | 162 | where InHNF a@Lit{} = a |
144 | InHNF a@Lam{} = a | 163 | InHNF a@Lam{} = a |
145 | InHNF a@(Op1 HNF_ _) = a | 164 | InHNF a@(Op1 HNFMark _) = a |
146 | InHNF a = Op1 HNF_ a | 165 | InHNF a = Op1 HNFMark a |
147 | 166 | ||
148 | getHNF x = case x of | 167 | getHNF x = case x of |
149 | Int{} -> Just x | 168 | Lit{} -> Just x |
150 | Lam{} -> Just x | 169 | Lam{} -> Just x |
151 | Op1 HNF_ a -> Just a | 170 | Op1 HNFMark a -> Just a |
152 | _ -> Nothing | 171 | _ -> Nothing |
153 | 172 | ||
154 | pattern Y a = Op1 YOp a | 173 | delta2 (Exp ua a) (Exp ub b) = (s, Exp ua' a, Exp ub' b) |
155 | pattern App a b = Op2 AppOp a b | ||
156 | pattern Seq a b = Op2 SeqOp a b | ||
157 | |||
158 | infixl 4 `App` | ||
159 | |||
160 | delta2 (Exp_ ua a) (Exp_ ub b) = (s, Exp_ ua' a, Exp_ ub' b) | ||
161 | where | 174 | where |
162 | (s, ua', ub') = delta2' ua ub | 175 | (s, ua', ub') = delta2' ua ub |
163 | 176 | ||
@@ -166,30 +179,30 @@ delta2' ua ub = (s, primContract s ua, primContract s ub) | |||
166 | s = ua <> ub | 179 | s = ua <> ub |
167 | 180 | ||
168 | deltas [] = (mempty, []) | 181 | deltas [] = (mempty, []) |
169 | deltas [Exp_ x e] = (x, [Exp_ (selfContract x) e]) | 182 | deltas [Exp x e] = (x, [Exp (selfContract x) e]) |
170 | deltas [Exp_ ua a, Exp_ ub b] = (s, [Exp_ (primContract s ua) a, Exp_ (primContract s ub) b]) | 183 | deltas [Exp ua a, Exp ub b] = (s, [Exp (primContract s ua) a, Exp (primContract s ub) b]) |
171 | where | 184 | where |
172 | s = ua <> ub | 185 | s = ua <> ub |
173 | deltas es = (s, [Exp_ (primContract s u) e | (u, Exp_ _ e) <- zip xs es]) | 186 | deltas es = (s, [Exp (primContract s u) e | (u, Exp _ e) <- zip xs es]) |
174 | where | 187 | where |
175 | xs = [ue | Exp_ ue _ <- es] | 188 | xs = [ue | Exp ue _ <- es] |
176 | 189 | ||
177 | s = mconcat xs | 190 | s = mconcat xs |
178 | 191 | ||
179 | upp :: FV -> Exp -> Exp | 192 | upp :: FV -> Exp -> Exp |
180 | upp a (Exp_ b e) = Exp_ (expand a b) e | 193 | upp a (Exp b e) = Exp (expand a b) e |
181 | 194 | ||
182 | up l n (Exp_ us x) = Exp_ (upFV l n us) x | 195 | up l n (Exp us x) = Exp (upFV l n us) x |
183 | 196 | ||
184 | -- free variables set | 197 | -- free variables set |
185 | fvs (Exp_ us _) = usedFVs us | 198 | --fvs (Exp us _) = usedFVs us |
186 | 199 | ||
187 | usedVar i (Exp_ us _) = sIndex us i | 200 | usedVar i (Exp us _) = sIndex us i |
188 | 201 | ||
189 | usedVar' i DExpNil = False | 202 | usedVar' i DExpNil = False |
190 | usedVar' i (DExpCons_ u _ _) = sIndex u i | 203 | usedVar' i (DExpCons_ u _ _) = sIndex u i |
191 | 204 | ||
192 | down i (Exp_ us e) = Exp_ <$> downFV i us <*> pure e | 205 | down i (Exp us e) = Exp <$> downFV i us <*> pure e |
193 | 206 | ||
194 | --------------------------- | 207 | --------------------------- |
195 | 208 | ||
@@ -199,29 +212,33 @@ initSt e = MSt DEnvNil e | |||
199 | ----------------------------------------------------------- machine code begins here | 212 | ----------------------------------------------------------- machine code begins here |
200 | 213 | ||
201 | justResult :: MSt -> MSt | 214 | justResult :: MSt -> MSt |
202 | justResult = steps 0 id (const ($)) (const (.)) | 215 | justResult st = steps st (\_ s -> justResult s) st |
203 | 216 | ||
204 | hnf = justResult . initSt | 217 | hnf = justResult . initSt |
205 | 218 | ||
206 | ---------------- | 219 | ---------------- |
207 | 220 | ||
221 | data StepTag = Begin String | End String | Step String | ||
222 | deriving Show | ||
223 | |||
208 | type GenSteps e | 224 | type GenSteps e |
209 | = (MSt -> e) | 225 | = e |
210 | -> (StepTag -> (MSt -> e) -> MSt -> e) | 226 | -> (StepTag -> MSt -> e) |
211 | -> (StepTag -> (MSt -> e) -> (MSt -> e) -> MSt -> e) | ||
212 | -> MSt -> e | 227 | -> MSt -> e |
213 | 228 | ||
214 | type StepTag = String | ||
215 | |||
216 | focusNotUsed (MSt (EDLet1 _ x `DEnvCons` _) _) = not $ usedVar' 0 x | 229 | focusNotUsed (MSt (EDLet1 _ x `DEnvCons` _) _) = not $ usedVar' 0 x |
217 | focusNotUsed _ = True | 230 | focusNotUsed _ = True |
218 | 231 | ||
219 | steps :: forall e . Int -> GenSteps e | 232 | inHNF :: MSt -> Bool |
220 | steps lev nostep bind cont (MSt vs e) = case e of | 233 | inHNF (MSt _ (InHNF _)) = True |
234 | inHNF _ = False | ||
235 | |||
236 | steps :: forall e . GenSteps e | ||
237 | steps nostep bind (MSt vs e) = case e of | ||
221 | 238 | ||
222 | Con cn i xs | 239 | Con cn i xs |
223 | | lz == 0 || focusNotUsed (MSt vs e) -> step "con hnf" $ MSt vs $ InHNF e | 240 | | lz == 0 || focusNotUsed (MSt vs e) -> step (cn ++ " hnf") $ MSt vs $ InHNF e |
224 | | otherwise -> step "copy con" $ MSt (foldr DEnvCons vs $ ELet "" <$> zs) $ InHNF $ Con cn i xs' -- share complex constructor arguments | 241 | | otherwise -> step (cn ++ " copy") $ MSt (foldr DEnvCons vs $ ELet "" <$> zs) $ InHNF $ Con cn i xs' -- share complex constructor arguments |
225 | where | 242 | where |
226 | lz = Nat $ length zs | 243 | lz = Nat $ length zs |
227 | (xs', concat -> zs) = unzip $ f 0 xs | 244 | (xs', concat -> zs) = unzip $ f 0 xs |
@@ -232,40 +249,39 @@ steps lev nostep bind cont (MSt vs e) = case e of | |||
232 | -- TODO: handle recursive constants | 249 | -- TODO: handle recursive constants |
233 | Y x -> step "Y" $ MSt vs $ App x (Y x) | 250 | Y x -> step "Y" $ MSt vs $ App x (Y x) |
234 | 251 | ||
235 | Var i -> step "var" $ zipDown i DExpNil vs | 252 | Var i -> begin "var" $ zipDown i DExpNil vs |
236 | Seq a b -> step "seq" $ MSt (EOp2_1 SeqOp b `DEnvCons` vs) a | 253 | Case cns a cs -> begin "case" $ MSt (ECase cns cs `DEnvCons` vs) a |
237 | Case cns a cs -> step "case" $ MSt (ECase cns cs `DEnvCons` vs) a | 254 | Op2 op a b -> begin (show op) $ MSt (EOp2_1 op b `DEnvCons` vs) a |
238 | Op2 op a b -> step "op2_1" $ MSt (EOp2_1 op b `DEnvCons` vs) a | ||
239 | 255 | ||
240 | InHNF a -> case vs of | 256 | InHNF a -> case vs of |
241 | 257 | ||
242 | DEnvNil -> bind "whnf" nostep $ MSt DEnvNil $ InHNF a | 258 | DEnvNil -> nostep |
243 | 259 | ||
244 | ELet n x `DEnvCons` vs -> step "goUp" $ MSt vs $ InHNF $ Let n x $ InHNF a | 260 | ELet n x `DEnvCons` vs -> step "goUp" $ MSt vs $ InHNF $ Let n x $ InHNF a |
245 | x `DEnvCons` vs | Let n y e <- a -> step "pakol" $ MSt (upP 0 1 x `DEnvCons` ELet n y `DEnvCons` vs) e | 261 | x `DEnvCons` vs | Let n y e <- a -> step "pakol" $ MSt (upP 0 1 x `DEnvCons` ELet n y `DEnvCons` vs) e |
246 | x `DEnvCons` vs -> case x of | 262 | x `DEnvCons` vs -> case x of |
247 | EOp2_1 SeqOp b -> case a of | 263 | ECase cns cs -> end "case" $ case a of |
248 | Int{} -> step "seq" $ MSt vs b | 264 | Con cn i es -> MSt vs $ foldl App (cs !! i) es -- TODO: remove unused cases |
249 | Lam{} -> step "seq" $ MSt vs b -- TODO: remove a | 265 | _ -> MSt vs $ InHNF $ Case cns (InHNF a) cs |
250 | Con{} -> step "seq" $ MSt vs b -- TODO: remove a | 266 | EOp2_1 AppOp b -> end "AppOp" $ case a of |
251 | _ -> step "seq hnf" $ MSt vs $ InHNF $ Seq (InHNF a) b | 267 | Lam _ (down 0 -> Just x) -> MSt vs x -- TODO: remove b |
252 | ECase cns cs -> case a of | 268 | Lam n x -> MSt (ELet n b `DEnvCons` vs) x |
253 | Con cn i es -> step "case" $ MSt vs $ foldl App (cs !! i) es -- TODO: remove unused cases | 269 | _ -> MSt vs $ InHNF $ App (InHNF a) b |
254 | _ -> step "case hnf" $ MSt vs $ InHNF $ Case cns (InHNF a) cs | 270 | EOp2_1 SeqOp b -> end "SeqOp" $ case a of |
255 | EOp2_1 AppOp b -> case a of | 271 | Lit{} -> MSt vs b |
256 | Lam _ (down 0 -> Just x) -> step "appdel" $ MSt vs x -- TODO: remove b | 272 | Lam{} -> MSt vs b -- TODO: remove a |
257 | Lam n x -> step "app" $ MSt (ELet n b `DEnvCons` vs) x | 273 | Con{} -> MSt vs b -- TODO: remove a |
258 | _ -> step "app hnf" $ MSt vs $ InHNF $ App (InHNF a) b | 274 | _ -> MSt vs $ InHNF $ Seq (InHNF a) b |
259 | EOp2_1 op b -> step "op2_2 hnf" $ MSt (EOp2_2 op (InHNF a) `DEnvCons` vs) b | 275 | EOp2_1 op b -> next (show op) $ MSt (EOp2_2 op (InHNF a) `DEnvCons` vs) b |
260 | EOp2_2 op b -> case (b, a) of | 276 | EOp2_2 op b -> end (show op) $ case (b, a) of |
261 | (Int e, Int f) -> step "op-done" $ MSt vs (int op e f) | 277 | (Int e, Int f) -> MSt vs (int op e f) |
262 | where | 278 | where |
263 | int Add a b = Int $ a + b | 279 | int Add a b = Int $ a + b |
264 | int Sub a b = Int $ a - b | 280 | int Sub a b = Int $ a - b |
265 | int Mod a b = Int $ a `mod` b | 281 | int Mod a b = Int $ a `mod` b |
266 | int LessEq a b = if a <= b then T else F | 282 | int LessEq a b = if a <= b then T else F |
267 | int EqInt a b = if a == b then T else F | 283 | int EqInt a b = if a == b then T else F |
268 | _ -> step "op2 hnf" $ MSt vs $ InHNF $ Op2 op b (InHNF a) | 284 | _ -> MSt vs $ InHNF $ Op2 op b (InHNF a) |
269 | EDLet1 _ (dDown 0 -> Just d) -> zipUp (InHNF a) vs d | 285 | EDLet1 _ (dDown 0 -> Just d) -> zipUp (InHNF a) vs d |
270 | EDLet1 n d -> zipUp (up 0 1 a) (ELet n (InHNF a) `DEnvCons` vs) d | 286 | EDLet1 n d -> zipUp (up 0 1 a) (ELet n (InHNF a) `DEnvCons` vs) d |
271 | 287 | ||
@@ -274,55 +290,56 @@ steps lev nostep bind cont (MSt vs e) = case e of | |||
274 | zipDown j e (z@ELet{} `DEnvCons` zs) = zipDown (j-1) (z `DExpCons` e) zs | 290 | zipDown j e (z@ELet{} `DEnvCons` zs) = zipDown (j-1) (z `DExpCons` e) zs |
275 | zipDown j e (z `DEnvCons` zs) = zipDown j (z `DExpCons` e) zs | 291 | zipDown j e (z `DEnvCons` zs) = zipDown j (z `DExpCons` e) zs |
276 | 292 | ||
277 | zipUp x xs DExpNil = step "zipUp ready" $ MSt xs x | 293 | zipUp x xs DExpNil = end "var" $ MSt xs x |
278 | zipUp x xs (DExpCons a@ELet{} as) = zipUp (up 0 1 x) (a `DEnvCons` xs) as | 294 | zipUp x xs (DExpCons a@ELet{} as) = zipUp (up 0 1 x) (a `DEnvCons` xs) as |
279 | zipUp x xs (DExpCons a as) = zipUp x (a `DEnvCons` xs) as | 295 | zipUp x xs (DExpCons a as) = zipUp x (a `DEnvCons` xs) as |
280 | 296 | ||
281 | rec i = steps i nostep bind cont | 297 | begin t = bind (Begin t) |
282 | 298 | next t = bind (Step t) | |
283 | step :: StepTag -> MSt -> e | 299 | end t = bind (End t) |
284 | step t = bind t (rec lev) | 300 | step t = bind (Step t) |
285 | {- | ||
286 | hnf :: StepTag -> (MSt -> e) -> MSt -> e | ||
287 | hnf t f = bind ("hnf " ++ t) $ cont t f (rec (1 + lev)) | ||
288 | |||
289 | hnf' :: StepTag -> MSt -> e | ||
290 | hnf' t = hnf t $ bind ("focus " ++ t) $ goUp t 0 | ||
291 | -} | ||
292 | 301 | ||
293 | simple = \case | 302 | simple = \case |
294 | Var{} -> True | 303 | Var{} -> True |
295 | Int{} -> True | 304 | Lit{} -> True |
296 | _ -> False | 305 | _ -> False |
297 | 306 | ||
298 | delElem i xs = take i xs ++ drop (i+1) xs | 307 | delElem i xs = take i xs ++ drop (i+1) xs |
299 | 308 | ||
300 | --------------------------------------------------------------------- toolbox: pretty print | 309 | --------------------------------------------------------------------- toolbox: pretty print |
301 | 310 | ||
311 | instance PShow Lit where | ||
312 | pShow (LInt i) = pShow i | ||
313 | |||
314 | instance Show Lit where show = ppShow | ||
315 | |||
302 | class ViewShow a where | 316 | class ViewShow a where |
303 | viewShow :: Bool -> a -> Doc | 317 | viewShow :: Bool -> a -> Doc |
304 | 318 | ||
305 | instance ViewShow Exp where | 319 | instance ViewShow Exp where |
306 | viewShow vi = pShow where | 320 | viewShow vi = pShow where |
307 | pShow e@(Exp_ fv x) = showFE green vi fv $ | 321 | pShow e@(Exp fv x) = showFE green vi fv $ |
308 | case {-if vi then Exp_ (selfContract fv) x else-} e of | 322 | case {-if vi then Exp_ (selfContract fv) x else-} e of |
309 | Var (Nat i) -> DVar i | 323 | Var (Nat i) -> DVar i |
310 | Let n a b -> shLet n (pShow a) $ pShow b | 324 | Let n a b -> shLet n (pShow a) $ pShow b |
311 | Lam n e -> shLam n $ pShow e | 325 | Lam n e -> shLam n $ pShow e |
312 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs | 326 | Con s i xs -> foldl DApp (text s) $ pShow <$> xs |
313 | Int i -> pShow' i | 327 | Lit i -> pShow' i |
314 | Y e -> "Y" `DApp` pShow e | 328 | Y e -> "Y" `DApp` pShow e |
315 | InHNF x -> DBrace (pShow x) | 329 | InHNF x -> DBrace (pShow x) |
316 | Op1 o x -> text (show o) `DApp` pShow x | 330 | Op1 o x -> text (show o) `DApp` pShow x |
317 | Op2 o x y -> shOp2 o (pShow x) (pShow y) | 331 | Op2 o x y -> shOp2 o (pShow x) (pShow y) |
318 | Case cn e xs -> shCase cn (pShow e) (pShow <$> xs) | 332 | Case cn e xs -> shCase cn (pShow e) pShow xs |
319 | Exp_ u Var_ -> onblue $ pShow' u | 333 | -- Exp_ u Var_ -> onblue $ pShow' u |
320 | e -> error $ "pShow @Exp: " ++ show e | 334 | e -> error $ "pShow @Exp: " ++ show e |
321 | 335 | ||
322 | glueTo = DGlue (InfixR 40) | 336 | glueTo = DGlue (InfixR 40) |
323 | 337 | ||
324 | shCase cn e xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of")) | 338 | app_ (Lam _ x) _ = x |
325 | $ foldr1 DSemi [DArr_ "->" (text a) b | (a, b) <- zip cn xs] | 339 | app_ x y = App x y |
340 | |||
341 | shCase cn e f xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of")) | ||
342 | $ foldr1 DSemi [foldr DFreshName (DArr_ "->" (foldl DApp (text a) $ DVar <$> reverse [0..length n - 1]) (f $ foldl app_ b $ Var . Nat <$> [0..length n - 1])) $ Just <$> n | ((a, n), b) <- zip cn xs] | ||
326 | 343 | ||
327 | shOp2 AppOp x y = DApp x y | 344 | shOp2 AppOp x y = DApp x y |
328 | shOp2 SeqOp a b = DOp "`seq`" (Infix 1) a b | 345 | shOp2 SeqOp a b = DOp "`seq`" (Infix 1) a b |
@@ -341,21 +358,25 @@ instance ViewShow MSt where | |||
341 | pShow = viewShow vi | 358 | pShow = viewShow vi |
342 | 359 | ||
343 | g y DEnvNil = y | 360 | g y DEnvNil = y |
344 | g y z@(DEnvCons p env) = flip g env $ {-showFE red vi (case p of EnvPiece f _ -> f) $-} case p of | 361 | g y z@(DEnvCons p env) = flip g env $ case p of |
345 | EDLet1 n x -> shLet n y (h x) | 362 | EDLet1 n x -> shLet n y (h 0 x) |
346 | ELet n x -> shLet n (pShow x) y | 363 | ELet n x -> shLet n (pShow x) y |
347 | ECase cns xs -> shCase cns y (pShow <$> xs) | 364 | ECase cns xs -> shCase cns y pShow xs |
348 | EOp2_1 op x -> shOp2 op y (pShow x) | 365 | EOp2_1 op x -> shOp2 op y (pShow x) |
349 | EOp2_2 op x -> shOp2 op (pShow x) y | 366 | EOp2_2 op x -> shOp2 op (pShow x) y |
350 | 367 | ||
351 | h DExpNil = onred $ white "*" --TODO? | 368 | h n DExpNil = onred $ white $ DVar n |
352 | h z@(DExpCons p (h -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of | 369 | h n z@(DExpCons p (h (adj p n) -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of |
353 | EDLet1 n x -> shLet n y (h x) | 370 | EDLet1 n x -> shLet n y (h 0 x) |
354 | ELet n x -> shLet n (pShow x) y | 371 | ELet n x -> shLet n (pShow x) y |
355 | ECase cns xs -> shCase cns y (pShow <$> xs) | 372 | ECase cns xs -> shCase cns y pShow xs |
356 | EOp2_1 op x -> shOp2 op y (pShow x) | 373 | EOp2_1 op x -> shOp2 op y (pShow x) |
357 | EOp2_2 op x -> shOp2 op (pShow x) y | 374 | EOp2_2 op x -> shOp2 op (pShow x) y |
358 | 375 | ||
376 | adj p n = case p of | ||
377 | ELet{} -> n + 1 | ||
378 | _ -> n | ||
379 | |||
359 | instance PShow MSt where pShow = viewShow False | 380 | instance PShow MSt where pShow = viewShow False |
360 | 381 | ||
361 | 382 | ||
@@ -386,8 +407,8 @@ pattern T = Con "True" 1 [] | |||
386 | pattern Nil = Con "[]" 0 [] | 407 | pattern Nil = Con "[]" 0 [] |
387 | pattern Cons a b = Con "Cons" 1 [a, b] | 408 | pattern Cons a b = Con "Cons" 1 [a, b] |
388 | 409 | ||
389 | caseBool x f t = Case ["False", "True"] x [f, t] | 410 | caseBool x f t = Case [("False", []), ("True", [])] x [f, t] |
390 | caseList x n c = Case ["[]", "Cons"] x [n, c] | 411 | caseList x n c = Case [("[]", []), ("Cons", ["c", "cs"])] x [n, c] |
391 | 412 | ||
392 | id_ = Lam "x" (Var 0) | 413 | id_ = Lam "x" (Var 0) |
393 | 414 | ||
@@ -455,7 +476,7 @@ inc = Lam "n" $ Op2 Add (Var 0) (Int 1) | |||
455 | 476 | ||
456 | test'' = Lam "f" (Int 4) `App` Int 3 | 477 | test'' = Lam "f" (Int 4) `App` Int 3 |
457 | 478 | ||
458 | twiceTest = twice `App` twice `App` twice `App` twice `App` inc `App` Int 0 | 479 | twiceTest n = (Lam "twice" $ (iterate (`App` Var 0) (Var 0) !! n) `App` inc `App` Int 0) `App` twice |
459 | twiceTest2 = twice2 `App` twice2 `App` twice2 `App` twice2 `App` inc `App` Int 0 | 480 | twiceTest2 = twice2 `App` twice2 `App` twice2 `App` twice2 `App` inc `App` Int 0 |
460 | 481 | ||
461 | tests | 482 | tests |