comparison src/elab_util.sml @ 203:dd82457fda82

Parsing and elaborating 'table'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 13:20:29 -0400
parents ab86aa858e6c
children cb8f69556975
comparison
equal deleted inserted replaced
202:af5bd54cbbd7 203:dd82457fda82
434 S.bind2 (con ctx c1, 434 S.bind2 (con ctx c1,
435 fn c1' => 435 fn c1' =>
436 S.map2 (con ctx c2, 436 S.map2 (con ctx c2,
437 fn c2' => 437 fn c2' =>
438 (SgiConstraint (c1', c2'), loc))) 438 (SgiConstraint (c1', c2'), loc)))
439 | SgiTable (x, n, c) =>
440 S.map2 (con ctx c,
441 fn c' =>
442 (SgiTable (x, n, c'), loc))
439 443
440 and sg ctx s acc = 444 and sg ctx s acc =
441 S.bindP (sg' ctx s acc, sgn ctx) 445 S.bindP (sg' ctx s acc, sgn ctx)
442 446
443 and sg' ctx (sAll as (s, loc)) = 447 and sg' ctx (sAll as (s, loc)) =
456 | SgiVal _ => ctx 460 | SgiVal _ => ctx
457 | SgiStr (x, _, sgn) => 461 | SgiStr (x, _, sgn) =>
458 bind (ctx, Str (x, sgn)) 462 bind (ctx, Str (x, sgn))
459 | SgiSgn (x, _, sgn) => 463 | SgiSgn (x, _, sgn) =>
460 bind (ctx, Sgn (x, sgn)) 464 bind (ctx, Sgn (x, sgn))
461 | SgiConstraint _ => ctx, 465 | SgiConstraint _ => ctx
466 | SgiTable _ => ctx,
462 sgi ctx si)) ctx sgis, 467 sgi ctx si)) ctx sgis,
463 fn sgis' => 468 fn sgis' =>
464 (SgnConst sgis', loc)) 469 (SgnConst sgis', loc))
465 470
466 | SgnVar _ => S.return2 sAll 471 | SgnVar _ => S.return2 sAll
592 | DStr (x, _, sgn, _) => 597 | DStr (x, _, sgn, _) =>
593 bind (ctx, Str (x, sgn)) 598 bind (ctx, Str (x, sgn))
594 | DFfiStr (x, _, sgn) => 599 | DFfiStr (x, _, sgn) =>
595 bind (ctx, Str (x, sgn)) 600 bind (ctx, Str (x, sgn))
596 | DConstraint _ => ctx 601 | DConstraint _ => ctx
597 | DExport _ => ctx, 602 | DExport _ => ctx
603 | DTable _ => ctx,
598 mfd ctx d)) ctx ds, 604 mfd ctx d)) ctx ds,
599 fn ds' => (StrConst ds', loc)) 605 fn ds' => (StrConst ds', loc))
600 | StrVar _ => S.return2 strAll 606 | StrVar _ => S.return2 strAll
601 | StrProj (str, x) => 607 | StrProj (str, x) =>
602 S.map2 (mfst ctx str, 608 S.map2 (mfst ctx str,
680 fn sgn' => 686 fn sgn' =>
681 S.map2 (mfst ctx str, 687 S.map2 (mfst ctx str,
682 fn str' => 688 fn str' =>
683 (DExport (en, sgn', str'), loc))) 689 (DExport (en, sgn', str'), loc)))
684 690
691 | DTable (x, n, c) =>
692 S.map2 (mfc ctx c,
693 fn c' =>
694 (DTable (x, n, c'), loc))
695
685 and mfvi ctx (x, n, c, e) = 696 and mfvi ctx (x, n, c, e) =
686 S.bind2 (mfc ctx c, 697 S.bind2 (mfc ctx c,
687 fn c' => 698 fn c' =>
688 S.map2 (mfe ctx e, 699 S.map2 (mfe ctx e,
689 fn e' => 700 fn e' =>