comparison lib/ur/basis.urs @ 621:8998114760c1

"Hello world" compiles, after replacing type-level fold with map
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 15:33:20 -0500
parents 1d34d916c206
children e68de2a5506b
comparison
equal deleted inserted replaced
620:d828b143e147 621:8998114760c1
118 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type 118 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
119 119
120 con sql_subset :: {{Type}} -> {{Type}} -> Type 120 con sql_subset :: {{Type}} -> {{Type}} -> Type
121 val sql_subset : keep_drop :: {({Type} * {Type})} 121 val sql_subset : keep_drop :: {({Type} * {Type})}
122 -> sql_subset 122 -> sql_subset
123 (fold (fn nm (fields :: ({Type} * {Type})) 123 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
124 acc [[nm] ~ acc] 124 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
125 [fields.1 ~ fields.2] =>
126 [nm = fields.1 ++ fields.2]
127 ++ acc) [] keep_drop)
128 (fold (fn nm (fields :: ({Type} * {Type}))
129 acc [[nm] ~ acc] =>
130 [nm = fields.1] ++ acc)
131 [] keep_drop)
132 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables 125 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
133 126
134 val sql_query1 : tables ::: {{Type}} 127 val sql_query1 : tables ::: {{Type}}
135 -> grouped ::: {{Type}} 128 -> grouped ::: {{Type}}
136 -> selectedFields ::: {{Type}} 129 -> selectedFields ::: {{Type}}
137 -> selectedExps ::: {Type} 130 -> selectedExps ::: {Type}
138 -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 131 -> {From : $(map (fn fields :: {Type} => sql_table fields) tables),
139 [nm = sql_table fields] ++ acc)
140 [] tables),
141 Where : sql_exp tables [] [] bool, 132 Where : sql_exp tables [] [] bool,
142 GroupBy : sql_subset tables grouped, 133 GroupBy : sql_subset tables grouped,
143 Having : sql_exp grouped tables [] bool, 134 Having : sql_exp grouped tables [] bool,
144 SelectFields : sql_subset grouped selectedFields, 135 SelectFields : sql_subset grouped selectedFields,
145 SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => 136 SelectExps : $(map (fn (t :: Type) => sql_exp grouped tables [] t) selectedExps) }
146 [nm = sql_exp grouped tables [] t]
147 ++ acc) [] selectedExps) }
148 -> sql_query1 tables selectedFields selectedExps 137 -> sql_query1 tables selectedFields selectedExps
149 138
150 type sql_relop 139 type sql_relop
151 val sql_union : sql_relop 140 val sql_union : sql_relop
152 val sql_intersect : sql_relop 141 val sql_intersect : sql_relop
289 278
290 val query : tables ::: {{Type}} -> exps ::: {Type} 279 val query : tables ::: {{Type}} -> exps ::: {Type}
291 -> fn [tables ~ exps] => 280 -> fn [tables ~ exps] =>
292 state ::: Type 281 state ::: Type
293 -> sql_query tables exps 282 -> sql_query tables exps
294 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 283 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
295 [nm = $fields] ++ acc) [] tables)
296 -> state 284 -> state
297 -> transaction state) 285 -> transaction state)
298 -> state 286 -> state
299 -> transaction state 287 -> transaction state
300 288
304 type dml 292 type dml
305 val dml : dml -> transaction unit 293 val dml : dml -> transaction unit
306 294
307 val insert : fields ::: {Type} 295 val insert : fields ::: {Type}
308 -> sql_table fields 296 -> sql_table fields
309 -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => 297 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
310 [nm = sql_exp [] [] [] t] ++ acc)
311 [] fields)
312 -> dml 298 -> dml
313 299
314 val update : unchanged ::: {Type} -> changed :: {Type} -> 300 val update : unchanged ::: {Type} -> changed :: {Type} ->
315 fn [changed ~ unchanged] => 301 fn [changed ~ unchanged] =>
316 $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => 302 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
317 [nm = sql_exp [T = changed ++ unchanged] [] [] t]
318 ++ acc)
319 [] changed)
320 -> sql_table (changed ++ unchanged) 303 -> sql_table (changed ++ unchanged)
321 -> sql_exp [T = changed ++ unchanged] [] [] bool 304 -> sql_exp [T = changed ++ unchanged] [] [] bool
322 -> dml 305 -> dml
323 306
324 val delete : fields ::: {Type} 307 val delete : fields ::: {Type}