Mercurial > urweb

comparison lib/ur/basis.urs @ 712:915ec60592d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More flexible foreign keying
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 13:59:34 -0400
parents 7292bcb7c02d
children 0f42461273cf
comparison
equal deleted inserted replaced
711:7292bcb7c02d 712:915ec60592d4
164 164
165 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type} 165 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
166 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest] 166 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
167 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique) 167 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
168 168
169 class linkable :: Type -> Type -> Type
170 val linkable_same : t ::: Type -> linkable t t
171 val linkable_from_nullable : t ::: Type -> linkable (option t) t
172 val linkable_to_nullable : t ::: Type -> linkable t (option t)
173
169 con matching :: {Type} -> {Type} -> Type 174 con matching :: {Type} -> {Type} -> Type
170 val mat_nil : matching [] [] 175 val mat_nil : matching [] []
171 val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type} 176 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
172 -> nm1 :: Name -> nm2 :: Name 177 -> nm1 :: Name -> nm2 :: Name
173 -> [[nm1] ~ rest1] => [[nm2] ~ rest2] 178 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
174 => matching rest1 rest2 179 => linkable t1 t2
175 -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2) 180 -> matching rest1 rest2
181 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
176 182
177 con propagation_mode :: {Type} -> Type 183 con propagation_mode :: {Type} -> Type
178 val restrict : fs ::: {Type} -> propagation_mode fs 184 val restrict : fs ::: {Type} -> propagation_mode fs
179 val cascade : fs ::: {Type} -> propagation_mode fs 185 val cascade : fs ::: {Type} -> propagation_mode fs
180 val no_action : fs ::: {Type} -> propagation_mode fs 186 val no_action : fs ::: {Type} -> propagation_mode fs