Mercurial > urweb

comparison lib/ur/basis.urs @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children 7292bcb7c02d
comparison
equal deleted inserted replaced
708:1a317a707d71 709:0406e9cccb72
159 val join_constraints : fs ::: {Type} 159 val join_constraints : fs ::: {Type}
160 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2] 160 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
161 => sql_constraints fs uniques1 -> sql_constraints fs uniques2 161 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
162 -> sql_constraints fs (uniques1 ++ uniques2) 162 -> sql_constraints fs (uniques1 ++ uniques2)
163 163
164
164 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type} 165 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
165 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest] 166 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
166 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique) 167 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
168
169 con matching :: {Type} -> {Type} -> Type
170 val mat_nil : matching [] []
171 val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type}
172 -> nm1 :: Name -> nm2 :: Name
173 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
174 => matching rest1 rest2
175 -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2)
176
177 con propagation_mode :: {Type} -> Type
178 val restrict : fs ::: {Type} -> propagation_mode fs
179 val cascade : fs ::: {Type} -> propagation_mode fs
180 val no_action : fs ::: {Type} -> propagation_mode fs
181 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
182
183
184 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
185 -> foreign ::: {Type} -> funused ::: {Type}
186 -> nm ::: Name -> uniques ::: {{Unit}}
187 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
188 => [foreign ~ funused] => [[nm] ~ uniques]
189 => matching ([mine1 = t] ++ mine) foreign
190 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
191 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
192 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
193 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
167 194
168 195
169 (*** Queries *) 196 (*** Queries *)
170 197
171 con sql_query :: {{Type}} -> {Type} -> Type 198 con sql_query :: {{Type}} -> {Type} -> Type