Mercurial > urweb

comparison src/expl_env.sml @ 806:0e554bfd6d6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:22:05 -0400
parents 8688e01ae469
children b2311dfb3158
comparison
equal deleted inserted replaced
805:e2780d2f4afc 806:0e554bfd6d6a
253 | SOME x => x 253 | SOME x => x
254 254
255 fun declBinds env (d, loc) = 255 fun declBinds env (d, loc) =
256 case d of 256 case d of
257 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) 257 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
258 | DDatatype (x, n, xs, xncs) => 258 | DDatatype dts =>
259 let 259 let
260 val env = pushCNamed env x n (KType, loc) NONE 260 fun doOne ((x, n, xs, xncs), env) =
261 let
262 val k = (KType, loc)
263 val nxs = length xs
264 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
265 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
266 (KArrow (k, kb), loc)))
267 ((CNamed n, loc), k) xs
268
269 val env = pushCNamed env x n kb NONE
270 in
271 foldl (fn ((x', n', to), env) =>
272 let
273 val t =
274 case to of
275 NONE => tb
276 | SOME t => (TFun (t, tb), loc)
277 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
278 in
279 pushENamed env x' n' t
280 end)
281 env xncs
282 end
283 in
284 foldl doOne env dts
285 end
286 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
287 let
288 val t = (CModProj (m, ms, x'), loc)
289 val env = pushCNamed env x n (KType, loc) (SOME t)
290
291 val t = (CNamed n, loc)
261 in 292 in
262 foldl (fn ((x', n', to), env) => 293 foldl (fn ((x', n', to), env) =>
263 let 294 let
264 val t = 295 val t =
265 case to of 296 case to of
270 in 301 in
271 pushENamed env x' n' t 302 pushENamed env x' n' t
272 end) 303 end)
273 env xncs 304 env xncs
274 end 305 end
275 | DDatatypeImp (x, n, m, ms, x', xs, xncs) => 306 | DVal (x, n, t, _) => pushENamed env x n t
276 let 307 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
277 val t = (CModProj (m, ms, x'), loc) 308 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
309 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
310 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
311 | DExport _ => env
312 | DTable (tn, x, n, c, _, pc, _, cc) =>
313 let
314 val ct = (CModProj (tn, [], "sql_table"), loc)
315 val ct = (CApp (ct, c), loc)
316 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
317 in
318 pushENamed env x n ct
319 end
320 | DSequence (tn, x, n) =>
321 let
322 val t = (CModProj (tn, [], "sql_sequence"), loc)
323 in
324 pushENamed env x n t
325 end
326 | DView (tn, x, n, _, c) =>
327 let
328 val ct = (CModProj (tn, [], "sql_view"), loc)
329 val ct = (CApp (ct, c), loc)
330 in
331 pushENamed env x n ct
332 end
333 | DDatabase _ => env
334 | DCookie (tn, x, n, c) =>
335 let
336 val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
337 in
338 pushENamed env x n t
339 end
340 | DStyle (tn, x, n) =>
341 let
342 val t = (CModProj (tn, [], "css_class"), loc)
343 in
344 pushENamed env x n t
345 end
346
347 fun sgiBinds env (sgi, loc) =
348 case sgi of
349 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
350 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
351 | SgiDatatype dts =>
352 let
353 fun doOne ((x, n, xs, xncs), env) =
354 let
355 val k = (KType, loc)
356 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
357
358 val env = pushCNamed env x n k' NONE
359 in
360 foldl (fn ((x', n', to), env) =>
361 let
362 val t =
363 case to of
364 NONE => (CNamed n, loc)
365 | SOME t => (TFun (t, (CNamed n, loc)), loc)
366
367 val k = (KType, loc)
368 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
369 in
370 pushENamed env x' n' t
371 end)
372 env xncs
373 end
374 in
375 foldl doOne env dts
376 end
377 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
378 let
379 val t = (CModProj (m1, ms, x'), loc)
278 val env = pushCNamed env x n (KType, loc) (SOME t) 380 val env = pushCNamed env x n (KType, loc) (SOME t)
279 381
280 val t = (CNamed n, loc) 382 val t = (CNamed n, loc)
281 in 383 in
282 foldl (fn ((x', n', to), env) => 384 foldl (fn ((x', n', to), env) =>
290 in 392 in
291 pushENamed env x' n' t 393 pushENamed env x' n' t
292 end) 394 end)
293 env xncs 395 env xncs
294 end 396 end
295 | DVal (x, n, t, _) => pushENamed env x n t
296 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
297 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
298 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
299 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
300 | DExport _ => env
301 | DTable (tn, x, n, c, _, pc, _, cc) =>
302 let
303 val ct = (CModProj (tn, [], "sql_table"), loc)
304 val ct = (CApp (ct, c), loc)
305 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
306 in
307 pushENamed env x n ct
308 end
309 | DSequence (tn, x, n) =>
310 let
311 val t = (CModProj (tn, [], "sql_sequence"), loc)
312 in
313 pushENamed env x n t
314 end
315 | DView (tn, x, n, _, c) =>
316 let
317 val ct = (CModProj (tn, [], "sql_view"), loc)
318 val ct = (CApp (ct, c), loc)
319 in
320 pushENamed env x n ct
321 end
322 | DDatabase _ => env
323 | DCookie (tn, x, n, c) =>
324 let
325 val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
326 in
327 pushENamed env x n t
328 end
329 | DStyle (tn, x, n) =>
330 let
331 val t = (CModProj (tn, [], "css_class"), loc)
332 in
333 pushENamed env x n t
334 end
335
336 fun sgiBinds env (sgi, loc) =
337 case sgi of
338 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
339 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
340 | SgiDatatype (x, n, xs, xncs) =>
341 let
342 val env = pushCNamed env x n (KType, loc) NONE
343 in
344 foldl (fn ((x', n', to), env) =>
345 let
346 val t =
347 case to of
348 NONE => (CNamed n, loc)
349 | SOME t => (TFun (t, (CNamed n, loc)), loc)
350 val k = (KType, loc)
351 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
352 in
353 pushENamed env x' n' t
354 end)
355 env xncs
356 end
357 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
358 let
359 val t = (CModProj (m1, ms, x'), loc)
360 val env = pushCNamed env x n (KType, loc) (SOME t)
361
362 val t = (CNamed n, loc)
363 in
364 foldl (fn ((x', n', to), env) =>
365 let
366 val t =
367 case to of
368 NONE => (CNamed n, loc)
369 | SOME t => (TFun (t, (CNamed n, loc)), loc)
370 val k = (KType, loc)
371 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
372 in
373 pushENamed env x' n' t
374 end)
375 env xncs
376 end
377 | SgiVal (x, n, t) => pushENamed env x n t 397 | SgiVal (x, n, t) => pushENamed env x n t
378 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn 398 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
379 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn 399 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
380 400
381 end 401 end