Mercurial > urweb

comparison src/elaborate.sml @ 205:cb8f69556975

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating 'SELECT *' queries
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 15:24:59 -0400
parents dd82457fda82
children cb8493759a7b
comparison
equal deleted inserted replaced
204:241c9a0e3397 205:cb8f69556975
556 | L'.CError => kerror 556 | L'.CError => kerror
557 | L'.CUnif (_, k, _, _) => k 557 | L'.CUnif (_, k, _, _) => k
558 558
559 val hnormCon = D.hnormCon 559 val hnormCon = D.hnormCon
560 560
561 datatype con_summary =
562 Nil
563 | Cons
564 | Unknown
565
566 fun compatible cs =
567 case cs of
568 (Unknown, _) => false
569 | (_, Unknown) => false
570 | (s1, s2) => s1 = s2
571
572 fun summarizeCon (env, denv) c =
573 let
574 val (c, gs) = hnormCon (env, denv) c
575 in
576 case #1 c of
577 L'.CRecord (_, []) => (Nil, gs)
578 | L'.CRecord (_, _ :: _) => (Cons, gs)
579 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
580 | L'.CDisjoint (_, _, c) =>
581 let
582 val (s, gs') = summarizeCon (env, denv) c
583 in
584 (s, gs @ gs')
585 end
586 | _ => (Unknown, gs)
587 end
588
589 fun p_con_summary s =
590 Print.PD.string (case s of
591 Nil => "Nil"
592 | Cons => "Cons"
593 | Unknown => "Unknown")
594
561 fun unifyRecordCons (env, denv) (c1, c2) = 595 fun unifyRecordCons (env, denv) (c1, c2) =
562 let 596 let
563 fun rkindof c = 597 fun rkindof c =
564 case hnormKind (kindof env c) of 598 case hnormKind (kindof env c) of
565 (L'.KRecord k, _) => k 599 (L'.KRecord k, _) => k
703 737
704 and unifyCons' (env, denv) c1 c2 = 738 and unifyCons' (env, denv) c1 c2 =
705 let 739 let
706 val (c1, gs1) = hnormCon (env, denv) c1 740 val (c1, gs1) = hnormCon (env, denv) c1
707 val (c2, gs2) = hnormCon (env, denv) c2 741 val (c2, gs2) = hnormCon (env, denv) c2
708 val gs3 = unifyCons'' (env, denv) c1 c2
709 in 742 in
710 gs1 @ gs2 @ gs3 743 let
744 val gs3 = unifyCons'' (env, denv) c1 c2
745 in
746 gs1 @ gs2 @ gs3
747 end
748 handle ex =>
749 let
750 val loc = #2 c1
751
752 fun unfold (dom, f, i, r, c) =
753 let
754 val nm = cunif (loc, (L'.KName, loc))
755 val v = cunif (loc, dom)
756 val rest = cunif (loc, (L'.KRecord dom, loc))
757
758 val (iS, gs3) = summarizeCon (env, denv) i
759
760 val app = (L'.CApp (f, nm), loc)
761 val app = (L'.CApp (app, v), loc)
762 val app = (L'.CApp (app, rest), loc)
763 val (appS, gs4) = summarizeCon (env, denv) app
764
765 val (cS, gs5) = summarizeCon (env, denv) c
766 in
767 (*prefaces "Summaries" [("iS", p_con_summary iS),
768 ("appS", p_con_summary appS),
769 ("cS", p_con_summary cS)];*)
770
771 if compatible (iS, appS) then
772 raise ex
773 else if compatible (cS, iS) then
774 let
775 (*val () = prefaces "Same?" [("i", p_con env i),
776 ("c", p_con env c)]*)
777 val gs6 = unifyCons (env, denv) i c
778 (*val () = TextIO.print "Yes!\n"*)
779
780 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
781 in
782 gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
783 end
784 else if compatible (cS, appS) then
785 let
786 (*val () = prefaces "Same?" [("app", p_con env app),
787 ("c", p_con env c),
788 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
789 val gs6 = unifyCons (env, denv) app c
790 (*val () = TextIO.print "Yes!\n"*)
791
792 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
793 val concat = (L'.CConcat (singleton, rest), loc)
794 val gs7 = unifyCons (env, denv) r concat
795 in
796 (loc, env, denv, singleton, rest) :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
797 end
798 else
799 raise ex
800 end
801 handle _ => raise ex
802 in
803 case (#1 c1, #1 c2) of
804 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r), _) =>
805 unfold (dom, f, i, r, c2)
806 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r)) =>
807 unfold (dom, f, i, r, c1)
808 | _ => raise ex
809 end
711 end 810 end
712 811
713 and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) = 812 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
714 let 813 let
715 fun err f = raise CUnify' (f (c1All, c2All)) 814 fun err f = raise CUnify' (f (c1All, c2All))
716 815
717 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) 816 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
718 in 817 in
792 err COccursCheckFailed 891 err COccursCheckFailed
793 else 892 else
794 (r := SOME c1All; 893 (r := SOME c1All;
795 []) 894 [])
796 895
797
798 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => 896 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
799 (unifyKinds dom1 dom2; 897 (unifyKinds dom1 dom2;
800 unifyKinds ran1 ran2; 898 unifyKinds ran1 ran2;
801 []) 899 [])
900
802 901
803 | _ => err CIncompatible 902 | _ => err CIncompatible
804 end 903 end
805 904
806 and unifyCons (env, denv) c1 c2 = 905 and unifyCons (env, denv) c1 c2 =
1262 val ran = cunif (loc, ktype) 1361 val ran = cunif (loc, ktype)
1263 val t = (L'.TFun (dom, ran), dummy) 1362 val t = (L'.TFun (dom, ran), dummy)
1264 1363
1265 val gs4 = checkCon (env, denv) e1' t1 t 1364 val gs4 = checkCon (env, denv) e1' t1 t
1266 val gs5 = checkCon (env, denv) e2' t2 dom 1365 val gs5 = checkCon (env, denv) e2' t2 dom
1366
1367 val gs = gs1 @ gs2 @ gs3 @ gs4 @ gs5
1267 in 1368 in
1268 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5) 1369 ((L'.EApp (e1', e2'), loc), ran, gs)
1269 end 1370 end
1270 | L.EAbs (x, to, e) => 1371 | L.EAbs (x, to, e) =>
1271 let 1372 let
1272 val (t', gs1) = case to of 1373 val (t', gs1) = case to of
1273 NONE => (cunif (loc, ktype), []) 1374 NONE => (cunif (loc, ktype), [])
1569 | NotDatatype loc => 1670 | NotDatatype loc =>
1570 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype" 1671 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
1571 1672
1572 val hnormSgn = E.hnormSgn 1673 val hnormSgn = E.hnormSgn
1573 1674
1675 fun tableOf' env =
1676 case E.lookupStr env "Basis" of
1677 NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
1678 | SOME (n, _) => n
1679
1680 fun tableOf env = (L'.CModProj (tableOf' env, [], "sql_table"), ErrorMsg.dummySpan)
1681
1574 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1682 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1575 case sgi of 1683 case sgi of
1576 L.SgiConAbs (x, k) => 1684 L.SgiConAbs (x, k) =>
1577 let 1685 let
1578 val k' = elabKind k 1686 val k' = elabKind k
1737 end 1845 end
1738 1846
1739 | L.SgiTable (x, c) => 1847 | L.SgiTable (x, c) =>
1740 let 1848 let
1741 val (c', k, gs) = elabCon (env, denv) c 1849 val (c', k, gs) = elabCon (env, denv) c
1742 val (env, n) = E.pushENamed env x c' 1850 val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc)
1743 in 1851 in
1744 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 1852 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1745 ([(L'.SgiTable (x, n, c'), loc)], (env, denv, gs)) 1853 ([(L'.SgiTable (tableOf' env, x, n, c'), loc)], (env, denv, gs))
1746 end 1854 end
1747 1855
1748 and elabSgn (env, denv) (sgn, loc) = 1856 and elabSgn (env, denv) (sgn, loc) =
1749 case sgn of 1857 case sgn of
1750 L.SgnConst sgis => 1858 L.SgnConst sgis =>
1804 sgnError env (DuplicateStr (loc, x)) 1912 sgnError env (DuplicateStr (loc, x))
1805 else 1913 else
1806 (); 1914 ();
1807 (cons, vals, sgns, SS.add (strs, x))) 1915 (cons, vals, sgns, SS.add (strs, x)))
1808 | L'.SgiConstraint _ => (cons, vals, sgns, strs) 1916 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
1809 | L'.SgiTable (x, _, _) => 1917 | L'.SgiTable (_, x, _, _) =>
1810 (if SS.member (vals, x) then 1918 (if SS.member (vals, x) then
1811 sgnError env (DuplicateVal (loc, x)) 1919 sgnError env (DuplicateVal (loc, x))
1812 else 1920 else
1813 (); 1921 ();
1814 (cons, SS.add (vals, x), sgns, strs))) 1922 (cons, SS.add (vals, x), sgns, strs)))
1907 in 2015 in
1908 case self str of 2016 case self str of
1909 NONE => sgn 2017 NONE => sgn
1910 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 2018 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1911 end 2019 end
1912
1913 fun tableOf env =
1914 case E.lookupStr env "Basis" of
1915 NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
1916 | SOME (n, _) => (L'.CModProj (n, [], "sql_table"), ErrorMsg.dummySpan)
1917 2020
1918 fun dopen (env, denv) {str, strs, sgn} = 2021 fun dopen (env, denv) {str, strs, sgn} =
1919 let 2022 let
1920 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) 2023 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1921 (L'.StrVar str, #2 sgn) strs 2024 (L'.StrVar str, #2 sgn) strs
1944 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) 2047 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
1945 | L'.SgiSgn (x, n, sgn) => 2048 | L'.SgiSgn (x, n, sgn) =>
1946 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 2049 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
1947 | L'.SgiConstraint (c1, c2) => 2050 | L'.SgiConstraint (c1, c2) =>
1948 (L'.DConstraint (c1, c2), loc) 2051 (L'.DConstraint (c1, c2), loc)
1949 | L'.SgiTable (x, n, c) => 2052 | L'.SgiTable (_, x, n, c) =>
1950 (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc), 2053 (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc),
1951 (L'.EModProj (str, strs, x), loc)), loc) 2054 (L'.EModProj (str, strs, x), loc)), loc)
1952 in 2055 in
1953 (d, (E.declBinds env' d, denv')) 2056 (d, (E.declBinds env' d, denv'))
1954 end) 2057 end)
1999 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 2102 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
2000 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2103 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2001 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2104 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2002 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2105 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2003 | L'.DExport _ => [] 2106 | L'.DExport _ => []
2004 | L'.DTable (x, n, c) => [(L'.SgiTable (x, n, c), loc)] 2107 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
2005 2108
2006 fun sgiBindsD (env, denv) (sgi, _) = 2109 fun sgiBindsD (env, denv) (sgi, _) =
2007 case sgi of 2110 case sgi of
2008 L'.SgiConstraint (c1, c2) => 2111 L'.SgiConstraint (c1, c2) =>
2009 (case D.assert env denv (c1, c2) of 2112 (case D.assert env denv (c1, c2) of
2192 handle CUnify (c1, c2, err) => 2295 handle CUnify (c1, c2, err) =>
2193 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2296 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2194 SOME (env, denv)) 2297 SOME (env, denv))
2195 else 2298 else
2196 NONE 2299 NONE
2197 | L'.SgiTable (x', n1, c1) => 2300 | L'.SgiTable (_, x', n1, c1) =>
2198 if x = x' then 2301 if x = x' then
2199 (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of 2302 (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of
2200 [] => SOME (env, denv) 2303 [] => SOME (env, denv)
2201 | _ => NONE) 2304 | _ => NONE)
2202 handle CUnify (c1, c2, err) => 2305 handle CUnify (c1, c2, err) =>
2264 end 2367 end
2265 else 2368 else
2266 NONE 2369 NONE
2267 | _ => NONE) 2370 | _ => NONE)
2268 2371
2269 | L'.SgiTable (x, n2, c2) => 2372 | L'.SgiTable (_, x, n2, c2) =>
2270 seek (fn sgi1All as (sgi1, _) => 2373 seek (fn sgi1All as (sgi1, _) =>
2271 case sgi1 of 2374 case sgi1 of
2272 L'.SgiTable (x', n1, c1) => 2375 L'.SgiTable (_, x', n1, c1) =>
2273 if x = x' then 2376 if x = x' then
2274 (case unifyCons (env, denv) c1 c2 of 2377 (case unifyCons (env, denv) c1 c2 of
2275 [] => SOME (env, denv) 2378 [] => SOME (env, denv)
2276 | _ => NONE) 2379 | _ => NONE)
2277 handle CUnify (c1, c2, err) => 2380 handle CUnify (c1, c2, err) =>
2539 end 2642 end
2540 2643
2541 | L.DOpen (m, ms) => 2644 | L.DOpen (m, ms) =>
2542 (case E.lookupStr env m of 2645 (case E.lookupStr env m of
2543 NONE => (strError env (UnboundStr (loc, m)); 2646 NONE => (strError env (UnboundStr (loc, m));
2544 ([], (env, denv, []))) 2647 ([], (env, denv, gs)))
2545 | SOME (n, sgn) => 2648 | SOME (n, sgn) =>
2546 let 2649 let
2547 val (_, sgn) = foldl (fn (m, (str, sgn)) => 2650 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
2548 case E.projectStr env {str = str, sgn = sgn, field = m} of 2651 case E.projectStr env {str = str, sgn = sgn, field = m} of
2549 NONE => (strError env (UnboundStr (loc, m)); 2652 NONE => (strError env (UnboundStr (loc, m));
2552 ((L'.StrVar n, loc), sgn) ms 2655 ((L'.StrVar n, loc), sgn) ms
2553 2656
2554 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} 2657 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
2555 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} 2658 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
2556 in 2659 in
2557 (ds, (env', denv', [])) 2660 (ds, (env', denv', gs))
2558 end) 2661 end)
2559 2662
2560 | L.DConstraint (c1, c2) => 2663 | L.DConstraint (c1, c2) =>
2561 let 2664 let
2562 val (c1', k1, gs1) = elabCon (env, denv) c1 2665 val (c1', k1, gs1) = elabCon (env, denv) c1
2566 val (denv', gs4) = D.assert env denv (c1', c2') 2669 val (denv', gs4) = D.assert env denv (c1', c2')
2567 in 2670 in
2568 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 2671 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
2569 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 2672 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
2570 2673
2571 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4)) 2674 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4 @ gs))
2572 end 2675 end
2573 2676
2574 | L.DOpenConstraints (m, ms) => 2677 | L.DOpenConstraints (m, ms) =>
2575 let 2678 let
2576 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} 2679 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
2577 in 2680 in
2578 ([], (env, denv, [])) 2681 ([], (env, denv, gs))
2579 end 2682 end
2580 2683
2581 | L.DExport str => 2684 | L.DExport str =>
2582 let 2685 let
2583 val (str', sgn, gs) = elabStr (env, denv) str 2686 val (str', sgn, gs') = elabStr (env, denv) str
2584 2687
2585 val sgn = 2688 val sgn =
2586 case #1 (hnormSgn env sgn) of 2689 case #1 (hnormSgn env sgn) of
2587 L'.SgnConst sgis => 2690 L'.SgnConst sgis =>
2588 let 2691 let
2624 in 2727 in
2625 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) 2728 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
2626 end 2729 end
2627 | _ => sgn 2730 | _ => sgn
2628 in 2731 in
2629 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs)) 2732 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
2630 end 2733 end
2631 2734
2632 | L.DTable (x, c) => 2735 | L.DTable (x, c) =>
2633 let 2736 let
2634 val (c', k, gs) = elabCon (env, denv) c 2737 val (c', k, gs') = elabCon (env, denv) c
2635 val (env, n) = E.pushENamed env x c' 2738 val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc)
2636 in 2739 in
2637 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 2740 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
2638 ([(L'.DTable (x, n, c'), loc)], (env, denv, gs)) 2741 ([(L'.DTable (tableOf' env, x, n, c'), loc)], (env, denv, gs' @ gs))
2639 end 2742 end
2640 2743
2641 and elabStr (env, denv) (str, loc) = 2744 and elabStr (env, denv) (str, loc) =
2642 case str of 2745 case str of
2643 L.StrConst ds => 2746 L.StrConst ds =>
2727 (SS.add (strs, x), x) 2830 (SS.add (strs, x), x)
2728 in 2831 in
2729 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 2832 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
2730 end 2833 end
2731 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) 2834 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
2732 | L'.SgiTable (x, n, c) => 2835 | L'.SgiTable (tn, x, n, c) =>
2733 let 2836 let
2734 val (vals, x) = 2837 val (vals, x) =
2735 if SS.member (vals, x) then 2838 if SS.member (vals, x) then
2736 (vals, "?" ^ x) 2839 (vals, "?" ^ x)
2737 else 2840 else
2738 (SS.add (vals, x), x) 2841 (SS.add (vals, x), x)
2739 in 2842 in
2740 ((L'.SgiTable (x, n, c), loc) :: sgis, cons, vals, sgns, strs) 2843 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
2741 end) 2844 end)
2742 2845
2743 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 2846 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
2744 in 2847 in
2745 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 2848 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)