Mercurial > urweb

comparison src/elab_env.sml @ 42:b3fbbc6cb1e5

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