Mercurial > urweb

comparison src/elab_env.sml @ 158:b4b70de488e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More datatype module stuff
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 16:36:41 -0400
parents adc4e42e3adc
children 06a98129b23f
comparison
equal deleted inserted replaced
157:adc4e42e3adc 158:b4b70de488e9
364 fun seek (sgis, sgns, strs, cons) = 364 fun seek (sgis, sgns, strs, cons) =
365 case sgis of 365 case sgis of
366 [] => NONE 366 [] => NONE
367 | (sgi, _) :: sgis => 367 | (sgi, _) :: sgis =>
368 case f sgi of 368 case f sgi of
369 SOME v => SOME (v, (sgns, strs, cons)) 369 SOME v =>
370 let
371 val cons =
372 case sgi of
373 SgiDatatype (x, n, _) => IM.insert (cons, n, x)
374 | SgiDatatypeImp (x, n, _, _, _) => IM.insert (cons, n, x)
375 | _ => cons
376 in
377 SOME (v, (sgns, strs, cons))
378 end
370 | NONE => 379 | NONE =>
371 case sgi of 380 case sgi of
372 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 381 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
373 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 382 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
374 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 383 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
501 NONE => NONE 510 NONE => NONE
502 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) 511 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
503 | SgnError => SOME (SgnError, ErrorMsg.dummySpan) 512 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
504 | _ => NONE 513 | _ => NONE
505 514
515 fun chaseMpath env (n, ms) =
516 let
517 val (_, sgn) = lookupStrNamed env n
518 in
519 foldl (fn (m, (str, sgn)) =>
520 case projectStr env {sgn = sgn, str = str, field = m} of
521 NONE => raise Fail "kindof: Unknown substructure"
522 | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
523 ((StrVar n, #2 sgn), sgn) ms
524 end
525
506 fun projectCon env {sgn, str, field} = 526 fun projectCon env {sgn, str, field} =
507 case #1 (hnormSgn env sgn) of 527 case #1 (hnormSgn env sgn) of
508 SgnConst sgis => 528 SgnConst sgis =>
509 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 529 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
510 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 530 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
511 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE 531 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
532 | SgiDatatypeImp (x, _, m1, ms, x') =>
533 if x = field then
534 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
535 else
536 NONE
512 | _ => NONE) sgis of 537 | _ => NONE) sgis of
513 NONE => NONE 538 NONE => NONE
514 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) 539 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
515 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) 540 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
516 | _ => NONE 541 | _ => NONE
517 542
518 fun projectDatatype env {sgn, str, field} = 543 fun projectDatatype env {sgn, str, field} =
519 case #1 (hnormSgn env sgn) of 544 case #1 (hnormSgn env sgn) of
520 SgnConst sgis => 545 SgnConst sgis =>
521 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE 546 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
547 | SgiDatatypeImp (x, _, m1, ms, x') =>
548 if x = field then
549 let
550 val (str, sgn) = chaseMpath env (m1, ms)
551 in
552 projectDatatype env {sgn = sgn, str = str, field = x'}
553 end
554 else
555 NONE
522 | _ => NONE) sgis of 556 | _ => NONE) sgis of
523 NONE => NONE 557 NONE => NONE
524 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) 558 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
525 | _ => NONE 559 | _ => NONE
526 560
527 fun projectVal env {sgn, str, field} = 561 fun projectVal env {sgn, str, field} =
528 case #1 (hnormSgn env sgn) of 562 case #1 (hnormSgn env sgn) of
529 SgnConst sgis => 563 SgnConst sgis =>
530 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of 564 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
565 | SgiDatatype (_, n, xncs) =>
566 ListUtil.search (fn (x, _, to) =>
567 if x = field then
568 SOME (case to of
569 NONE => (CNamed n, #2 sgn)
570 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
571 else
572 NONE) xncs
573 | SgiDatatypeImp (_, n, m1, ms, x') =>
574 let
575 val (str, sgn) = chaseMpath env (m1, ms)
576 in
577 case projectDatatype env {sgn = sgn, str = str, field = x'} of
578 NONE => NONE
579 | SOME xncs =>
580 ListUtil.search (fn (x, _, to) =>
581 if x = field then
582 SOME (case to of
583 NONE => (CNamed n, #2 sgn)
584 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
585 else
586 NONE) xncs
587 end
588 | _ => NONE) sgis of
531 NONE => NONE 589 NONE => NONE
532 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) 590 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
533 | SgnError => SOME (CError, ErrorMsg.dummySpan) 591 | SgnError => SOME (CError, ErrorMsg.dummySpan)
534 | _ => NONE 592 | _ => NONE
535 593