Mercurial > urweb
comparison src/unnest.sml @ 825:7f871c03e3a1
Destructing local let, to the point where demo compiles
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 28 May 2009 12:07:05 -0400 |
parents | 8688e01ae469 |
children | 78504d97410b |
comparison
equal
deleted
inserted
replaced
824:be0988e46336 | 825:7f871c03e3a1 |
---|---|
171 | 171 |
172 fun kind (_, k, st) = (k, st) | 172 fun kind (_, k, st) = (k, st) |
173 | 173 |
174 fun exp ((ks, ts), e as old, st : state) = | 174 fun exp ((ks, ts), e as old, st : state) = |
175 case e of | 175 case e of |
176 ELet (eds, e) => | 176 ELet (eds, e, t) => |
177 let | 177 let |
178 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) | 178 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) |
179 | 179 |
180 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs | 180 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs |
181 | 181 |
188 | 188 |
189 val (eds, (ts, maxName, ds, subs, by)) = | 189 val (eds, (ts, maxName, ds, subs, by)) = |
190 ListUtil.foldlMapConcat | 190 ListUtil.foldlMapConcat |
191 (fn (ed, (ts, maxName, ds, subs, by)) => | 191 (fn (ed, (ts, maxName, ds, subs, by)) => |
192 case #1 ed of | 192 case #1 ed of |
193 EDVal (x, t, e) => | 193 EDVal (p, t, e) => |
194 let | 194 let |
195 val e = doSubst (e, subs, by) | 195 val e = doSubst (e, subs, by) |
196 | |
197 fun doVars ((p, _), ts) = | |
198 case p of | |
199 PWild => ts | |
200 | PVar xt => xt :: ts | |
201 | PPrim _ => ts | |
202 | PCon (_, _, _, NONE) => ts | |
203 | PCon (_, _, _, SOME p) => doVars (p, ts) | |
204 | PRecord xpcs => | |
205 foldl (fn ((_, p, _), ts) => doVars (p, ts)) | |
206 ts xpcs | |
196 in | 207 in |
197 ([(EDVal (x, t, e), #2 ed)], | 208 ([(EDVal (p, t, e), #2 ed)], |
198 ((x, t) :: ts, | 209 (doVars (p, ts), |
199 maxName, ds, | 210 maxName, ds, |
200 ((0, (ERel 0, #2 ed)) | 211 ((0, (ERel 0, #2 ed)) |
201 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), | 212 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), |
202 by)) | 213 by)) |
203 end | 214 end |
339 val e' = doSubst (e, subs, by) | 350 val e' = doSubst (e, subs, by) |
340 in | 351 in |
341 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), | 352 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), |
342 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), | 353 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), |
343 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) | 354 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) |
344 (ELet (eds, e'), | 355 (ELet (eds, e', t), |
345 {maxName = maxName, | 356 {maxName = maxName, |
346 decls = ds}) | 357 decls = ds}) |
347 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*) | 358 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*) |
348 end | 359 end |
349 | 360 |