Mercurial > urweb
comparison src/mono_util.sml @ 808:d8f58d488cfb
Mutual datatypes through Pathcheck
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 15:55:15 -0400 |
parents | fa2019a63ea4 |
children | 493f44759879 |
comparison
equal
deleted
inserted
replaced
807:61a1f5c5ae2c | 808:d8f58d488cfb |
---|---|
464 fun mfd ctx d acc = | 464 fun mfd ctx d acc = |
465 S.bindP (mfd' ctx d acc, fd ctx) | 465 S.bindP (mfd' ctx d acc, fd ctx) |
466 | 466 |
467 and mfd' ctx (dAll as (d, loc)) = | 467 and mfd' ctx (dAll as (d, loc)) = |
468 case d of | 468 case d of |
469 DDatatype (x, n, xncs) => | 469 DDatatype dts => |
470 S.map2 (ListUtil.mapfold (fn (x, n, c) => | 470 S.map2 (ListUtil.mapfold (fn (x, n, xncs) => |
471 case c of | 471 S.map2 (ListUtil.mapfold (fn (x, n, c) => |
472 NONE => S.return2 (x, n, c) | 472 case c of |
473 | SOME c => | 473 NONE => S.return2 (x, n, c) |
474 S.map2 (mft c, | 474 | SOME c => |
475 fn c' => (x, n, SOME c'))) xncs, | 475 S.map2 (mft c, |
476 fn xncs' => | 476 fn c' => (x, n, SOME c'))) xncs, |
477 (DDatatype (x, n, xncs'), loc)) | 477 fn xncs' => (x, n, xncs'))) dts, |
478 fn dts' => | |
479 (DDatatype dts', loc)) | |
478 | DVal vi => | 480 | DVal vi => |
479 S.map2 (mfvi ctx vi, | 481 S.map2 (mfvi ctx vi, |
480 fn vi' => | 482 fn vi' => |
481 (DVal vi', loc)) | 483 (DVal vi', loc)) |
482 | DValRec vis => | 484 | DValRec vis => |
564 S.bind2 (mfd ctx d, | 566 S.bind2 (mfd ctx d, |
565 fn d' => | 567 fn d' => |
566 let | 568 let |
567 val ctx' = | 569 val ctx' = |
568 case #1 d' of | 570 case #1 d' of |
569 DDatatype (x, n, xncs) => | 571 DDatatype dts => |
570 let | 572 foldl (fn ((x, n, xncs), ctx) => |
571 val ctx = bind (ctx, Datatype (x, n, xncs)) | 573 let |
572 val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), #2 d') | 574 val ctx = bind (ctx, Datatype (x, n, xncs)) |
573 in | 575 val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), |
574 foldl (fn ((x, n, to), ctx) => | 576 #2 d') |
575 let | 577 in |
576 val t = case to of | 578 foldl (fn ((x, n, to), ctx) => |
577 NONE => t | 579 let |
578 | SOME t' => (TFun (t', t), #2 d') | 580 val t = case to of |
579 in | 581 NONE => t |
580 bind (ctx, NamedE (x, n, t, NONE, "")) | 582 | SOME t' => (TFun (t', t), #2 d') |
581 end) | 583 in |
582 ctx xncs | 584 bind (ctx, NamedE (x, n, t, NONE, "")) |
583 end | 585 end) |
586 ctx xncs | |
587 end) ctx dts | |
584 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s)) | 588 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s)) |
585 | DValRec vis => foldl (fn ((x, n, t, e, s), ctx) => | 589 | DValRec vis => foldl (fn ((x, n, t, e, s), ctx) => |
586 bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis | 590 bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis |
587 | DExport _ => ctx | 591 | DExport _ => ctx |
588 | DTable _ => ctx | 592 | DTable _ => ctx |
629 S.Continue (_, s) => s | 633 S.Continue (_, s) => s |
630 | S.Return _ => raise Fail "MonoUtil.File.fold: Impossible" | 634 | S.Return _ => raise Fail "MonoUtil.File.fold: Impossible" |
631 | 635 |
632 val maxName = foldl (fn ((d, _) : decl, count) => | 636 val maxName = foldl (fn ((d, _) : decl, count) => |
633 case d of | 637 case d of |
634 DDatatype (_, n, ns) => | 638 DDatatype dts => |
635 foldl (fn ((_, n', _), m) => Int.max (n', m)) | 639 foldl (fn ((_, n, ns), count) => |
636 (Int.max (n, count)) ns | 640 foldl (fn ((_, n', _), m) => Int.max (n', m)) |
641 (Int.max (n, count)) ns) count dts | |
637 | DVal (_, n, _, _, _) => Int.max (n, count) | 642 | DVal (_, n, _, _, _) => Int.max (n, count) |
638 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis | 643 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis |
639 | DExport _ => count | 644 | DExport _ => count |
640 | DTable _ => count | 645 | DTable _ => count |
641 | DSequence _ => count | 646 | DSequence _ => count |