Mercurial > urweb

comparison src/elab_env.sml @ 162:06a98129b23f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents b4b70de488e9
children c7a6e6dbc318
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
351 in 351 in
352 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 352 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
353 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 353 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
354 env xncs 354 env xncs
355 end 355 end
356 | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) 356 | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
357 let
358 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
359 in
360 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
361 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
362 env xncs
363 end
357 | SgiVal (x, n, t) => pushENamedAs env x n t 364 | SgiVal (x, n, t) => pushENamedAs env x n t
358 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 365 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
359 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 366 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
360 | SgiConstraint _ => env 367 | SgiConstraint _ => env
361 368
369 SOME v => 376 SOME v =>
370 let 377 let
371 val cons = 378 val cons =
372 case sgi of 379 case sgi of
373 SgiDatatype (x, n, _) => IM.insert (cons, n, x) 380 SgiDatatype (x, n, _) => IM.insert (cons, n, x)
374 | SgiDatatypeImp (x, n, _, _, _) => IM.insert (cons, n, x) 381 | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x)
375 | _ => cons 382 | _ => cons
376 in 383 in
377 SOME (v, (sgns, strs, cons)) 384 SOME (v, (sgns, strs, cons))
378 end 385 end
379 | NONE => 386 | NONE =>
380 case sgi of 387 case sgi of
381 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 388 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
382 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 389 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
383 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 390 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
384 | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 391 | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
385 | SgiVal _ => seek (sgis, sgns, strs, cons) 392 | SgiVal _ => seek (sgis, sgns, strs, cons)
386 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 393 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
387 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 394 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
388 | SgiConstraint _ => seek (sgis, sgns, strs, cons) 395 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
389 in 396 in
527 case #1 (hnormSgn env sgn) of 534 case #1 (hnormSgn env sgn) of
528 SgnConst sgis => 535 SgnConst sgis =>
529 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 536 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
530 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 537 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
531 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE 538 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
532 | SgiDatatypeImp (x, _, m1, ms, x') => 539 | SgiDatatypeImp (x, _, m1, ms, x', _) =>
533 if x = field then 540 if x = field then
534 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) 541 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
535 else 542 else
536 NONE 543 NONE
537 | _ => NONE) sgis of 544 | _ => NONE) sgis of
542 549
543 fun projectDatatype env {sgn, str, field} = 550 fun projectDatatype env {sgn, str, field} =
544 case #1 (hnormSgn env sgn) of 551 case #1 (hnormSgn env sgn) of
545 SgnConst sgis => 552 SgnConst sgis =>
546 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE 553 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
547 | SgiDatatypeImp (x, _, m1, ms, x') => 554 | SgiDatatypeImp (x, _, _, _, _, xncs) => if x = field then SOME xncs else NONE
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
556 | _ => NONE) sgis of 555 | _ => NONE) sgis of
557 NONE => NONE 556 NONE => NONE
558 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) 557 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
559 | _ => NONE 558 | _ => NONE
560 559
561 fun projectVal env {sgn, str, field} = 560 fun projectVal env {sgn, str, field} =
562 case #1 (hnormSgn env sgn) of 561 case #1 (hnormSgn env sgn) of
563 SgnConst sgis => 562 SgnConst sgis =>
564 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE 563 let
565 | SgiDatatype (_, n, xncs) => 564 fun seek (n, xncs) =
566 ListUtil.search (fn (x, _, to) => 565 ListUtil.search (fn (x, _, to) =>
567 if x = field then 566 if x = field then
568 SOME (case to of 567 SOME (case to of
569 NONE => (CNamed n, #2 sgn) 568 NONE => (CNamed n, #2 sgn)
570 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn)) 569 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
571 else 570 else
572 NONE) xncs 571 NONE) xncs
573 | SgiDatatypeImp (_, n, m1, ms, x') => 572 in
574 let 573 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
575 val (str, sgn) = chaseMpath env (m1, ms) 574 | SgiDatatype (_, n, xncs) => seek (n, xncs)
576 in 575 | SgiDatatypeImp (_, n, _, _, _, xncs) => seek (n, xncs)
577 case projectDatatype env {sgn = sgn, str = str, field = x'} of 576 | _ => NONE) sgis of
578 NONE => NONE 577 NONE => NONE
579 | SOME xncs => 578 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
580 ListUtil.search (fn (x, _, to) => 579 end
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
589 NONE => NONE
590 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
591 | SgnError => SOME (CError, ErrorMsg.dummySpan) 580 | SgnError => SOME (CError, ErrorMsg.dummySpan)
592 | _ => NONE 581 | _ => NONE
593 582
594 fun sgnSeekConstraints (str, sgis) = 583 fun sgnSeekConstraints (str, sgis) =
595 let 584 let
605 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) 594 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
606 end 595 end
607 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 596 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
608 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 597 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
609 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 598 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
610 | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 599 | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
611 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 600 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
612 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 601 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
613 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 602 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
614 in 603 in
615 seek (sgis, IM.empty, IM.empty, IM.empty, []) 604 seek (sgis, IM.empty, IM.empty, IM.empty, [])
630 in 619 in
631 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 620 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
632 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 621 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
633 env xncs 622 env xncs
634 end 623 end
635 | DDatatypeImp (x, n, m, ms, x') => 624 | DDatatypeImp (x, n, m, ms, x', xncs) =>
636 let 625 let
637 val t = (CModProj (m, ms, x'), loc) 626 val t = (CModProj (m, ms, x'), loc)
638 val env = pushCNamedAs env x n (KType, loc) (SOME t) 627 val env = pushCNamedAs env x n (KType, loc) (SOME t)
639 val (_, sgn) = lookupStrNamed env m
640 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
641 case projectStr env {sgn = sgn, str = str, field = m} of
642 NONE => raise Fail "ElabEnv.declBinds: Couldn't projectStr"
643 | SOME sgn => ((StrProj (str, m), loc), sgn))
644 ((StrVar m, loc), sgn) ms
645 val xncs = case projectDatatype env {sgn = sgn, str = str, field = x'} of
646 NONE => raise Fail "ElabEnv.declBinds: Couldn't projectDatatype"
647 | SOME xncs => xncs
648 628
649 val t = (CNamed n, loc) 629 val t = (CNamed n, loc)
650 in 630 in
651 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t 631 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t
652 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc)) 632 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc))