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