comparison src/core_util.sml @ 163:80192edca30d

Datatypes through corify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 13:16:21 -0400
parents 7420fa18d657
children 5d030ee143e2
comparison
equal deleted inserted replaced
162:06a98129b23f 163:80192edca30d
388 S.bind2 (mfk k, 388 S.bind2 (mfk k,
389 fn k' => 389 fn k' =>
390 S.map2 (mfc ctx c, 390 S.map2 (mfc ctx c,
391 fn c' => 391 fn c' =>
392 (DCon (x, n, k', c'), loc))) 392 (DCon (x, n, k', c'), loc)))
393 | DDatatype (x, n, xncs) =>
394 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
395 case c of
396 NONE => S.return2 (x, n, c)
397 | SOME c =>
398 S.map2 (mfc ctx c,
399 fn c' => (x, n, SOME c'))) xncs,
400 fn xncs' =>
401 (DDatatype (x, n, xncs'), loc))
393 | DVal vi => 402 | DVal vi =>
394 S.map2 (mfvi ctx vi, 403 S.map2 (mfvi ctx vi,
395 fn vi' => 404 fn vi' =>
396 (DVal vi', loc)) 405 (DVal vi', loc))
397 | DValRec vis => 406 | DValRec vis =>
456 fn d' => 465 fn d' =>
457 let 466 let
458 val ctx' = 467 val ctx' =
459 case #1 d' of 468 case #1 d' of
460 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c)) 469 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
470 | DDatatype (x, n, xncs) =>
471 let
472 val ctx = bind (ctx, NamedC (x, n, (KType, #2 d'), NONE))
473 val t = (CNamed n, #2 d')
474 in
475 foldl (fn ((x, n, to), ctx) =>
476 let
477 val t = case to of
478 NONE => t
479 | SOME t' => (TFun (t', t), #2 d')
480 in
481 bind (ctx, NamedE (x, n, t, NONE, ""))
482 end)
483 ctx xncs
484 end
461 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s)) 485 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
462 | DValRec vis => 486 | DValRec vis =>
463 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s))) 487 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
464 ctx vis 488 ctx vis
465 | DExport _ => ctx 489 | DExport _ => ctx