summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 16:14:31 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 16:14:31 -0400
commit26ad31287745567b98b357de9793a0e795c63334 (patch)
tree6fa2aa05d829b2b71c6e2d778b4898999992a00f /lib
parent98370da7e9f70e3d83f666019b765e15f617b846 (diff)
PRIMARY KEY
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/basis.urs30
1 files changed, 21 insertions, 9 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 4e926f87..997495b1 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -126,6 +126,27 @@ con sql_table :: {Type} -> {{Unit}} -> Type
(*** Constraints *)
+(**** Primary keys *)
+
+class sql_injectable_prim
+val sql_bool : sql_injectable_prim bool
+val sql_int : sql_injectable_prim int
+val sql_float : sql_injectable_prim float
+val sql_string : sql_injectable_prim string
+val sql_time : sql_injectable_prim time
+val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
+val sql_client : sql_injectable_prim client
+
+con primary_key :: {Type} -> {{Unit}} -> Type
+val no_primary_key : fs ::: {Type} -> primary_key fs []
+val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
+ -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
+ => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
+ -> primary_key ([key1 = t] ++ keys ++ rest)
+ [Pkey = [key1] ++ map (fn _ => ()) keys]
+
+(**** Other constraints *)
+
con sql_constraints :: {Type} -> {{Unit}} -> Type
(* Arguments: column types, uniqueness implications of constraints *)
@@ -224,15 +245,6 @@ val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {T
-> nm :: Name
-> sql_exp tabs agg ([nm = t] ++ rest) t
-class sql_injectable_prim
-val sql_bool : sql_injectable_prim bool
-val sql_int : sql_injectable_prim int
-val sql_float : sql_injectable_prim float
-val sql_string : sql_injectable_prim string
-val sql_time : sql_injectable_prim time
-val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
-val sql_client : sql_injectable_prim client
-
class sql_injectable
val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)