# HG changeset patch # User Adam Chlipala # Date 1241377053 14400 # Node ID 87a7702d681d6a51446d1b194992d23443f73ad2 # Parent 9f2555f06901e5235917744861f439978c18f09e outer demo diff -r 9f2555f06901 -r 87a7702d681d demo/cookie.urp --- a/demo/cookie.urp Sun May 03 12:49:47 2009 -0400 +++ b/demo/cookie.urp Sun May 03 14:57:33 2009 -0400 @@ -1,3 +1,2 @@ -debug cookie diff -r 9f2555f06901 -r 87a7702d681d demo/form.urp --- a/demo/form.urp Sun May 03 12:49:47 2009 -0400 +++ b/demo/form.urp Sun May 03 14:57:33 2009 -0400 @@ -1,3 +1,2 @@ -debug form diff -r 9f2555f06901 -r 87a7702d681d demo/outer.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/outer.ur Sun May 03 14:57:33 2009 -0400 @@ -0,0 +1,35 @@ +table t : { Id : int, B : string } + PRIMARY KEY Id + +table u : { Id : int, Link : int, C : string, D : option float } + PRIMARY KEY Id, + CONSTRAINT Link FOREIGN KEY Link REFERENCES t(Id) + +fun main () = + xml <- queryX (SELECT t.Id, t.B, u.Id, u.C, u.D + FROM t LEFT JOIN u ON t.Id = u.Link) + (fn r => + {[r.T.Id]} + {[r.T.B]} + {[r.U.Id]} + {[r.U.C]} + {[r.U.D]} + ); + return + {xml}
+ +
Insert into t: + +
+ Insert into u: + + +
+ +and addT r = + dml (INSERT INTO t (Id, B) VALUES ({[readError r.Id]}, {[r.B]})); + main () + +and addU r = + dml (INSERT INTO u (Id, Link, C, D) VALUES ({[readError r.Id]}, {[readError r.Link]}, {[r.C]}, {[readError r.D]})); + main () diff -r 9f2555f06901 -r 87a7702d681d demo/outer.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/outer.urp Sun May 03 14:57:33 2009 -0400 @@ -0,0 +1,4 @@ +database dbname=test +sql outer.sql + +outer diff -r 9f2555f06901 -r 87a7702d681d demo/outer.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/outer.urs Sun May 03 14:57:33 2009 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page diff -r 9f2555f06901 -r 87a7702d681d demo/prose --- a/demo/prose Sun May 03 12:49:47 2009 -0400 +++ b/demo/prose Sun May 03 14:57:33 2009 -0400 @@ -135,6 +135,10 @@
  • The FOREIGN KEY constraint declares that a row of the table references a particular column of another table, or of the same table, as we see in this example. It's a static type error to reference a foreign key column that has no PRIMARY KEY or UNIQUE constraint.
    • +outer.urp + +

    SQL outer joins are no problem, as this demo shows. Unlike with SQL, here we have static type inference determining for us which columns may become nullable as a result of an outer join, and the compiler will reject programs that make the wrong assumptions about that process. The details of that nullification don't appear in this example, where the magic of type classes determines both the post-join type of each field and the right pretty-printing and parsing function for each of those types.

    + sum.urp

    Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.

    diff -r 9f2555f06901 -r 87a7702d681d lib/ur/basis.urs --- a/lib/ur/basis.urs Sun May 03 12:49:47 2009 -0400 +++ b/lib/ur/basis.urs Sun May 03 14:57:33 2009 -0400 @@ -70,6 +70,7 @@ val read_string : read string val read_bool : read bool val read_time : read time +val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t (** * Monads *) diff -r 9f2555f06901 -r 87a7702d681d lib/ur/top.ur --- a/lib/ur/top.ur Sun May 03 12:49:47 2009 -0400 +++ b/lib/ur/top.ur Sun May 03 14:57:33 2009 -0400 @@ -71,6 +71,24 @@ fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) +fun show_option (t ::: Type) (_ : show t) = + mkShow (fn opt : option t => + case opt of + None => "" + | Some x => show x) + +fun read_option (t ::: Type) (_ : read t) = + mkRead (fn s => + case s of + "" => None + | _ => Some (readError s : t)) + (fn s => + case s of + "" => Some None + | _ => case read s of + None => None + | v => Some v) + fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = cdata (show v) diff -r 9f2555f06901 -r 87a7702d681d lib/ur/top.urs --- a/lib/ur/top.urs Sun May 03 12:49:47 2009 -0400 +++ b/lib/ur/top.urs Sun May 03 14:57:33 2009 -0400 @@ -39,6 +39,9 @@ val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) +val show_option : t ::: Type -> show t -> show (option t) +val read_option : t ::: Type -> read t -> read (option t) + val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t -> xml ctx use [] diff -r 9f2555f06901 -r 87a7702d681d src/elaborate.sml --- a/src/elaborate.sml Sun May 03 12:49:47 2009 -0400 +++ b/src/elaborate.sml Sun May 03 14:57:33 2009 -0400 @@ -497,24 +497,6 @@ others : L'.con list } - fun normalizeRecordSummary env (r : record_summary) = - let - val (fields, unifs, others) = - foldl (fn (u as (uc, _), (fields, unifs, others)) => - let - val uc' = hnormCon env uc - in - case #1 uc' of - L'.CUnif _ => (fields, u :: unifs, others) - | L'.CRecord (_, fs) => (fs @ fields, unifs, others) - | L'.CConcat ((L'.CRecord (_, fs), _), rest) => (fs @ fields, unifs, rest :: others) - | _ => (fields, unifs, uc' :: others) - end) - (#fields r, [], #others r) (#unifs r) - in - {fields = fields, unifs = unifs, others = others} - end - fun summaryToCon {fields, unifs, others} = let val c = (L'.CRecord (ktype, []), dummy) @@ -639,9 +621,9 @@ val recdCounter = ref 0 val mayDelay = ref false - val delayedUnifs = ref ([] : (E.env * L'.kind * record_summary * record_summary) list) - - fun unifyRecordCons env (c1, c2) = + val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) + + fun unifyRecordCons env (loc, c1, c2) = let fun rkindof c = case hnormKind (kindof env c) of @@ -663,9 +645,12 @@ val r2 = recordSummary env c2 in unifyKinds env k1 k2; - unifySummaries env (k1, r1, r2) + unifySummaries env (loc, k1, r1, r2) end + and normalizeRecordSummary env (r : record_summary) = + recordSummary env (summaryToCon r) + and recordSummary env c = let val c = hnormCon env c @@ -690,18 +675,26 @@ end and consEq env (c1, c2) = - (unifyCons env c1 c2; - true) - handle CUnify _ => false + let + val mayDelay' = !mayDelay + in + (mayDelay := false; + unifyCons env c1 c2; + mayDelay := mayDelay'; + true) + handle CUnify _ => (mayDelay := mayDelay'; false) + end and consNeq env (c1, c2) = case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of (L'.CName x1, L'.CName x2) => x1 <> x2 | _ => false - and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = + and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = let val loc = #2 k + val pdescs = [("#1", p_summary env s1), + ("#2", p_summary env s2)] (*val () = eprefaces "Summaries" [("#1", p_summary env s1), ("#2", p_summary env s2)]*) @@ -791,7 +784,7 @@ | orig => orig (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), - ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) + ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) fun isGuessable (other, fs, unifs) = let @@ -811,13 +804,10 @@ else (fs1, fs2, others1, others2, unifs1, unifs2) | (_, [], [], [other2], _, []) => - if isGuessable (other2, fs1, unifs1) then - ([], [], [], [], [], []) - else - (prefaces "Not guessable" [("other2", p_con env other2), - ("fs1", p_con env (L'.CRecord (k, fs1), loc)), - ("#unifs1", PD.string (Int.toString (length unifs1)))]; - (fs1, fs2, others1, others2, unifs1, unifs2)) + if isGuessable (other2, fs1, unifs1) then + ([], [], [], [], [], []) + else + (fs1, fs2, others1, others2, unifs1, unifs2) | _ => (fs1, fs2, others1, others2, unifs1, unifs2) (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), @@ -826,23 +816,19 @@ val empty = (L'.CRecord (k, []), dummy) fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) in - case (unifs1, fs1, others1, unifs2, fs2, others2) of - (_, [], [], [], [], []) => - app (fn (_, r) => r := SOME empty) unifs1 - | ([], [], [], _, [], []) => - app (fn (_, r) => r := SOME empty) unifs2 - | ([], _, _, _, _ :: _, _) => failure () - | ([], _, _, _, _, _ :: _) => failure () - | (_, _ :: _, _, [], _, _) => failure () - | (_, _, _ :: _, [], _, _) => failure () - | _ => - if !mayDelay then - delayedUnifs := (env, k, s1, s2) :: !delayedUnifs - else - failure () - - (*before eprefaces "Summaries'" [("#1", p_summary env s1), - ("#2", p_summary env s2)]*) + (case (unifs1, fs1, others1, unifs2, fs2, others2) of + (_, [], [], [], [], []) => + app (fn (_, r) => r := SOME empty) unifs1 + | ([], [], [], _, [], []) => + app (fn (_, r) => r := SOME empty) unifs2 + | _ => + if !mayDelay then + delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs + else + failure ()) + + (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), + ("#2", p_summary env (normalizeRecordSummary env s2))]*) end and guessMap env (c1, c2, ex) = @@ -882,11 +868,7 @@ unifyCons env r (L'.CConcat (r1, r2), loc) end | L'.CUnif (_, _, _, ur) => - let - val ur' = cunif (loc, (L'.KRecord dom, loc)) - in - ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc) - end + ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) | _ => raise ex in unfold (r, c) @@ -978,7 +960,7 @@ | _ => onFail ()) | _ => onFail () - fun isRecord' () = unifyRecordCons env (c1All, c2All) + fun isRecord' () = unifyRecordCons env (loc, c1All, c2All) fun isRecord () = case (c1, c2) of @@ -3737,12 +3719,20 @@ val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file - val delayed = !delayedUnifs + fun oneSummaryRound () = + if ErrorMsg.anyErrors () then + () + else + let + val delayed = !delayedUnifs + in + delayedUnifs := []; + app (fn (loc, env, k, s1, s2) => + unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) + delayed + end in - delayedUnifs := []; - app (fn (env, k, s1, s2) => - unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) - delayed; + oneSummaryRound (); if ErrorMsg.anyErrors () then () @@ -3808,7 +3798,7 @@ in case (gs, solved) of ([], _) => () - | (_, true) => solver gs + | (_, true) => (oneSummaryRound (); solver gs) | _ => app (fn Disjoint (loc, env, denv, c1, c2) => ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; @@ -3826,12 +3816,15 @@ mayDelay := false; - app (fn (env, k, s1, s2) => - unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) - handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification"; - cunifyError env err)) - (!delayedUnifs); - delayedUnifs := []; + if ErrorMsg.anyErrors () then + () + else + (app (fn (loc, env, k, s1, s2) => + unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) + handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; + cunifyError env err)) + (!delayedUnifs); + delayedUnifs := []); if ErrorMsg.anyErrors () then () diff -r 9f2555f06901 -r 87a7702d681d src/monoize.sml --- a/src/monoize.sml Sun May 03 12:49:47 2009 -0400 +++ b/src/monoize.sml Sun May 03 14:57:33 2009 -0400 @@ -1036,6 +1036,20 @@ ((L'.EAbs ("f", readType (t, loc), readErrType (t, loc), (L'.EField ((L'.ERel 0, loc), "ReadError"), loc)), loc), fm) end + | L.ECApp ((L.EFfi ("Basis", "mkRead"), _), t) => + let + val t = monoType env t + val b = (L'.TFfi ("Basis", "string"), loc) + val b' = (L'.TOption b, loc) + val dom = (L'.TFun (t, b), loc) + val dom' = (L'.TFun (t, b'), loc) + in + ((L'.EAbs ("f", dom, (L'.TFun (dom', readType (t, loc)), loc), + (L'.EAbs ("f'", dom', readType (t, loc), + (L'.ERecord [("Read", (L'.ERel 0, loc), dom), + ("ReadError", (L'.ERel 1, loc), dom')], loc)), loc)), loc), + fm) + end | L.EFfi ("Basis", "read_int") => let val t = (L'.TFfi ("Basis", "int"), loc)