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