summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-09 13:59:34 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-09 13:59:34 -0400
commitb167bec378ae4577ba2994e0621bf01a44832d34 (patch)
treeff692444e26cba80b8c5b19ad5be21a85cbf563c
parenta75aaa90b3b827f9ef002491bc081df36260f136 (diff)
More flexible foreign keying
-rw-r--r--lib/ur/basis.urs12
-rw-r--r--src/elab_err.sml4
-rw-r--r--src/elaborate.sml2
-rw-r--r--src/monoize.sml49
-rw-r--r--src/urweb.grm1
-rw-r--r--tests/cst.ur11
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