Mercurial > urweb

comparison src/elab_util.sml @ 156:34ccd7d2bea8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of datatype support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:02:03 -0400
parents 7420fa18d657
children 06a98129b23f
comparison
equal deleted inserted replaced
155:4334bb734187 156:34ccd7d2bea8
363 val kind = Kind.mapfold kind 363 val kind = Kind.mapfold kind
364 364
365 fun sgi ctx si acc = 365 fun sgi ctx si acc =
366 S.bindP (sgi' ctx si acc, sgn_item ctx) 366 S.bindP (sgi' ctx si acc, sgn_item ctx)
367 367
368 and sgi' ctx (si, loc) = 368 and sgi' ctx (siAll as (si, loc)) =
369 case si of 369 case si of
370 SgiConAbs (x, n, k) => 370 SgiConAbs (x, n, k) =>
371 S.map2 (kind k, 371 S.map2 (kind k,
372 fn k' => 372 fn k' =>
373 (SgiConAbs (x, n, k'), loc)) 373 (SgiConAbs (x, n, k'), loc))
375 S.bind2 (kind k, 375 S.bind2 (kind k,
376 fn k' => 376 fn k' =>
377 S.map2 (con ctx c, 377 S.map2 (con ctx c,
378 fn c' => 378 fn c' =>
379 (SgiCon (x, n, k', c'), loc))) 379 (SgiCon (x, n, k', c'), loc)))
380 | SgiDatatype (x, n, xncs) =>
381 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
382 case c of
383 NONE => S.return2 (x, n, c)
384 | SOME c =>
385 S.map2 (con ctx c,
386 fn c' => (x, n, SOME c'))) xncs,
387 fn xncs' =>
388 (SgiDatatype (x, n, xncs'), loc))
389 | SgiDatatypeImp _ => S.return2 siAll
380 | SgiVal (x, n, c) => 390 | SgiVal (x, n, c) =>
381 S.map2 (con ctx c, 391 S.map2 (con ctx c,
382 fn c' => 392 fn c' =>
383 (SgiVal (x, n, c'), loc)) 393 (SgiVal (x, n, c'), loc))
384 | SgiStr (x, n, s) => 394 | SgiStr (x, n, s) =>
406 (case #1 si of 416 (case #1 si of
407 SgiConAbs (x, _, k) => 417 SgiConAbs (x, _, k) =>
408 bind (ctx, NamedC (x, k)) 418 bind (ctx, NamedC (x, k))
409 | SgiCon (x, _, k, _) => 419 | SgiCon (x, _, k, _) =>
410 bind (ctx, NamedC (x, k)) 420 bind (ctx, NamedC (x, k))
421 | SgiDatatype (x, n, xncs) =>
422 bind (ctx, NamedC (x, (KType, loc)))
423 | SgiDatatypeImp (x, _, _, _, _) =>
424 bind (ctx, NamedC (x, (KType, loc)))
411 | SgiVal _ => ctx 425 | SgiVal _ => ctx
412 | SgiStr (x, _, sgn) => 426 | SgiStr (x, _, sgn) =>
413 bind (ctx, Str (x, sgn)) 427 bind (ctx, Str (x, sgn))
414 | SgiSgn (x, _, sgn) => 428 | SgiSgn (x, _, sgn) =>
415 bind (ctx, Sgn (x, sgn)) 429 bind (ctx, Sgn (x, sgn))
510 StrConst ds => 524 StrConst ds =>
511 S.map2 (ListUtil.mapfoldB (fn (ctx, d) => 525 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
512 (case #1 d of 526 (case #1 d of
513 DCon (x, _, k, _) => 527 DCon (x, _, k, _) =>
514 bind (ctx, NamedC (x, k)) 528 bind (ctx, NamedC (x, k))
529 | DDatatype (x, n, xncs) =>
530 let
531 val ctx = bind (ctx, NamedC (x, (KType, loc)))
532 in
533 foldl (fn ((x, _, co), ctx) =>
534 let
535 val t =
536 case co of
537 NONE => CNamed n
538 | SOME t => TFun (t, (CNamed n, loc))
539 in
540 bind (ctx, NamedE (x, (t, loc)))
541 end)
542 ctx xncs
543 end
544 | DDatatypeImp (x, n, m, ms, x') =>
545 bind (ctx, NamedC (x, (KType, loc)))
515 | DVal (x, _, c, _) => 546 | DVal (x, _, c, _) =>
516 bind (ctx, NamedE (x, c)) 547 bind (ctx, NamedE (x, c))
517 | DValRec vis => 548 | DValRec vis =>
518 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis 549 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
519 | DSgn (x, _, sgn) => 550 | DSgn (x, _, sgn) =>
556 S.bind2 (mfk k, 587 S.bind2 (mfk k,
557 fn k' => 588 fn k' =>
558 S.map2 (mfc ctx c, 589 S.map2 (mfc ctx c,
559 fn c' => 590 fn c' =>
560 (DCon (x, n, k', c'), loc))) 591 (DCon (x, n, k', c'), loc)))
592 | DDatatype (x, n, xncs) =>
593 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
594 case c of
595 NONE => S.return2 (x, n, c)
596 | SOME c =>
597 S.map2 (mfc ctx c,
598 fn c' => (x, n, SOME c'))) xncs,
599 fn xncs' =>
600 (DDatatype (x, n, xncs'), loc))
601 | DDatatypeImp _ => S.return2 dAll
561 | DVal vi => 602 | DVal vi =>
562 S.map2 (mfvi ctx vi, 603 S.map2 (mfvi ctx vi,
563 fn vi' => 604 fn vi' =>
564 (DVal vi', loc)) 605 (DVal vi', loc))
565 | DValRec vis => 606 | DValRec vis =>