Mercurial > urweb

comparison src/elab_env.sml @ 754:8688e01ae469

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