Mercurial > urweb

comparison src/unnest.sml @ 453:787d4931fb07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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