Mercurial > urweb

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PRIMARY KEY
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 16:14:31 -0400
parents e6706a1df013
children 0406e9cccb72
comparison
equal deleted inserted replaced
706:1fb318c17546 707:d8217b4cb617
123 (** SQL *) 123 (** SQL *)
124 124
125 con sql_table :: {Type} -> {{Unit}} -> Type 125 con sql_table :: {Type} -> {{Unit}} -> Type
126 126
127 (*** Constraints *) 127 (*** Constraints *)
128
129 (**** Primary keys *)
130
131 class sql_injectable_prim
132 val sql_bool : sql_injectable_prim bool
133 val sql_int : sql_injectable_prim int
134 val sql_float : sql_injectable_prim float
135 val sql_string : sql_injectable_prim string
136 val sql_time : sql_injectable_prim time
137 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
138 val sql_client : sql_injectable_prim client
139
140 con primary_key :: {Type} -> {{Unit}} -> Type
141 val no_primary_key : fs ::: {Type} -> primary_key fs []
142 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
143 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
144 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
145 -> primary_key ([key1 = t] ++ keys ++ rest)
146 [Pkey = [key1] ++ map (fn _ => ()) keys]
147
148 (**** Other constraints *)
128 149
129 con sql_constraints :: {Type} -> {{Unit}} -> Type 150 con sql_constraints :: {Type} -> {{Unit}} -> Type
130 (* Arguments: column types, uniqueness implications of constraints *) 151 (* Arguments: column types, uniqueness implications of constraints *)
131 152
132 con sql_constraint :: {Type} -> {Unit} -> Type 153 con sql_constraint :: {Type} -> {Unit} -> Type
221 agg exps fieldType 242 agg exps fieldType
222 243
223 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} 244 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
224 -> nm :: Name 245 -> nm :: Name
225 -> sql_exp tabs agg ([nm = t] ++ rest) t 246 -> sql_exp tabs agg ([nm = t] ++ rest) t
226
227 class sql_injectable_prim
228 val sql_bool : sql_injectable_prim bool
229 val sql_int : sql_injectable_prim int
230 val sql_float : sql_injectable_prim float
231 val sql_string : sql_injectable_prim string
232 val sql_time : sql_injectable_prim time
233 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
234 val sql_client : sql_injectable_prim client
235 247
236 class sql_injectable 248 class sql_injectable
237 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t 249 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
238 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) 250 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
239 251