diff lib/ur/basis.urs @ 707:d8217b4cb617

PRIMARY KEY
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 16:14:31 -0400
parents e6706a1df013
children 0406e9cccb72
line wrap: on
line diff
--- a/lib/ur/basis.urs	Tue Apr 07 15:04:07 2009 -0400
+++ b/lib/ur/basis.urs	Tue Apr 07 16:14:31 2009 -0400
@@ -126,6 +126,27 @@
 
 (*** 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 @@
               -> 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)