comparison lib/ur/basis.urs @ 714:0f42461273cf

CHECK constraints
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 15:30:15 -0400
parents 915ec60592d4
children e28637743279
comparison
equal deleted inserted replaced
713:baaae037e7f6 714:0f42461273cf
196 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques) 196 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
197 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine), 197 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
198 OnUpdate : propagation_mode ([mine1 = t] ++ mine)} 198 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
199 -> sql_constraint ([mine1 = t] ++ mine ++ munused) [] 199 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
200 200
201 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
202
203 val check : fs ::: {Type}
204 -> sql_exp [] [] fs bool
205 -> sql_constraint fs []
206
207
201 208
202 (*** Queries *) 209 (*** Queries *)
203 210
204 con sql_query :: {{Type}} -> {Type} -> Type 211 con sql_query :: {{Type}} -> {Type} -> Type
205 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type 212 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
206 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
207 213
208 con sql_subset :: {{Type}} -> {{Type}} -> Type 214 con sql_subset :: {{Type}} -> {{Type}} -> Type
209 val sql_subset : keep_drop :: {({Type} * {Type})} 215 val sql_subset : keep_drop :: {({Type} * {Type})}
210 -> sql_subset 216 -> sql_subset
211 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) 217 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)