summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 14:57:33 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 14:57:33 -0400
commite1618fb012b5926889d80893c9ac4ce08838519d (patch)
tree46b157b5c6fb6967e1ab4809f94a6d6505de7411
parentddac92a3d792b7e7342e4003862cd5ff5c1f0ab8 (diff)
outer demo
Diffstat
-rw-r--r--demo/cookie.urp1
-rw-r--r--demo/form.urp1
-rw-r--r--demo/outer.ur35
-rw-r--r--demo/outer.urp4
-rw-r--r--demo/outer.urs1
-rw-r--r--demo/prose4
-rw-r--r--lib/ur/basis.urs1
-rw-r--r--lib/ur/top.ur18
-rw-r--r--lib/ur/top.urs3
-rw-r--r--src/elaborate.sml129
-rw-r--r--src/monoize.sml14
11 files changed, 141 insertions, 70 deletions
diff --git a/demo/cookie.urp b/demo/cookie.urp
index 61a1a1e0..9e283d4b 100644
--- a/demo/cookie.urp
+++ b/demo/cookie.urp
@@ -1,3 +1,2 @@
-debug
cookie
diff --git a/demo/form.urp b/demo/form.urp
index f28331fc..73356d49 100644
--- a/demo/form.urp
+++ b/demo/form.urp
@@ -1,3 +1,2 @@
-debug
form
diff --git a/demo/outer.ur b/demo/outer.ur
new file mode 100644
index 00000000..ac49f475
--- /dev/null
+++ b/demo/outer.ur
@@ -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 => <xml><tr>
+ <td>{[r.T.Id]}</td>
+ <td>{[r.T.B]}</td>
+ <td>{[r.U.Id]}</td>
+ <td>{[r.U.C]}</td>
+ <td>{[r.U.D]}</td>
+ </tr></xml>);
+ return <xml><body>
+ <table>{xml}</table>
+
+ <form>Insert into t: <textbox{#Id} size={5}/> <textbox{#B} size={5}/>
+ <submit action={addT}/></form>
+ <form>
+ Insert into u: <textbox{#Id} size={5}/> <textbox{#Link} size={5}/> <textbox{#C} size={5}/>
+ <textbox{#D} size={5}/> <submit action={addU}/>
+ </form>
+ </body></xml>
+
+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 --git a/demo/outer.urp b/demo/outer.urp
new file mode 100644
index 00000000..994c3e1a
--- /dev/null
+++ b/demo/outer.urp
@@ -0,0 +1,4 @@
+database dbname=test
+sql outer.sql
+
+outer
diff --git a/demo/outer.urs b/demo/outer.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/outer.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/prose b/demo/prose
index 2d4f5ea3..2cfbb291 100644
--- a/demo/prose
+++ b/demo/prose
@@ -135,6 +135,10 @@ constraints.urp
<li>The <tt>FOREIGN KEY</tt> 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 <tt>PRIMARY KEY</tt> or <tt>UNIQUE</tt> constraint.</li>
</ol>
+outer.urp
+
+<p>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.</p>
+
sum.urp
<p>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.</p>
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index ea4432cd..9736ce1e 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -70,6 +70,7 @@ val read_float : read float
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 --git a/lib/ur/top.ur b/lib/ur/top.ur
index b9728158..f9b3d033 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -71,6 +71,24 @@ fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf =
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 --git a/lib/ur/top.urs b/lib/ur/top.urs
index 60b6dac2..4ed64075 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -39,6 +39,9 @@ val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
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 --git a/src/elaborate.sml b/src/elaborate.sml
index b9378e1b..38696976 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -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)
+ val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list)
- fun unifyRecordCons env (c1, c2) =
+ 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 @@ fun elabFile basis topStr topSgn env file =
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 @@ fun elabFile basis topStr topSgn env file =
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 @@ fun elabFile basis topStr topSgn env file =
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 --git a/src/monoize.sml b/src/monoize.sml
index 4b6b3c5f..b71b13a5 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1036,6 +1036,20 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
((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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 02:00:59 +0000