Mercurial > urweb
comparison src/elab_env.sml @ 42:b3fbbc6cb1e5
Elaborating 'where'
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 19 Jun 2008 16:35:40 -0400 |
parents | 1405d8c26790 |
children | 0a5c312de09a |
comparison
equal
deleted
inserted
replaced
41:1405d8c26790 | 42:b3fbbc6cb1e5 |
---|---|
359 ElabUtil.Sgn.map {kind = id, | 359 ElabUtil.Sgn.map {kind = id, |
360 con = sgnS_con (str, (strs, cons)), | 360 con = sgnS_con (str, (strs, cons)), |
361 sgn_item = id, | 361 sgn_item = id, |
362 sgn = id} | 362 sgn = id} |
363 | 363 |
364 fun projectCon env {sgn = (sgn, _), str, field} = | 364 fun hnormSgn env (all as (sgn, loc)) = |
365 case sgn of | 365 case sgn of |
366 SgnError => all | |
367 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) | |
368 | SgnConst _ => all | |
369 | SgnFun _ => all | |
370 | SgnWhere (sgn, x, c) => | |
371 case #1 (hnormSgn env sgn) of | |
372 SgnError => (SgnError, loc) | |
373 | SgnConst sgis => | |
374 let | |
375 fun traverse (pre, post) = | |
376 case post of | |
377 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" | |
378 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => | |
379 if x = x' then | |
380 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) | |
381 else | |
382 traverse (sgi :: pre, rest) | |
383 | sgi :: rest => traverse (sgi :: pre, rest) | |
384 | |
385 val sgis = traverse ([], sgis) | |
386 in | |
387 (SgnConst sgis, loc) | |
388 end | |
389 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" | |
390 | |
391 fun projectCon env {sgn, str, field} = | |
392 case #1 (hnormSgn env sgn) of | |
366 SgnConst sgis => | 393 SgnConst sgis => |
367 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE | 394 (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 | 395 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE |
369 | _ => NONE) sgis of | 396 | _ => NONE) sgis of |
370 NONE => NONE | 397 NONE => NONE |
371 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) | 398 | 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)) | 399 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) |
379 | SgnFun _ => NONE | 400 | _ => NONE |
380 | 401 |
381 fun projectVal env {sgn = (sgn, _), str, field} = | 402 fun projectVal env {sgn, str, field} = |
382 case sgn of | 403 case #1 (hnormSgn env sgn) of |
383 SgnConst sgis => | 404 SgnConst sgis => |
384 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of | 405 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of |
385 NONE => NONE | 406 NONE => NONE |
386 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) | 407 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) |
387 | SgnVar n => | |
388 let | |
389 val (_, sgn) = lookupSgnNamed env n | |
390 in | |
391 projectVal env {sgn = sgn, str = str, field = field} | |
392 end | |
393 | SgnError => SOME (CError, ErrorMsg.dummySpan) | 408 | SgnError => SOME (CError, ErrorMsg.dummySpan) |
394 | SgnFun _ => NONE | 409 | _ => NONE |
395 | 410 |
396 fun projectStr env {sgn = (sgn, _), str, field} = | 411 fun projectStr env {sgn, str, field} = |
397 case sgn of | 412 case #1 (hnormSgn env sgn) of |
398 SgnConst sgis => | 413 SgnConst sgis => |
399 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of | 414 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of |
400 NONE => NONE | 415 NONE => NONE |
401 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) | 416 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) |
402 | SgnVar n => | |
403 let | |
404 val (_, sgn) = lookupSgnNamed env n | |
405 in | |
406 projectStr env {sgn = sgn, str = str, field = field} | |
407 end | |
408 | SgnError => SOME (SgnError, ErrorMsg.dummySpan) | 417 | SgnError => SOME (SgnError, ErrorMsg.dummySpan) |
409 | SgnFun _ => NONE | 418 | _ => NONE |
410 | 419 |
411 | 420 |
412 val ktype = (KType, ErrorMsg.dummySpan) | 421 val ktype = (KType, ErrorMsg.dummySpan) |
413 | 422 |
414 fun bbind env x = #1 (pushCNamed env x ktype NONE) | 423 fun bbind env x = #1 (pushCNamed env x ktype NONE) |