Mercurial > urweb

comparison src/elab_env.sml @ 34:44b5405e74c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating module projection
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 16:38:54 -0400
parents 1c91c5e6840f
children 1405d8c26790
comparison
equal deleted inserted replaced
33:535c324f0b35 34:44b5405e74c7
296 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 296 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
297 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 297 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
298 | SgiVal (x, n, t) => pushENamedAs env x n t 298 | SgiVal (x, n, t) => pushENamedAs env x n t
299 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 299 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
300 300
301 fun sgnSeek f sgis =
302 let
303 fun seek (sgis, strs, cons) =
304 case sgis of
305 [] => NONE
306 | (sgi, _) :: sgis =>
307 case f sgi of
308 SOME v => SOME (v, (strs, cons))
309 | NONE =>
310 case sgi of
311 SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x))
312 | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x))
313 | SgiVal _ => seek (sgis, strs, cons)
314 | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons)
315 in
316 seek (sgis, IM.empty, IM.empty)
317 end
318
319 fun id x = x
320
321 fun unravelStr (str, _) =
322 case str of
323 StrVar x => (x, [])
324 | StrProj (str, m) =>
325 let
326 val (x, ms) = unravelStr str
327 in
328 (x, ms @ [m])
329 end
330 | _ => raise Fail "unravelStr"
331
332 fun sgnS_con (str, (strs, cons)) c =
333 case c of
334 CModProj (m1, ms, x) =>
335 (case IM.find (strs, m1) of
336 NONE => c
337 | SOME m1x =>
338 let
339 val (m1, ms') = unravelStr str
340 in
341 CModProj (m1, ms' @ m1x :: ms, x)
342 end)
343 | CNamed n =>
344 (case IM.find (cons, n) of
345 NONE => c
346 | SOME nx =>
347 let
348 val (m1, ms) = unravelStr str
349 in
350 CModProj (m1, ms, nx)
351 end)
352 | _ => c
353
354 fun sgnSubCon (str, (strs, cons)) =
355 ElabUtil.Con.map {kind = id,
356 con = sgnS_con (str, (strs, cons))}
357
358 fun sgnSubSgn (str, (strs, cons)) =
359 ElabUtil.Sgn.map {kind = id,
360 con = sgnS_con (str, (strs, cons)),
361 sgn_item = id,
362 sgn = id}
363
364 fun projectCon env {sgn = (sgn, _), str, field} =
365 case sgn of
366 SgnConst sgis =>
367 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
368 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
369 | _ => NONE) sgis of
370 NONE => NONE
371 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
372 | SgnVar n =>
373 let
374 val (_, sgn) = lookupSgnNamed env n
375 in
376 projectCon env {sgn = sgn, str = str, field = field}
377 end
378 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
379
380 fun projectVal env {sgn = (sgn, _), str, field} =
381 case sgn of
382 SgnConst sgis =>
383 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
384 NONE => NONE
385 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
386 | SgnVar n =>
387 let
388 val (_, sgn) = lookupSgnNamed env n
389 in
390 projectVal env {sgn = sgn, str = str, field = field}
391 end
392 | SgnError => SOME (CError, ErrorMsg.dummySpan)
393
394 fun projectStr env {sgn = (sgn, _), str, field} =
395 case sgn of
396 SgnConst sgis =>
397 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
398 NONE => NONE
399 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
400 | SgnVar n =>
401 let
402 val (_, sgn) = lookupSgnNamed env n
403 in
404 projectStr env {sgn = sgn, str = str, field = field}
405 end
406 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
407
301 408
302 val ktype = (KType, ErrorMsg.dummySpan) 409 val ktype = (KType, ErrorMsg.dummySpan)
303 410
304 fun bbind env x = #1 (pushCNamed env x ktype NONE) 411 fun bbind env x = #1 (pushCNamed env x ktype NONE)
305 412