Mercurial > urweb

comparison src/elaborate.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 87a7702d681d
comparison
equal deleted inserted replaced
753:d484df4e841a 754:8688e01ae469
801 (guessMap env (other, c, GuessFailure); 801 (guessMap env (other, c, GuessFailure);
802 true) 802 true)
803 handle GuessFailure => false 803 handle GuessFailure => false
804 end 804 end
805 805
806 val (fs1, fs2, others1, others2) = 806 val (fs1, fs2, others1, others2, unifs1, unifs2) =
807 case (fs1, fs2, others1, others2, unifs1, unifs2) of 807 case (fs1, fs2, others1, others2, unifs1, unifs2) of
808 ([], _, [other1], [], [], _) => 808 ([], _, [other1], [], [], _) =>
809 if isGuessable (other1, fs2, unifs2) then 809 if isGuessable (other1, fs2, unifs2) then
810 ([], [], [], []) 810 ([], [], [], [], [], [])
811 else 811 else
812 (fs1, fs2, others1, others2) 812 (fs1, fs2, others1, others2, unifs1, unifs2)
813 | (_, [], [], [other2], _, []) => 813 | (_, [], [], [other2], _, []) =>
814 if isGuessable (other2, fs1, unifs1) then 814 if isGuessable (other2, fs1, unifs1) then
815 ([], [], [], []) 815 ([], [], [], [], [], [])
816 else 816 else
817 (fs1, fs2, others1, others2) 817 (prefaces "Not guessable" [("other2", p_con env other2),
818 | _ => (fs1, fs2, others1, others2) 818 ("fs1", p_con env (L'.CRecord (k, fs1), loc)),
819 ("#unifs1", PD.string (Int.toString (length unifs1)))];
820 (fs1, fs2, others1, others2, unifs1, unifs2))
821 | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
819 822
820 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 823 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
821 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 824 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
822 825
823 val empty = (L'.CRecord (k, []), dummy) 826 val empty = (L'.CRecord (k, []), dummy)
847 val loc = #2 c1 850 val loc = #2 c1
848 851
849 fun unfold (dom, ran, f, r, c) = 852 fun unfold (dom, ran, f, r, c) =
850 let 853 let
851 fun unfold (r, c) = 854 fun unfold (r, c) =
852 case #1 c of 855 case #1 (hnormCon env c) of
853 L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc) 856 L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc)
854 | L'.CRecord (_, [(x, v)]) => 857 | L'.CRecord (_, [(x, v)]) =>
855 let 858 let
856 val v' = case dom of 859 val v' = case dom of
857 (L'.KUnit, _) => (L'.CUnit, loc) 860 (L'.KUnit, _) => (L'.CUnit, loc)
876 in 879 in
877 unfold (r1, c1'); 880 unfold (r1, c1');
878 unfold (r2, c2'); 881 unfold (r2, c2');
879 unifyCons env r (L'.CConcat (r1, r2), loc) 882 unifyCons env r (L'.CConcat (r1, r2), loc)
880 end 883 end
881 | L'.CUnif (_, _, _, ref (SOME c)) => unfold (r, c) 884 | L'.CUnif (_, _, _, ur) =>
882 | L'.CUnif (_, _, _, ur as ref NONE) =>
883 let 885 let
884 val ur' = cunif (loc, (L'.KRecord dom, loc)) 886 val ur' = cunif (loc, (L'.KRecord dom, loc))
885 in 887 in
886 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc) 888 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc)
887 end 889 end
1933 1935
1934 val hnormSgn = E.hnormSgn 1936 val hnormSgn = E.hnormSgn
1935 1937
1936 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) 1938 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1937 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) 1939 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
1940 fun viewOf () = (L'.CModProj (!basis_r, [], "sql_view"), ErrorMsg.dummySpan)
1941 fun queryOf () = (L'.CModProj (!basis_r, [], "sql_query"), ErrorMsg.dummySpan)
1938 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) 1942 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan)
1939 fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan) 1943 fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan)
1940 1944
1941 fun dopenConstraints (loc, env, denv) {str, strs} = 1945 fun dopenConstraints (loc, env, denv) {str, strs} =
1942 case E.lookupStr env str of 1946 case E.lookupStr env str of
2432 | L'.DExport _ => [] 2436 | L'.DExport _ => []
2433 | L'.DTable (tn, x, n, c, _, pc, _, cc) => 2437 | L'.DTable (tn, x, n, c, _, pc, _, cc) =>
2434 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), 2438 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
2435 (L'.CConcat (pc, cc), loc)), loc)), loc)] 2439 (L'.CConcat (pc, cc), loc)), loc)), loc)]
2436 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2440 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2441 | L'.DView (tn, x, n, _, c) =>
2442 [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)]
2437 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2443 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2438 | L'.DDatabase _ => [] 2444 | L'.DDatabase _ => []
2439 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2445 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2440 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] 2446 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
2441 2447
3402 | L.DSequence x => 3408 | L.DSequence x =>
3403 let 3409 let
3404 val (env, n) = E.pushENamed env x (sequenceOf ()) 3410 val (env, n) = E.pushENamed env x (sequenceOf ())
3405 in 3411 in
3406 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) 3412 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
3413 end
3414 | L.DView (x, e) =>
3415 let
3416 val (e', t, gs') = elabExp (env, denv) e
3417
3418 val k = (L'.KRecord (L'.KType, loc), loc)
3419 val fs = cunif (loc, k)
3420 val ts = cunif (loc, (L'.KRecord k, loc))
3421 val tf = (L'.CApp ((L'.CMap (k, k), loc),
3422 (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc)
3423 val ts = (L'.CApp (tf, ts), loc)
3424
3425 val cv = viewOf ()
3426 val cv = (L'.CApp (cv, fs), loc)
3427 val (env', n) = E.pushENamed env x cv
3428
3429 val ct = queryOf ()
3430 val ct = (L'.CApp (ct, ts), loc)
3431 val ct = (L'.CApp (ct, fs), loc)
3432 in
3433 checkCon env e' t ct;
3434 ([(L'.DView (!basis_r, x, n, e', fs), loc)],
3435 (env', denv, gs' @ gs))
3407 end 3436 end
3408 3437
3409 | L.DClass (x, k, c) => 3438 | L.DClass (x, k, c) =>
3410 let 3439 let
3411 val k = elabKind env k 3440 val k = elabKind env k