Mercurial > urweb
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)