From 1589307fcb887ec55b5baea7445747b479a665d2 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 Dec 2009 14:34:18 -0500 Subject: Fixing a bug in DInitializer elaboration --- lib/ur/top.ur | 3 +++ lib/ur/top.urs | 3 +++ src/elaborate.sml | 4 ++-- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 8b737179..78a799b1 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -271,6 +271,9 @@ fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql None => error Query returned no rows | Some r => r.nm) +fun nonempty [fs] [us] (t : sql_table fs us) = + oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t) + fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] [t ::: Type] (_ : sql_injectable (option t)) (e1 : sql_exp tables agg exps (option t)) diff --git a/lib/ur/top.urs b/lib/ur/top.urs index 59ffec92..57bc2b1e 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -173,6 +173,9 @@ val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type sql_query (mapU [] tabs) [nm = t] -> transaction t +val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us + -> transaction bool + val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> sql_injectable (option t) -> sql_exp tables agg exps (option t) diff --git a/src/elaborate.sml b/src/elaborate.sml index 327004e2..d1b9648a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3671,12 +3671,12 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = end | L.DInitializer e => let - val (e', t, gs) = elabExp (env, denv) e + val (e', t, gs') = elabExp (env, denv) e val t' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc) in checkCon env e' t t'; - ([(L'.DInitializer e', loc)], (env, denv, gs)) + ([(L'.DInitializer e', loc)], (env, denv, gs' @ gs)) end (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) -- cgit v1.2.3