Mercurial > urweb

comparison lib/ur/basis.urs @ 705:e6706a1df013

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track uniqueness sets in table types
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 14:11:32 -0400
parents 70cbdcf5989b
children d8217b4cb617
comparison
equal deleted inserted replaced
704:70cbdcf5989b 705:e6706a1df013
120 val self : transaction client 120 val self : transaction client
121 121
122 122
123 (** SQL *) 123 (** SQL *)
124 124
125 con sql_table :: {Type} -> Type 125 con sql_table :: {Type} -> {{Unit}} -> Type
126 126
127 (*** Constraints *) 127 (*** Constraints *)
128 128
129 con sql_constraints :: {Unit} -> {Type} -> Type 129 con sql_constraints :: {Type} -> {{Unit}} -> Type
130 con sql_constraint :: {Type} -> Type 130 (* Arguments: column types, uniqueness implications of constraints *)
131 131
132 val no_constraint : fs ::: {Type} -> sql_constraints [] fs 132 con sql_constraint :: {Type} -> {Unit} -> Type
133 val one_constraint : fs ::: {Type} -> name :: Name -> sql_constraint fs -> sql_constraints [name] fs 133
134 val join_constraints : names1 ::: {Unit} -> names2 ::: {Unit} -> fs ::: {Type} -> [names1 ~ names2] 134 val no_constraint : fs ::: {Type} -> sql_constraints fs []
135 => sql_constraints names1 fs -> sql_constraints names2 fs 135 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
136 -> sql_constraints (names1 ++ names2) fs 136 -> sql_constraint fs unique
137 137 -> sql_constraints fs [name = unique]
138 val unique : rest ::: {Type} -> unique :: {Type} -> [unique ~ rest] => sql_constraint (unique ++ rest) 138 val join_constraints : fs ::: {Type}
139 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
140 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
141 -> sql_constraints fs (uniques1 ++ uniques2)
142
143 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
144 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
145 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
139 146
140 147
141 (*** Queries *) 148 (*** Queries *)
142 149
143 con sql_query :: {{Type}} -> {Type} -> Type 150 con sql_query :: {{Type}} -> {Type} -> Type
149 -> sql_subset 156 -> sql_subset
150 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) 157 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
151 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop) 158 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
152 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables 159 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
153 160
154 val sql_query1 : tables ::: {{Type}} 161 val sql_query1 : tables ::: {({Type} * {{Unit}})}
155 -> grouped ::: {{Type}} 162 -> grouped ::: {{Type}}
156 -> selectedFields ::: {{Type}} 163 -> selectedFields ::: {{Type}}
157 -> selectedExps ::: {Type} 164 -> selectedExps ::: {Type}
158 -> {From : $(map sql_table tables), 165 -> {From : $(map (fn p :: ({Type} * {{Unit}}) => sql_table p.1 p.2) tables),
159 Where : sql_exp tables [] [] bool, 166 Where : sql_exp (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] [] bool,
160 GroupBy : sql_subset tables grouped, 167 GroupBy : sql_subset (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) grouped,
161 Having : sql_exp grouped tables [] bool, 168 Having : sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] bool,
162 SelectFields : sql_subset grouped selectedFields, 169 SelectFields : sql_subset grouped selectedFields,
163 SelectExps : $(map (sql_exp grouped tables []) selectedExps) } 170 SelectExps : $(map (sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [])
164 -> sql_query1 tables selectedFields selectedExps 171 selectedExps) }
172 -> sql_query1 (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) selectedFields selectedExps
165 173
166 type sql_relop 174 type sql_relop
167 val sql_union : sql_relop 175 val sql_union : sql_relop
168 val sql_intersect : sql_relop 176 val sql_intersect : sql_relop
169 val sql_except : sql_relop 177 val sql_except : sql_relop
319 (*** Database mutators *) 327 (*** Database mutators *)
320 328
321 type dml 329 type dml
322 val dml : dml -> transaction unit 330 val dml : dml -> transaction unit
323 331
324 val insert : fields ::: {Type} 332 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
325 -> sql_table fields 333 -> sql_table fields uniques
326 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) 334 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
327 -> dml 335 -> dml
328 336
329 val update : unchanged ::: {Type} -> changed :: {Type} -> 337 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
330 [changed ~ unchanged] => 338 [changed ~ unchanged] =>
331 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) 339 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
332 -> sql_table (changed ++ unchanged) 340 -> sql_table (changed ++ unchanged) uniques
333 -> sql_exp [T = changed ++ unchanged] [] [] bool 341 -> sql_exp [T = changed ++ unchanged] [] [] bool
334 -> dml 342 -> dml
335 343
336 val delete : fields ::: {Type} 344 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
337 -> sql_table fields 345 -> sql_table fields uniques
338 -> sql_exp [T = fields] [] [] bool 346 -> sql_exp [T = fields] [] [] bool
339 -> dml 347 -> dml
340 348
341 (*** Sequences *) 349 (*** Sequences *)
342 350