From b167bec378ae4577ba2994e0621bf01a44832d34 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 9 Apr 2009 13:59:34 -0400 Subject: More flexible foreign keying --- lib/ur/basis.urs | 12 +++++++++--- src/elab_err.sml | 4 ++-- src/elaborate.sml | 2 +- src/monoize.sml | 49 +++++++++++++++++++++++++++++++++---------------- src/urweb.grm | 1 + tests/cst.ur | 11 +++++++---- 6 files changed, 53 insertions(+), 26 deletions(-) diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 87f20d6b..454b10b2 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -166,13 +166,19 @@ 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) +class linkable :: Type -> Type -> Type +val linkable_same : t ::: Type -> linkable t t +val linkable_from_nullable : t ::: Type -> linkable (option t) t +val linkable_to_nullable : t ::: Type -> linkable t (option t) + con matching :: {Type} -> {Type} -> Type val mat_nil : matching [] [] -val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type} +val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type} -> nm1 :: Name -> nm2 :: Name -> [[nm1] ~ rest1] => [[nm2] ~ rest2] - => matching rest1 rest2 - -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2) + => linkable t1 t2 + -> matching rest1 rest2 + -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2) con propagation_mode :: {Type} -> Type val restrict : fs ::: {Type} -> propagation_mode fs diff --git a/src/elab_err.sml b/src/elab_err.sml index 172f7d37..ee8e1fd0 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -217,7 +217,7 @@ fun expError env err = ("Type", p_con env c)]) co) | Unresolvable (loc, c) => (ErrorMsg.errorAt loc "Can't resolve type class instance"; - eprefaces' [("Class constraint", p_con env c), + eprefaces' [("Class constraint", p_con env c)(*, ("Class database", p_list (fn (c, rules) => box [P.p_con env c, PD.string ":", @@ -227,7 +227,7 @@ fun expError env err = PD.string ":", space, P.p_con env c]) rules]) - (E.listClasses env))]) + (E.listClasses env))*)]) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff --git a/src/elaborate.sml b/src/elaborate.sml index 1323086c..6ee32da1 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -170,7 +170,7 @@ fun cunif (loc, k) = let val n = !count - val s = if n <= 26 then + val s = if n < 26 then str (chr (ord #"A" + n)) else "U" ^ Int.toString (n - 26) diff --git a/src/monoize.sml b/src/monoize.sml index 84707b6e..bc44c550 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -155,6 +155,8 @@ fun monoType env = (L'.TFfi ("Basis", "sql_constraints"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CFfi ("Basis", "linkable"), _), _), _), _) => + (L'.TRecord [], loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "matching"), _), _), _), _) => let val string = (L'.TFfi ("Basis", "string"), loc) @@ -1226,6 +1228,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) = fm) end + | L.ECApp ((L.EFfi ("Basis", "linkable_same"), loc), _) => + ((L'.ERecord [], loc), fm) + | L.ECApp ((L.EFfi ("Basis", "linkable_from_nullable"), loc), _) => + ((L'.ERecord [], loc), fm) + | L.ECApp ((L.EFfi ("Basis", "linkable_to_nullable"), loc), _) => + ((L'.ERecord [], loc), fm) + | L.EFfi ("Basis", "mat_nil") => let val string = (L'.TFfi ("Basis", "string"), loc) @@ -1239,7 +1248,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "mat_cons"), _), + (L.ECApp ( + (L.EFfi ("Basis", "mat_cons"), _), + _), _), _), _), _), _), _), _), @@ -1249,21 +1260,27 @@ fun monoExp (env, st, fm) (all as (e, loc)) = val string = (L'.TFfi ("Basis", "string"), loc) val mat = (L'.TRecord [("1", string), ("2", string)], loc) in - ((L'.EAbs ("m", mat, mat, - (L'.ECase ((L'.EField ((L'.ERel 0, loc), "1"), loc), - [((L'.PPrim (Prim.String ""), loc), - (L'.ERecord [("1", (L'.EPrim (Prim.String ("uw_" ^ nm1)), loc), string), - ("2", (L'.EPrim (Prim.String ("uw_" ^ nm2)), loc), string)], loc)), - ((L'.PWild, loc), - (L'.ERecord [("1", (L'.EStrcat ( - (L'.EPrim (Prim.String ("uw_" ^ nm1 ^ ", ")), loc), - (L'.EField ((L'.ERel 0, loc), "1"), loc)), loc), string), - ("2", (L'.EStrcat ( - (L'.EPrim (Prim.String ("uw_" ^ nm2 ^ ", ")), loc), - (L'.EField ((L'.ERel 0, loc), "2"), loc)), loc), string)], - loc))], - {disc = string, - result = mat}), loc)), loc), + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (mat, mat), loc), + (L'.EAbs ("m", mat, mat, + (L'.ECase ((L'.EField ((L'.ERel 0, loc), "1"), loc), + [((L'.PPrim (Prim.String ""), loc), + (L'.ERecord [("1", (L'.EPrim (Prim.String ("uw_" ^ nm1)), + loc), string), + ("2", (L'.EPrim (Prim.String ("uw_" ^ nm2)), + loc), string)], loc)), + ((L'.PWild, loc), + (L'.ERecord [("1", (L'.EStrcat ( + (L'.EPrim (Prim.String ("uw_" ^ nm1 ^ ", ")), + loc), + (L'.EField ((L'.ERel 0, loc), "1"), loc)), + loc), string), + ("2", (L'.EStrcat ( + (L'.EPrim (Prim.String ("uw_" ^ nm2 ^ ", ")), loc), + (L'.EField ((L'.ERel 0, loc), "2"), loc)), + loc), string)], + loc))], + {disc = string, + result = mat}), loc)), loc)), loc), fm) end diff --git a/src/urweb.grm b/src/urweb.grm index 16a77150..50fb6cb3 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -523,6 +523,7 @@ cst : UNIQUE tnames (let val e = (ECApp (e, nm2), loc) val e = (EDisjointApp e, loc) val e = (EDisjointApp e, loc) + val e = (EApp (e, (EWild, loc)), loc) in (EApp (e, mat), loc) end) diff --git a/tests/cst.ur b/tests/cst.ur index 548862be..cbaa36ed 100644 --- a/tests/cst.ur +++ b/tests/cst.ur @@ -1,8 +1,9 @@ -table u : {C : int, D : int, E : int} +table u : {C : int, D : int, E : option int} PRIMARY KEY C, - CONSTRAINT U UNIQUE (C, D) + CONSTRAINT U UNIQUE (C, D), + CONSTRAINT U2 UNIQUE E -table t : {A : int, B : int} +table t : {A : int, B : int, C : option int} PRIMARY KEY B, CONSTRAINT UniA UNIQUE A, @@ -20,8 +21,10 @@ table t : {A : int, B : int} CONSTRAINT ForA FOREIGN KEY A REFERENCES u (C), CONSTRAINT ForAB FOREIGN KEY (A, B) REFERENCES u (D, C) ON DELETE CASCADE ON UPDATE RESTRICT, CONSTRAINT ForBA FOREIGN KEY (A, B) REFERENCES u (C, D) ON UPDATE NO ACTION, + CONSTRAINT ForB FOREIGN KEY B REFERENCES u (E), + CONSTRAINT ForC FOREIGN KEY C REFERENCES u (C) - CONSTRAINT Self FOREIGN KEY B REFERENCES t (B) + (*CONSTRAINT Self FOREIGN KEY B REFERENCES t (B)*) table s : {B : option int} CONSTRAINT UniB UNIQUE B -- cgit v1.2.3