Mercurial > urweb
comparison src/unnest.sml @ 453:787d4931fb07
Almost have that nested save function compiling
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 01 Nov 2008 21:19:43 -0400 |
parents | 07f6576aeb0a |
children | d4a81273d4b1 |
comparison
equal
deleted
inserted
replaced
452:222cbc1da232 | 453:787d4931fb07 |
---|---|
122 | _ => c, | 122 | _ => c, |
123 exp = fn (cb, eb) => fn e => | 123 exp = fn (cb, eb) => fn e => |
124 case e of | 124 case e of |
125 ERel n => | 125 ERel n => |
126 if n >= eb then | 126 if n >= eb then |
127 ERel (positionOf (n - eb) efv + eb) | 127 ERel (positionOf (n - eb) efv + eb) |
128 else | 128 else |
129 e | 129 e |
130 | _ => e, | 130 | _ => e, |
131 bind = fn (ctx as (cb, eb), b) => | 131 bind = fn (ctx as (cb, eb), b) => |
132 case b of | 132 case b of |
140 decls : decl list | 140 decls : decl list |
141 } | 141 } |
142 | 142 |
143 fun kind (k, st) = (k, st) | 143 fun kind (k, st) = (k, st) |
144 | 144 |
145 fun exp ((ks, ts), e, st : state) = | 145 fun exp ((ks, ts), e as old, st : state) = |
146 case e of | 146 case e of |
147 ELet (eds, e) => | 147 ELet (eds, e) => |
148 let | 148 let |
149 (*val () = Print.prefaces "let" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) | |
150 | |
149 val doSubst = foldl (fn (p, e) => E.subExpInExp p e) | 151 val doSubst = foldl (fn (p, e) => E.subExpInExp p e) |
150 | 152 |
151 val (eds, (maxName, ds, subs)) = | 153 val (eds, (ts, maxName, ds, subs)) = |
152 ListUtil.foldlMapConcat | 154 ListUtil.foldlMapConcat |
153 (fn (ed, (maxName, ds, subs)) => | 155 (fn (ed, (ts, maxName, ds, subs)) => |
154 case #1 ed of | 156 case #1 ed of |
155 EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) | 157 EDVal (x, t, _) => ([ed], |
158 ((x, t) :: ts, | |
159 maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) | |
156 | EDValRec vis => | 160 | EDValRec vis => |
157 let | 161 let |
158 val loc = #2 ed | 162 val loc = #2 ed |
159 | 163 |
160 val nr = length vis | 164 val nr = length vis |
172 (IS.union (cfv, IS.union (cfv', cfv'')), | 176 (IS.union (cfv, IS.union (cfv', cfv'')), |
173 IS.union (efv, efv')) | 177 IS.union (efv, efv')) |
174 end) | 178 end) |
175 (IS.empty, IS.empty) vis | 179 (IS.empty, IS.empty) vis |
176 | 180 |
177 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) | 181 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n") |
182 val () = app (fn (x, t) => | |
183 Print.prefaces "Var" [("x", Print.PD.string x), | |
184 ("t", ElabPrint.p_con E.empty t)]) ts*) | |
178 val cfv = IS.foldl (fn (x, cfv) => | 185 val cfv = IS.foldl (fn (x, cfv) => |
179 let | 186 let |
180 (*val () = print (Int.toString x ^ "\n")*) | 187 (*val () = print (Int.toString x ^ "\n")*) |
181 val (_, t) = List.nth (ts, x) | 188 val (_, t) = List.nth (ts, x) |
182 in | 189 in |
191 maxName + 1)) | 198 maxName + 1)) |
192 maxName vis | 199 maxName vis |
193 | 200 |
194 fun apply e = | 201 fun apply e = |
195 let | 202 let |
196 val e = IS.foldl (fn (x, e) => | 203 val e = IS.foldr (fn (x, e) => |
197 (ECApp (e, (CRel x, loc)), loc)) | 204 (ECApp (e, (CRel x, loc)), loc)) |
198 e cfv | 205 e cfv |
199 in | 206 in |
200 IS.foldl (fn (x, e) => | 207 IS.foldr (fn (x, e) => |
201 (EApp (e, (ERel x, loc)), loc)) | 208 (EApp (e, (ERel x, loc)), loc)) |
202 e efv | 209 e efv |
203 end | 210 end |
204 | 211 |
205 val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs | 212 val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs |
235 (*val () = Print.prefaces "squishCon" | 242 (*val () = Print.prefaces "squishCon" |
236 [("t", ElabPrint.p_con E.empty t)]*) | 243 [("t", ElabPrint.p_con E.empty t)]*) |
237 val t = squishCon cfv t | 244 val t = squishCon cfv t |
238 (*val () = Print.prefaces "squishExp" | 245 (*val () = Print.prefaces "squishExp" |
239 [("e", ElabPrint.p_exp E.empty e)]*) | 246 [("e", ElabPrint.p_exp E.empty e)]*) |
240 val e = squishExp (nr, cfv, efv) e | 247 val e = squishExp (0(*nr*), cfv, efv) e |
241 | 248 |
242 val (e, t) = foldr (fn (ex, (e, t)) => | 249 val (e, t) = foldl (fn (ex, (e, t)) => |
243 let | 250 let |
244 val (name, t') = List.nth (ts, ex) | 251 val (name, t') = List.nth (ts, ex) |
245 in | 252 in |
246 ((EAbs (name, | 253 ((EAbs (name, |
247 t', | 254 t', |
250 (TFun (t', | 257 (TFun (t', |
251 t), loc)) | 258 t), loc)) |
252 end) | 259 end) |
253 (e, t) efv | 260 (e, t) efv |
254 | 261 |
255 val (e, t) = foldr (fn (cx, (e, t)) => | 262 val (e, t) = foldl (fn (cx, (e, t)) => |
256 let | 263 let |
257 val (name, k) = List.nth (ks, cx) | 264 val (name, k) = List.nth (ks, cx) |
258 in | 265 in |
259 ((ECAbs (Explicit, | 266 ((ECAbs (Explicit, |
260 name, | 267 name, |
270 (x, n, t, e) | 277 (x, n, t, e) |
271 end) | 278 end) |
272 vis | 279 vis |
273 | 280 |
274 val d = (DValRec vis, #2 ed) | 281 val d = (DValRec vis, #2 ed) |
282 | |
283 val ts = map (fn (x, _, t, _) => (x, t)) vis @ ts | |
275 in | 284 in |
276 ([], (maxName, d :: ds, subs)) | 285 ([], (ts, maxName, d :: ds, subs)) |
277 end) | 286 end) |
278 (#maxName st, #decls st, []) eds | 287 (ts, #maxName st, #decls st, []) eds |
279 in | 288 in |
280 (ELet (eds, doSubst e subs), | 289 (ELet (eds, doSubst e subs), |
281 {maxName = maxName, | 290 {maxName = maxName, |
282 decls = ds}) | 291 decls = ds}) |
283 end | 292 end |