Mercurial > urweb

comparison src/iflow.sml @ 1226:df5bd4115267

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use functional dependency information
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 15:05:51 -0400
parents 3950cf1f5736
children 1d8fba74e7f5
comparison
equal deleted inserted replaced
1225:950d1e540df6 1226:df5bd4115267
390 val check : database * atom -> bool 390 val check : database * atom -> bool
391 391
392 val p_database : database Print.printer 392 val p_database : database Print.printer
393 393
394 val builtFrom : database * {Base : exp list, Derived : exp} -> bool 394 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
395
396 val p_repOf : database -> exp Print.printer
395 end = struct 397 end = struct
396 398
397 exception Contradiction 399 exception Contradiction
398 exception Undetermined 400 exception Undetermined
399 401
410 and variety = 412 and variety =
411 Dt0 of string 413 Dt0 of string
412 | Dt1 of string * node ref 414 | Dt1 of string * node ref
413 | Prim of Prim.t 415 | Prim of Prim.t
414 | Recrd of node ref SM.map ref * bool 416 | Recrd of node ref SM.map ref * bool
415 | VFinish
416 | Nothing 417 | Nothing
417 418
418 type representative = node ref 419 type representative = node ref
419
420 val finish = ref (Node {Rep = ref NONE,
421 Cons = ref SM.empty,
422 Variety = VFinish,
423 Known = ref true})
424 420
425 type database = {Vars : representative IM.map ref, 421 type database = {Vars : representative IM.map ref,
426 Consts : representative CM.map ref, 422 Consts : representative CM.map ref,
427 Con0s : representative SM.map ref, 423 Con0s : representative SM.map ref,
428 Records : (representative SM.map * representative) list ref, 424 Records : (representative SM.map * representative) list ref,
465 string "}", 461 string "}",
466 if b then 462 if b then
467 box [space, 463 box [space,
468 string "(complete)"] 464 string "(complete)"]
469 else 465 else
470 box []] 466 box []]]
471 | VFinish => string "FINISH"]
472 467
473 fun p_database (db : database) = 468 fun p_database (db : database) =
474 box [string "Vars:", 469 box [string "Vars:",
475 newline, 470 newline,
476 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i), 471 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
598 in 593 in
599 cons := SM.insert (!cons, f, r''); 594 cons := SM.insert (!cons, f, r'');
600 #Rep (unNode r) := SOME r''; 595 #Rep (unNode r) := SOME r'';
601 r' 596 r'
602 end 597 end
603 | VFinish => r
604 | _ => raise Contradiction 598 | _ => raise Contradiction
605 end 599 end
606 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon" 600 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
607 | Func (Other f, es) => 601 | Func (Other f, es) =>
608 let 602 let
677 Known = #Known (unNode r)}) 671 Known = #Known (unNode r)})
678 in 672 in
679 #Rep (unNode r) := SOME r''; 673 #Rep (unNode r) := SOME r'';
680 r' 674 r'
681 end 675 end
682 | VFinish => r
683 | _ => raise Contradiction 676 | _ => raise Contradiction
684 end 677 end
685 | Finish => finish 678 | Finish => raise Contradiction
686 in 679 in
687 rep e 680 rep e
688 end 681 end
682
683 fun p_repOf db e = p_rep (representative (db, e))
689 684
690 fun assert (db, a) = 685 fun assert (db, a) =
691 case a of 686 case a of
692 ACond _ => () 687 ACond _ => ()
693 | AReln x => 688 | AReln x =>
744 | _ => raise Contradiction 739 | _ => raise Contradiction
745 end 740 end
746 | (Eq, [e1, e2]) => 741 | (Eq, [e1, e2]) =>
747 let 742 let
748 fun markEq (r1, r2) = 743 fun markEq (r1, r2) =
749 if r1 = r2 then 744 let
750 () 745 val r1 = repOf r1
751 else case (#Variety (unNode r1), #Variety (unNode r2)) of 746 val r2 = repOf r2
752 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then 747 in
753 () 748 if r1 = r2 then
754 else 749 ()
755 raise Contradiction 750 else case (#Variety (unNode r1), #Variety (unNode r2)) of
756 | (Dt0 f1, Dt0 f2) => if f1 = f2 then 751 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
757 () 752 ()
758 else 753 else
759 raise Contradiction 754 raise Contradiction
760 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then 755 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
761 markEq (r1, r2) 756 ()
762 else 757 else
763 raise Contradiction 758 raise Contradiction
764 | (Recrd (xes1, _), Recrd (xes2, _)) => 759 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
765 let 760 markEq (r1, r2)
766 fun unif (xes1, xes2) = 761 else
767 SM.appi (fn (x, r1) => 762 raise Contradiction
768 case SM.find (xes2, x) of 763 | (Recrd (xes1, _), Recrd (xes2, _)) =>
769 NONE => () 764 let
770 | SOME r2 => markEq (r1, r2)) xes1 765 fun unif (xes1, xes2) =
771 in 766 SM.appi (fn (x, r1) =>
772 unif (!xes1, !xes2); 767 case SM.find (!xes2, x) of
773 unif (!xes2, !xes1) 768 NONE => xes2 := SM.insert (!xes2, x, r1)
774 end 769 | SOME r2 => markEq (r1, r2)) (!xes1)
775 | (VFinish, VFinish) => () 770 in
776 | (Nothing, _) => mergeNodes (r1, r2) 771 unif (xes1, xes2);
777 | (_, Nothing) => mergeNodes (r2, r1) 772 unif (xes2, xes1)
778 | _ => raise Contradiction 773 end
774 | (Nothing, _) => mergeNodes (r1, r2)
775 | (_, Nothing) => mergeNodes (r2, r1)
776 | _ => raise Contradiction
777 end
779 778
780 and mergeNodes (r1, r2) = 779 and mergeNodes (r1, r2) =
781 (#Rep (unNode r1) := SOME r2; 780 (#Rep (unNode r1) := SOME r2;
782 if !(#Known (unNode r1)) then 781 if !(#Known (unNode r1)) then
783 markKnown r2 782 markKnown r2
868 orelse case #Variety (unNode d) of 867 orelse case #Variety (unNode d) of
869 Dt0 _ => true 868 Dt0 _ => true
870 | Dt1 (_, d) => loop d 869 | Dt1 (_, d) => loop d
871 | Prim _ => true 870 | Prim _ => true
872 | Recrd (xes, _) => List.all loop (SM.listItems (!xes)) 871 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
873 | VFinish => true
874 | Nothing => false 872 | Nothing => false
875 end 873 end
876 in 874 in
877 loop (representative (db, d)) 875 loop (representative (db, d))
878 end 876 end
896 | Cond x => k [ACond x] 894 | Cond x => k [ACond x]
897 in 895 in
898 decomp 896 decomp
899 end 897 end
900 898
899 val tabs = ref (SM.empty : (string list * string list list) SM.map)
900
901 fun imply (hyps, goals, outs) = 901 fun imply (hyps, goals, outs) =
902 let 902 let
903 fun gls goals onFail acc = 903 fun gls goals onFail acc =
904 case goals of 904 case goals of
905 [] => 905 [] =>
906 (let 906 (let
907 val cc = Cc.database () 907 val cc = Cc.database ()
908 val () = app (fn a => Cc.assert (cc, a)) hyps 908 val () = app (fn a => Cc.assert (cc, a)) hyps
909
910 (* Take advantage of table key information *)
911 fun findKeys hyps =
912 case hyps of
913 [] => ()
914 | AReln (Sql tab, [r1]) :: hyps =>
915 (case SM.find (!tabs, tab) of
916 NONE => findKeys hyps
917 | SOME (_, []) => findKeys hyps
918 | SOME (_, ks) =>
919 let
920 fun finder hyps =
921 case hyps of
922 [] => ()
923 | AReln (Sql tab', [r2]) :: hyps =>
924 (if tab' = tab andalso
925 List.exists (List.all (fn f =>
926 let
927 val r =
928 Cc.check (cc,
929 AReln (Eq, [Proj (r1, f),
930 Proj (r2, f)]))
931 in
932 (*Print.prefaces "Fs"
933 [("tab",
934 Print.PD.string tab),
935 ("r1",
936 p_exp (Proj (r1, f))),
937 ("r2",
938 p_exp (Proj (r2, f))),
939 ("r",
940 Print.PD.string
941 (Bool.toString r))];*)
942 r
943 end)) ks then
944 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
945 ("r1", p_exp r1),
946 ("r2", p_exp r2),
947 ("rp1", Cc.p_repOf cc r1),
948 ("rp2", Cc.p_repOf cc r2)];*)
949 Cc.assert (cc, AReln (Eq, [r1, r2])))
950 else
951 ();
952 finder hyps)
953 | _ :: hyps => finder hyps
954 in
955 finder hyps;
956 findKeys hyps
957 end)
958 | _ :: hyps => findKeys hyps
909 in 959 in
960 findKeys hyps;
961
910 (*Print.preface ("db", Cc.p_database cc);*) 962 (*Print.preface ("db", Cc.p_database cc);*)
911 (List.all (fn a => 963 (List.all (fn a =>
912 if Cc.check (cc, a) then 964 if Cc.check (cc, a) then
913 true 965 true
914 else 966 else
1832 Delete = #Delete t, 1884 Delete = #Delete t,
1833 Update = c :: #Update t} 1885 Update = c :: #Update t}
1834 1886
1835 end 1887 end
1836 1888
1837 val tabs = ref (SM.empty : string list SM.map)
1838
1839 fun evalExp env (e as (_, loc), st) = 1889 fun evalExp env (e as (_, loc), st) =
1840 let 1890 let
1841 fun default () = 1891 fun default () =
1842 let 1892 let
1843 val (st, nv) = St.nextVar st 1893 val (st, nv) = St.nextVar st
2139 in 2189 in
2140 ((x, e), st) 2190 ((x, e), st)
2141 end) 2191 end)
2142 st fs 2192 st fs
2143 2193
2144 val fs' = case SM.find (!tabs, "uw_" ^ tab) of 2194 val fs' = case SM.find (!tabs, tab) of
2145 NONE => raise Fail "Iflow.evalExp: Updating unknown table" 2195 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
2146 | SOME fs' => fs' 2196 | SOME (fs', _) => fs'
2147 2197
2148 val fs = foldl (fn (f, fs) => 2198 val fs = foldl (fn (f, fs) =>
2149 if List.exists (fn (f', _) => f' = f) fs then 2199 if List.exists (fn (f', _) => f' = f) fs then
2150 fs 2200 fs
2151 else 2201 else
2198 DExport (_, _, n, _, _, _) => IS.add (exptd, n) 2248 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
2199 | _ => exptd) IS.empty file 2249 | _ => exptd) IS.empty file
2200 2250
2201 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) = 2251 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
2202 case d of 2252 case d of
2203 DTable (tab, fs, _, _) => 2253 DTable (tab, fs, pk, _) =>
2204 (tabs := SM.insert (!tabs, tab, map #1 fs); 2254 let
2205 (vals, inserts, deletes, updates, client, insert, delete, update)) 2255 val ks =
2256 case #1 pk of
2257 EPrim (Prim.String s) =>
2258 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
2259 [] => []
2260 | pk => [pk])
2261 | _ => []
2262 in
2263 if size tab >= 3 then
2264 (tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
2265 (map #1 fs,
2266 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
2267 ^ String.extract (s, 4, NONE))) ks));
2268 (vals, inserts, deletes, updates, client, insert, delete, update))
2269 else
2270 raise Fail "Table name does not begin with uw_"
2271 end
2206 | DVal (_, n, _, e, _) => 2272 | DVal (_, n, _, e, _) =>
2207 let 2273 let
2208 val isExptd = IS.member (exptd, n) 2274 val isExptd = IS.member (exptd, n)
2209 2275
2210 fun deAbs (e, env, nv, p) = 2276 fun deAbs (e, env, nv, p) =