Mercurial > urweb
comparison src/elab_env.sml @ 754:8688e01ae469
A view query works
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 28 Apr 2009 15:04:37 -0400 |
parents | d484df4e841a |
children | e2780d2f4afc |
comparison
equal
deleted
inserted
replaced
753:d484df4e841a | 754:8688e01ae469 |
---|---|
589 | (d, _) => d} | 589 | (d, _) => d} |
590 0 | 590 0 |
591 | 591 |
592 exception Bad of con * con | 592 exception Bad of con * con |
593 | 593 |
594 val hasUnif = U.Con.exists {kind = fn _ => false, | |
595 con = fn CUnif (_, _, _, ref NONE) => true | |
596 | _ => false} | |
597 | |
598 fun startsWithUnif c = | |
599 let | |
600 fun firstArg (c, acc) = | |
601 case #1 c of | |
602 CApp (f, x) => firstArg (f, SOME x) | |
603 | _ => acc | |
604 in | |
605 case firstArg (c, NONE) of | |
606 NONE => false | |
607 | SOME x => hasUnif x | |
608 end | |
609 | |
594 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = | 610 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = |
595 let | 611 let |
596 fun resolve c = | 612 fun resolve c = |
597 let | 613 let |
598 fun doHead f = | 614 fun doHead f = |
669 | SOME _ => SOME e | 685 | SOME _ => SOME e |
670 in | 686 in |
671 tryGrounds (#ground class) | 687 tryGrounds (#ground class) |
672 end | 688 end |
673 in | 689 in |
674 case #1 c of | 690 if startsWithUnif c then |
675 TRecord c => | 691 NONE |
676 (case #1 (hnorm c) of | 692 else |
677 CRecord (_, xts) => | 693 case #1 c of |
678 let | 694 TRecord c => |
679 fun resolver (xts, acc) = | 695 (case #1 (hnorm c) of |
680 case xts of | 696 CRecord (_, xts) => |
681 [] => SOME (ERecord acc, #2 c) | 697 let |
682 | (x, t) :: xts => | 698 fun resolver (xts, acc) = |
683 let | 699 case xts of |
684 val t = hnorm t | 700 [] => SOME (ERecord acc, #2 c) |
685 | 701 | (x, t) :: xts => |
686 val t = case t of | 702 let |
687 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) | 703 val t = hnorm t |
688 | _ => t | 704 |
689 in | 705 val t = case t of |
690 case resolve t of | 706 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) |
691 NONE => NONE | 707 | _ => t |
692 | SOME e => resolver (xts, (x, e, t) :: acc) | 708 in |
693 end | 709 case resolve t of |
694 in | 710 NONE => NONE |
695 resolver (xts, []) | 711 | SOME e => resolver (xts, (x, e, t) :: acc) |
696 end | 712 end |
697 | _ => NONE) | 713 in |
698 | _ => | 714 resolver (xts, []) |
699 case class_head_in c of | 715 end |
700 SOME f => doHead f | 716 | _ => NONE) |
701 | _ => NONE | 717 | _ => |
718 case class_head_in c of | |
719 SOME f => doHead f | |
720 | _ => NONE | |
702 end | 721 end |
703 in | 722 in |
704 resolve | 723 resolve |
705 end | 724 end |
706 | 725 |
1480 let | 1499 let |
1481 val t = (CModProj (tn, [], "sql_sequence"), loc) | 1500 val t = (CModProj (tn, [], "sql_sequence"), loc) |
1482 in | 1501 in |
1483 pushENamedAs env x n t | 1502 pushENamedAs env x n t |
1484 end | 1503 end |
1504 | DView (tn, x, n, _, c) => | |
1505 let | |
1506 val ct = (CModProj (tn, [], "sql_view"), loc) | |
1507 val ct = (CApp (ct, c), loc) | |
1508 in | |
1509 pushENamedAs env x n ct | |
1510 end | |
1485 | DClass (x, n, k, c) => | 1511 | DClass (x, n, k, c) => |
1486 let | 1512 let |
1487 val k = (KArrow (k, (KType, loc)), loc) | 1513 val k = (KArrow (k, (KType, loc)), loc) |
1488 val env = pushCNamedAs env x n k (SOME c) | 1514 val env = pushCNamedAs env x n k (SOME c) |
1489 in | 1515 in |