Mercurial > urweb
changeset 705:e6706a1df013
Track uniqueness sets in table types
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 07 Apr 2009 14:11:32 -0400 |
| parents | 70cbdcf5989b |
| children | 1fb318c17546 |
| files | lib/ur/basis.urs src/core.sml src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/defunc.sig src/defunc.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/explify.sml src/monoize.sml src/reduce.sml src/shake.sml src/sources src/urweb.grm tests/cst.ur |
| diffstat | 23 files changed, 263 insertions(+), 503 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Apr 07 12:24:31 2009 -0400 +++ b/lib/ur/basis.urs Tue Apr 07 14:11:32 2009 -0400 @@ -122,20 +122,27 @@ (** SQL *) -con sql_table :: {Type} -> Type +con sql_table :: {Type} -> {{Unit}} -> Type (*** Constraints *) -con sql_constraints :: {Unit} -> {Type} -> Type -con sql_constraint :: {Type} -> Type +con sql_constraints :: {Type} -> {{Unit}} -> Type +(* Arguments: column types, uniqueness implications of constraints *) -val no_constraint : fs ::: {Type} -> sql_constraints [] fs -val one_constraint : fs ::: {Type} -> name :: Name -> sql_constraint fs -> sql_constraints [name] fs -val join_constraints : names1 ::: {Unit} -> names2 ::: {Unit} -> fs ::: {Type} -> [names1 ~ names2] - => sql_constraints names1 fs -> sql_constraints names2 fs - -> sql_constraints (names1 ++ names2) fs +con sql_constraint :: {Type} -> {Unit} -> Type -val unique : rest ::: {Type} -> unique :: {Type} -> [unique ~ rest] => sql_constraint (unique ++ rest) +val no_constraint : fs ::: {Type} -> sql_constraints fs [] +val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name + -> sql_constraint fs unique + -> sql_constraints fs [name = unique] +val join_constraints : fs ::: {Type} + -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2] + => sql_constraints fs uniques1 -> sql_constraints fs uniques2 + -> sql_constraints fs (uniques1 ++ uniques2) + +val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type} + -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest] + => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique) (*** Queries *) @@ -151,17 +158,18 @@ (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop) val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables -val sql_query1 : tables ::: {{Type}} +val sql_query1 : tables ::: {({Type} * {{Unit}})} -> grouped ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} - -> {From : $(map sql_table tables), - Where : sql_exp tables [] [] bool, - GroupBy : sql_subset tables grouped, - Having : sql_exp grouped tables [] bool, + -> {From : $(map (fn p :: ({Type} * {{Unit}}) => sql_table p.1 p.2) tables), + Where : sql_exp (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] [] bool, + GroupBy : sql_subset (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) grouped, + Having : sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] bool, SelectFields : sql_subset grouped selectedFields, - SelectExps : $(map (sql_exp grouped tables []) selectedExps) } - -> sql_query1 tables selectedFields selectedExps + SelectExps : $(map (sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) []) + selectedExps) } + -> sql_query1 (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) selectedFields selectedExps type sql_relop val sql_union : sql_relop @@ -321,20 +329,20 @@ type dml val dml : dml -> transaction unit -val insert : fields ::: {Type} - -> sql_table fields +val insert : fields ::: {Type} -> uniques ::: {{Unit}} + -> sql_table fields uniques -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) -> dml -val update : unchanged ::: {Type} -> changed :: {Type} -> +val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> [changed ~ unchanged] => $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) - -> sql_table (changed ++ unchanged) + -> sql_table (changed ++ unchanged) uniques -> sql_exp [T = changed ++ unchanged] [] [] bool -> dml -val delete : fields ::: {Type} - -> sql_table fields +val delete : fields ::: {Type} -> uniques ::: {{Unit}} + -> sql_table fields uniques -> sql_exp [T = fields] [] [] bool -> dml
--- a/src/core.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/core.sml Tue Apr 07 14:11:32 2009 -0400 @@ -130,7 +130,7 @@ | DVal of string * int * con * exp * string | DValRec of (string * int * con * exp * string) list | DExport of export_kind * int - | DTable of string * int * con * string * exp + | DTable of string * int * con * string * exp * con | DSequence of string * int * string | DDatabase of string | DCookie of string * int * con * string
--- a/src/core_env.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/core_env.sml Tue Apr 07 14:11:32 2009 -0400 @@ -313,11 +313,13 @@ | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env - | DTable (x, n, c, s, _) => + | DTable (x, n, c, s, _, cc) => let - val t = (CApp ((CFfi ("Basis", "sql_table"), loc), c), loc) + val ct = (CFfi ("Basis", "sql_table"), loc) + val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, cc), loc) in - pushENamed env x n t NONE s + pushENamed env x n ct NONE s end | DSequence (x, n, s) => let
--- a/src/core_print.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/core_print.sml Tue Apr 07 14:11:32 2009 -0400 @@ -546,21 +546,21 @@ space, (p_con env (#2 (E.lookupENamed env n)) handle E.UnboundNamed _ => string "UNBOUND")] - | DTable (x, n, c, s, e) => box [string "table", - space, - p_named x n, - space, - string "as", - space, - string s, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (x, n, c, s, e, _) => box [string "table", + space, + p_named x n, + space, + string "as", + space, + string s, + space, + string ":", + space, + p_con env c, + space, + string "constraints", + space, + p_exp env e] | DSequence (x, n, s) => box [string "sequence", space, p_named x n,
--- a/src/core_util.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/core_util.sml Tue Apr 07 14:11:32 2009 -0400 @@ -933,12 +933,14 @@ (DValRec vis', loc)) end | DExport _ => S.return2 dAll - | DTable (x, n, c, s, e) => + | DTable (x, n, c, s, e, cc) => S.bind2 (mfc ctx c, fn c' => - S.map2 (mfe ctx e, + S.bind2 (mfe ctx e, fn e' => - (DTable (x, n, c', s, e'), loc))) + S.map2 (mfc ctx cc, + fn cc' => + (DTable (x, n, c', s, e', cc'), loc)))) | DSequence _ => S.return2 dAll | DDatabase _ => S.return2 dAll | DCookie (x, n, c, s) => @@ -1060,11 +1062,14 @@ foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis | DExport _ => ctx - | DTable (x, n, c, s, _) => + | DTable (x, n, c, s, _, cc) => let - val t = (CApp ((CFfi ("Basis", "sql_table"), #2 d'), c), #2 d') + val loc = #2 d' + val ct = (CFfi ("Basis", "sql_table"), loc) + val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, cc), loc) in - bind (ctx, NamedE (x, n, t, NONE, s)) + bind (ctx, NamedE (x, n, ct, NONE, s)) end | DSequence (x, n, s) => let @@ -1136,7 +1141,7 @@ | DVal (_, n, _, _, _) => Int.max (n, count) | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis | DExport _ => count - | DTable (_, n, _, _, _) => Int.max (n, count) + | DTable (_, n, _, _, _, _) => Int.max (n, count) | DSequence (_, n, _) => Int.max (n, count) | DDatabase _ => count | DCookie (_, n, _, _) => Int.max (n, count)) 0
--- a/src/corify.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/corify.sml Tue Apr 07 14:11:32 2009 -0400 @@ -976,12 +976,12 @@ end | _ => raise Fail "Non-const signature for 'export'") - | L.DTable (_, x, n, c, e) => + | L.DTable (_, x, n, c, e, cc) => let val (st, n) = St.bindVal st x n val s = relify (doRestify (mods, x)) in - ([(L'.DTable (x, n, corifyCon st c, s, corifyExp st e), loc)], st) + ([(L'.DTable (x, n, corifyCon st c, s, corifyExp st e, corifyCon st cc), loc)], st) end | L.DSequence (_, x, n) => let @@ -1052,7 +1052,7 @@ | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) | L.DFfiStr (_, n', _) => Int.max (n, n') | L.DExport _ => n - | L.DTable (_, _, n', _, _) => Int.max (n, n') + | L.DTable (_, _, n', _, _, _) => Int.max (n, n') | L.DSequence (_, _, n') => Int.max (n, n') | L.DDatabase _ => n | L.DCookie (_, _, n', _) => Int.max (n, n'))
--- a/src/defunc.sig Tue Apr 07 12:24:31 2009 -0400 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* Copyright (c) 2008, Adam Chlipala - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * - Redistributions of source code must retain the above copyright notice, - * this list of conditions and the following disclaimer. - * - Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - The names of contributors may not be used to endorse or promote products - * derived from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - *) - -signature DEFUNC = sig - - val defunc : Core.file -> Core.file - -end
--- a/src/defunc.sml Tue Apr 07 12:24:31 2009 -0400 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,260 +0,0 @@ -(* Copyright (c) 2008, Adam Chlipala - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * - Redistributions of source code must retain the above copyright notice, - * this list of conditions and the following disclaimer. - * - Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - The names of contributors may not be used to endorse or promote products - * derived from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - *) - -structure Defunc :> DEFUNC = struct - -open Core - -structure E = CoreEnv -structure U = CoreUtil - -structure IS = IntBinarySet - -val functionInside = U.Con.exists {kind = fn _ => false, - con = fn TFun _ => true - | CFfi ("Basis", "transaction") => true - | _ => false} - -val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs, - con = fn (_, _, xs) => xs, - exp = fn (bound, e, xs) => - case e of - ERel x => - if x >= bound then - IS.add (xs, x - bound) - else - xs - | _ => xs, - bind = fn (bound, b) => - case b of - U.Exp.RelE _ => bound + 1 - | _ => bound} - 0 IS.empty - -fun positionOf (v : int, ls) = - let - fun pof (pos, ls) = - case ls of - [] => raise Fail "Defunc.positionOf" - | v' :: ls' => - if v = v' then - pos - else - pof (pos + 1, ls') - in - pof (0, ls) - end - -fun squish fvs = - U.Exp.mapB {kind = fn _ => fn k => k, - con = fn _ => fn c => c, - exp = fn bound => fn e => - case e of - ERel x => - if x >= bound then - ERel (positionOf (x - bound, fvs) + bound) - else - e - | _ => e, - bind = fn (bound, b) => - case b of - U.Exp.RelE _ => bound + 1 - | _ => bound} - 0 - -fun default (_, x, st) = (x, st) - -datatype 'a search = - Yes - | No - | Maybe of 'a - -structure EK = struct -type ord_key = exp -val compare = U.Exp.compare -end - -structure EM = BinaryMapFn(EK) - -type state = { - maxName : int, - funcs : int EM.map, - vis : (string * int * con * exp * string) list -} - -fun exp (env, e, st) = - case e of - ERecord xes => - let - val (xes, st) = - ListUtil.foldlMap - (fn (tup as (fnam as (CName x, loc), e, xt), st) => - if (x <> "Link" andalso x <> "Action") - orelse case #1 e of - ENamed _ => true - | _ => false then - (tup, st) - else - let - fun needsAttention (e, _) = - case e of - ENamed f => Maybe (#2 (E.lookupENamed env f)) - | EApp (f, _) => - (case needsAttention f of - No => No - | Yes => Yes - | Maybe t => - case t of - (TFun (dom, _), _) => - if functionInside dom then - Yes - else - No - | _ => No) - | _ => No - - fun headSymbol (e, _) = - case e of - ENamed f => f - | EApp (e, _) => headSymbol e - | _ => raise Fail "Defunc: headSymbol" - - fun rtype (e, _) = - case e of - ENamed f => #2 (E.lookupENamed env f) - | EApp (f, _) => - (case rtype f of - (TFun (_, ran), _) => ran - | _ => raise Fail "Defunc: rtype [1]") - | _ => raise Fail "Defunc: rtype [2]" - in - (*Print.prefaces "Found one!" - [("e", CorePrint.p_exp env e)];*) - case needsAttention e of - Yes => - let - (*val () = print "Yes\n"*) - val f = headSymbol e - - val fvs = IS.listItems (freeVars e) - - val e = squish fvs e - val (e, t) = foldl (fn (n, (e, t)) => - let - val (x, xt) = E.lookupERel env n - in - ((EAbs (x, xt, t, e), loc), - (TFun (xt, t), loc)) - end) - (e, rtype e) fvs - - val (f', st) = - case EM.find (#funcs st, e) of - SOME f' => (f', st) - | NONE => - let - val (fx, _, _, tag) = E.lookupENamed env f - val f' = #maxName st - - val vi = (fx, f', t, e, tag) - in - (f', {maxName = f' + 1, - funcs = EM.insert (#funcs st, e, f'), - vis = vi :: #vis st}) - end - - val e = foldr (fn (n, e) => - (EApp (e, (ERel n, loc)), loc)) - (ENamed f', loc) fvs - in - (*app (fn n => Print.prefaces - "Free" - [("n", CorePrint.p_exp env (ERel n, ErrorMsg.dummySpan))]) - fvs; - Print.prefaces "Squished" - [("e", CorePrint.p_exp CoreEnv.empty e)];*) - - ((fnam, e, xt), st) - end - | _ => (tup, st) - end - | (tup, st) => (tup, st)) - st xes - in - (ERecord xes, st) - end - | _ => (e, st) - -fun bind (env, b) = - case b of - U.Decl.RelK x => E.pushKRel env x - | U.Decl.RelC (x, k) => E.pushCRel env x k - | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co - | U.Decl.RelE (x, t) => E.pushERel env x t - | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s - -fun doDecl env = U.Decl.foldMapB {kind = default, - con = default, - exp = exp, - decl = default, - bind = bind} - env - -fun defunc file = - let - fun doDecl' (d, (env, st)) = - let - val env = E.declBinds env d - - val (d, st) = doDecl env st d - - val ds = - case #vis st of - [] => [d] - | vis => - case d of - (DValRec vis', loc) => [(DValRec (vis' @ vis), loc)] - | _ => [(DValRec vis, #2 d), d] - in - (ds, - (env, - {maxName = #maxName st, - funcs = #funcs st, - vis = []})) - end - - val (file, _) = ListUtil.foldlMapConcat doDecl' - (E.empty, - {maxName = U.File.maxName file + 1, - funcs = EM.empty, - vis = []}) - file - in - file - end - -end
--- a/src/elab.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elab.sml Tue Apr 07 14:11:32 2009 -0400 @@ -166,7 +166,7 @@ | DFfiStr of string * int * sgn | DConstraint of con * con | DExport of int * sgn * str - | DTable of int * string * int * con * exp + | DTable of int * string * int * con * exp * con | DSequence of int * string * int | DClass of string * int * kind * con | DDatabase of string
--- a/src/elab_env.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elab_env.sml Tue Apr 07 14:11:32 2009 -0400 @@ -1532,11 +1532,13 @@ | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn | DConstraint _ => env | DExport _ => env - | DTable (tn, x, n, c, _) => + | DTable (tn, x, n, c, _, cc) => let - val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc) + val ct = (CModProj (tn, [], "sql_table"), loc) + val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, cc), loc) in - pushENamedAs env x n t + pushENamedAs env x n ct end | DSequence (tn, x, n) => let
--- a/src/elab_print.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elab_print.sml Tue Apr 07 14:11:32 2009 -0400 @@ -740,17 +740,17 @@ string ":", space, p_sgn env sgn] - | DTable (_, x, n, c, e) => box [string "table", - space, - p_named x n, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (_, x, n, c, e, _) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c, + space, + string "constraints", + space, + p_exp env e] | DSequence (_, x, n) => box [string "sequence", space, p_named x n]
--- a/src/elab_util.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elab_util.sml Tue Apr 07 14:11:32 2009 -0400 @@ -766,9 +766,14 @@ bind (ctx, Str (x, sgn)) | DConstraint _ => ctx | DExport _ => ctx - | DTable (tn, x, n, c, _) => - bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc), - c), loc))) + | DTable (tn, x, n, c, _, cc) => + let + val ct = (CModProj (n, [], "sql_table"), loc) + val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, cc), loc) + in + bind (ctx, NamedE (x, ct)) + end | DSequence (tn, x, n) => bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) | DClass (x, n, k, _) => @@ -864,12 +869,14 @@ fn str' => (DExport (en, sgn', str'), loc))) - | DTable (tn, x, n, c, e) => + | DTable (tn, x, n, c, e, cc) => S.bind2 (mfc ctx c, fn c' => - S.map2 (mfe ctx e, + S.bind2 (mfe ctx e, fn e' => - (DTable (tn, x, n, c', e'), loc))) + S.map2 (mfc ctx cc, + fn cc' => + (DTable (tn, x, n, c', e', cc'), loc)))) | DSequence _ => S.return2 dAll | DClass (x, n, k, c) => @@ -1020,7 +1027,7 @@ | DConstraint _ => 0 | DClass (_, n, _, _) => n | DExport _ => 0 - | DTable (n1, _, n2, _, _) => Int.max (n1, n2) + | DTable (n1, _, n2, _, _, _) => Int.max (n1, n2) | DSequence (n1, _, n2) => Int.max (n1, n2) | DDatabase _ => 0 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
--- a/src/elaborate.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/elaborate.sml Tue Apr 07 14:11:32 2009 -0400 @@ -880,88 +880,6 @@ (L'.CError, _) => () | (_, L'.CError) => () - | (L'.CRecord _, _) => isRecord () - | (_, L'.CRecord _) => isRecord () - | (L'.CConcat _, _) => isRecord () - | (_, L'.CConcat _) => isRecord () - - | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => - if r1 = r2 then - () - else - (unifyKinds env k1 k2; - r1 := SOME c2All) - - | (L'.CUnif (_, _, _, r), _) => - if occursCon r c2All then - err COccursCheckFailed - else - r := SOME c2All - | (_, L'.CUnif (_, _, _, r)) => - if occursCon r c1All then - err COccursCheckFailed - else - r := SOME c1All - - | (L'.CUnit, L'.CUnit) => () - - | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => - (unifyCons' env d1 d2; - unifyCons' env r1 r2) - | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => - if expl1 <> expl2 then - err CExplicitness - else - (unifyKinds env d1 d2; - let - (*val befor = Time.now ()*) - val env' = E.pushCRel env x1 d1 - in - (*TextIO.print ("E.pushCRel: " - ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) - ^ "\n");*) - unifyCons' env' r1 r2 - end) - | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 - | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => - (unifyCons' env c1 c2; - unifyCons' env d1 d2; - unifyCons' env e1 e2) - - | (L'.CRel n1, L'.CRel n2) => - if n1 = n2 then - () - else - err CIncompatible - | (L'.CNamed n1, L'.CNamed n2) => - if n1 = n2 then - () - else - err CIncompatible - - | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => - (unifyCons' env d1 d2; - unifyCons' env r1 r2) - | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => - (unifyKinds env k1 k2; - unifyCons' (E.pushCRel env x1 k1) c1 c2) - - | (L'.CName n1, L'.CName n2) => - if n1 = n2 then - () - else - err CIncompatible - - | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => - if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then - () - else - err CIncompatible - - | (L'.CTuple cs1, L'.CTuple cs2) => - ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) - handle ListPair.UnequalLengths => err CIncompatible) - | (L'.CProj (c1, n1), _) => let fun trySnd () = @@ -1020,6 +938,88 @@ | _ => err CIncompatible) | _ => err CIncompatible) + | (L'.CRecord _, _) => isRecord () + | (_, L'.CRecord _) => isRecord () + | (L'.CConcat _, _) => isRecord () + | (_, L'.CConcat _) => isRecord () + + | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => + if r1 = r2 then + () + else + (unifyKinds env k1 k2; + r1 := SOME c2All) + + | (L'.CUnif (_, _, _, r), _) => + if occursCon r c2All then + err COccursCheckFailed + else + r := SOME c2All + | (_, L'.CUnif (_, _, _, r)) => + if occursCon r c1All then + err COccursCheckFailed + else + r := SOME c1All + + | (L'.CUnit, L'.CUnit) => () + + | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => + if expl1 <> expl2 then + err CExplicitness + else + (unifyKinds env d1 d2; + let + (*val befor = Time.now ()*) + val env' = E.pushCRel env x1 d1 + in + (*TextIO.print ("E.pushCRel: " + ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) + ^ "\n");*) + unifyCons' env' r1 r2 + end) + | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 + | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => + (unifyCons' env c1 c2; + unifyCons' env d1 d2; + unifyCons' env e1 e2) + + | (L'.CRel n1, L'.CRel n2) => + if n1 = n2 then + () + else + err CIncompatible + | (L'.CNamed n1, L'.CNamed n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => + (unifyKinds env k1 k2; + unifyCons' (E.pushCRel env x1 k1) c1 c2) + + | (L'.CName n1, L'.CName n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => + if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then + () + else + err CIncompatible + + | (L'.CTuple cs1, L'.CTuple cs2) => + ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) + handle ListPair.UnequalLengths => err CIncompatible) + | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => (unifyKinds env dom1 dom2; unifyKinds env ran1 ran2) @@ -2319,7 +2319,8 @@ | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] - | L'.DTable (tn, x, n, c, _) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] + | L'.DTable (tn, x, n, c, _, cc) => + [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), loc)), loc)] | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] | L'.DDatabase _ => [] @@ -3268,17 +3269,22 @@ | L.DTable (x, c, e) => let val (c', k, gs') = elabCon (env, denv) c - val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) + val uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)) + + val ct = tableOf () + val ct = (L'.CApp (ct, c'), loc) + val ct = (L'.CApp (ct, uniques), loc) + + val (env, n) = E.pushENamed env x ct val (e', et, gs'') = elabExp (env, denv) e - val names = cunif (loc, (L'.KRecord (L'.KUnit, loc), loc)) val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) - val cst = (L'.CApp (cst, names), loc) val cst = (L'.CApp (cst, c'), loc) + val cst = (L'.CApp (cst, uniques), loc) in checkKind env c' k (L'.KRecord (L'.KType, loc), loc); checkCon env e' et cst; - ([(L'.DTable (!basis_r, x, n, c', e'), loc)], (env, denv, gs'' @ enD gs' @ gs)) + ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs)) end | L.DSequence x => let
--- a/src/expl.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/expl.sml Tue Apr 07 14:11:32 2009 -0400 @@ -141,7 +141,7 @@ | DStr of string * int * sgn * str | DFfiStr of string * int * sgn | DExport of int * sgn * str - | DTable of int * string * int * con * exp + | DTable of int * string * int * con * exp * con | DSequence of int * string * int | DDatabase of string | DCookie of int * string * int * con
--- a/src/expl_env.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/expl_env.sml Tue Apr 07 14:11:32 2009 -0400 @@ -298,11 +298,13 @@ | DStr (x, n, sgn, _) => pushStrNamed env x n sgn | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn | DExport _ => env - | DTable (tn, x, n, c, _) => + | DTable (tn, x, n, c, _, cc) => let - val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc) + val ct = (CModProj (tn, [], "sql_table"), loc) + val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, cc), loc) in - pushENamed env x n t + pushENamed env x n ct end | DSequence (tn, x, n) => let
--- a/src/expl_print.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/expl_print.sml Tue Apr 07 14:11:32 2009 -0400 @@ -663,17 +663,17 @@ string ":", space, p_sgn env sgn] - | DTable (_, x, n, c, e) => box [string "table", - space, - p_named x n, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (_, x, n, c, e, _) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c, + space, + string "constraints", + space, + p_exp env e] | DSequence (_, x, n) => box [string "sequence", space, p_named x n]
--- a/src/explify.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/explify.sml Tue Apr 07 14:11:32 2009 -0400 @@ -178,7 +178,7 @@ | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc) | L.DConstraint (c1, c2) => NONE | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc) - | L.DTable (nt, x, n, c, e) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e), loc) + | L.DTable (nt, x, n, c, e, cc) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e, explifyCon cc), loc) | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc) | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
--- a/src/monoize.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/monoize.sml Tue Apr 07 14:11:32 2009 -0400 @@ -139,7 +139,7 @@ (L'.TSignal (mt env dtmap t), loc) | L.CApp ((L.CFfi ("Basis", "http_cookie"), _), _) => (L'.TFfi ("Basis", "string"), loc) - | L.CApp ((L.CFfi ("Basis", "sql_table"), _), _) => + | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_table"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CFfi ("Basis", "sql_sequence") => (L'.TFfi ("Basis", "string"), loc) @@ -151,7 +151,7 @@ (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraints"), _), _), _), _) => (L'.TFfi ("Basis", "sql_constraints"), loc) - | L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _) => + | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_subset"), _), _), _), _) => @@ -1162,13 +1162,19 @@ | L.ECApp ((L.EFfi ("Basis", "no_constraint"), _), _) => ((L'.ERecord [], loc), fm) - | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "one_constraint"), _), _), _), (L.CName name, _)) => + | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "one_constraint"), _), _), _), _), _), (L.CName name, _)) => ((L'.EAbs ("c", (L'.TFfi ("Basis", "string"), loc), (L'.TFfi ("Basis", "sql_constraints"), loc), (L'.ERecord [(name, (L'.ERel 0, loc), (L'.TFfi ("Basis", "string"), loc))], loc)), loc), fm) - | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "join_constraints"), _), _), _), _), _), _) => + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "join_constraints"), _), + _), _), + _), _), + _) => let val constraints = (L'.TFfi ("Basis", "sql_constraints"), loc) in @@ -1178,12 +1184,18 @@ fm) end - | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "unique"), _), _), _), - (L.CRecord (_, unique), _)) => - ((L'.EPrim (Prim.String ("UNIQUE (" - ^ String.concatWith ", " (map (fn (x, _) => "uw_" ^ monoName env x) unique) - ^ ")")), loc), - fm) + | L.ECApp ( + (L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "unique"), _), _), _), t), _), + nm), _), + (L.CRecord (_, unique), _)) => + let + val unique = (nm, t) :: unique + in + ((L'.EPrim (Prim.String ("UNIQUE (" + ^ String.concatWith ", " (map (fn (x, _) => "uw_" ^ monoName env x) unique) + ^ ")")), loc), + fm) + end | L.EFfiApp ("Basis", "dml", [e]) => let @@ -1193,7 +1205,7 @@ fm) end - | L.ECApp ((L.EFfi ("Basis", "insert"), _), fields) => + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "insert"), _), fields), _), _) => (case monoType env (L.TRecord fields, loc) of (L'.TRecord fields, _) => let @@ -1217,7 +1229,7 @@ end | _ => poly ()) - | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), _), _), changed) => + | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), _), _), _), _), changed) => (case monoType env (L.TRecord changed, loc) of (L'.TRecord changed, _) => let @@ -1246,7 +1258,7 @@ end | _ => poly ()) - | L.ECApp ((L.EFfi ("Basis", "delete"), _), _) => + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "delete"), _), _), _), _) => let val s = (L'.TFfi ("Basis", "string"), loc) fun sc s = (L'.EPrim (Prim.String s), loc) @@ -1348,6 +1360,12 @@ val un = (L'.TRecord [], loc) fun gf s = (L'.EField ((L'.ERel 0, loc), s), loc) + val tables = List.mapPartial + (fn (x, (L.CTuple [y, _], _)) => SOME (x, y) + | _ => (E.errorAt loc "Bad sql_query1 tables pair"; + NONE)) + tables + fun doTables tables = let val tables = map (fn ((L.CName x, _), xts) => @@ -2481,7 +2499,7 @@ in SOME (env, fm, [(L'.DExport (ek, s, n, ts, ran), loc)]) end - | L.DTable (x, n, (L.CRecord (_, xts), _), s, e) => + | L.DTable (x, n, (L.CRecord (_, xts), _), s, e, _) => let val t = (L.CFfi ("Basis", "string"), loc) val t' = (L'.TFfi ("Basis", "string"), loc) @@ -2615,7 +2633,7 @@ in foldl (fn ((d, _), e) => case d of - L.DTable (_, _, xts, tab, _) => doTable (tab, #1 xts, e) + L.DTable (_, _, xts, tab, _, _) => doTable (tab, #1 xts, e) | _ => e) e file end @@ -2660,7 +2678,7 @@ in foldl (fn ((d, _), e) => case d of - L.DTable (_, _, xts, tab, _) => doTable (tab, #1 xts, e) + L.DTable (_, _, xts, tab, _, _) => doTable (tab, #1 xts, e) | _ => e) e file end
--- a/src/reduce.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/reduce.sml Tue Apr 07 14:11:32 2009 -0400 @@ -461,8 +461,9 @@ ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc), st) | DExport _ => (d, st) - | DTable (s, n, c, s', e) => ((DTable (s, n, con namedC [] c, s', - exp (namedC, namedE) [] e), loc), st) + | DTable (s, n, c, s', e, cc) => ((DTable (s, n, con namedC [] c, s', + exp (namedC, namedE) [] e, + con namedC [] cc), loc), st) | DSequence _ => (d, st) | DDatabase _ => (d, st) | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
--- a/src/shake.sml Tue Apr 07 12:24:31 2009 -0400 +++ b/src/shake.sml Tue Apr 07 14:11:32 2009 -0400 @@ -59,7 +59,7 @@ val (usedE, usedC, table_cs) = List.foldl (fn ((DExport (_, n), _), (usedE, usedC, table_cs)) => (IS.add (usedE, n), usedE, table_cs) - | ((DTable (_, _, c, _, e), _), (usedE, usedC, table_cs)) => + | ((DTable (_, _, c, _, e, _), _), (usedE, usedC, table_cs)) => let val (usedE, usedC) = usedVars (usedE, usedC) e in @@ -79,7 +79,7 @@ IM.insert (edef, n, (all_ns, t, e))) edef vis) end | ((DExport _, _), acc) => acc - | ((DTable (_, n, c, _, _), _), (cdef, edef)) => + | ((DTable (_, n, c, _, _, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], c, dummye))) | ((DSequence (_, n, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], dummyt, dummye)))
--- a/src/sources Tue Apr 07 12:24:31 2009 -0400 +++ b/src/sources Tue Apr 07 14:11:32 2009 -0400 @@ -105,9 +105,6 @@ especialize.sig especialize.sml -defunc.sig -defunc.sml - rpcify.sig rpcify.sml
--- a/src/urweb.grm Tue Apr 07 12:24:31 2009 -0400 +++ b/src/urweb.grm Tue Apr 07 14:11:32 2009 -0400 @@ -294,9 +294,9 @@ | query1 of exp | tables of (con * exp) list | tname of con - | tnameW of (con * con) - | tnames of con - | tnames' of (con * con) list + | tnameW of con * con + | tnames of (con * con) * (con * con) list + | tnames' of (con * con) * (con * con) list | table of con * exp | tident of con | fident of con @@ -493,7 +493,9 @@ val loc = s (UNIQUEleft, tnamesright) val e = (EVar (["Basis"], "unique", Infer), loc) - val e = (ECApp (e, tnames), loc) + val e = (ECApp (e, #1 (#1 tnames)), loc) + val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc) + val e = (EDisjointApp e, loc) in (EDisjointApp e, loc) end) @@ -505,12 +507,11 @@ (tname, (CWild (KType, loc), loc)) end) -tnames : tnameW (CRecord [tnameW], s (tnameWleft, tnameWright)) - | LPAREN tnames' RPAREN (CRecord tnames', s (LPARENleft, RPARENright)) - | LBRACE LBRACE cexp RBRACE RBRACE (cexp) +tnames : tnameW (tnameW, []) + | LPAREN tnames' RPAREN (tnames') -tnames': tnameW ([tnameW]) - | tnameW COMMA tnames' (tnameW :: tnames') +tnames': tnameW (tnameW, []) + | tnameW COMMA tnames' (#1 tnames', tnameW :: #2 tnames') valis : vali ([vali]) | vali AND valis (vali :: valis)
--- a/tests/cst.ur Tue Apr 07 12:24:31 2009 -0400 +++ b/tests/cst.ur Tue Apr 07 14:11:32 2009 -0400 @@ -4,9 +4,12 @@ CONSTRAINT UniBoth UNIQUE (A, B), CONSTRAINT UniAm UNIQUE {#A}, - CONSTRAINT UniAm2 UNIQUE {{[A = _]}}, - CONSTRAINT UniAm3 {unique [[A = _]] !}, - {{one_constraint [#UniAm4] (unique [[A = _]] !)}} + CONSTRAINT UniAm2 {unique [#A] [[]] ! !}, + {{one_constraint [#UniAm3] (unique [#A] [[]] ! !)}}, + + CONSTRAINT UniBothm UNIQUE ({#A}, {#B}), + CONSTRAINT UniBothm2 {unique [#A] [[B = _]] ! !}, + {{one_constraint [#UniBothm3] (unique [#A] [[B = _]] ! !)}} fun main () : transaction page = queryI (SELECT * FROM t) (fn _ => return ());