Mercurial > urweb

comparison src/elab_util.sml @ 329:eec65c11d3e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents 42dfb0d61cf0
children 9601c717d2f3
comparison
equal deleted inserted replaced
328:58f1260f293f 329:eec65c11d3e2
94 94
95 structure Con = struct 95 structure Con = struct
96 96
97 datatype binder = 97 datatype binder =
98 Rel of string * Elab.kind 98 Rel of string * Elab.kind
99 | Named of string * Elab.kind 99 | Named of string * int * Elab.kind
100 100
101 fun mapfoldB {kind = fk, con = fc, bind} = 101 fun mapfoldB {kind = fk, con = fc, bind} =
102 let 102 let
103 val mfk = Kind.mapfold fk 103 val mfk = Kind.mapfold fk
104 104
238 238
239 structure Exp = struct 239 structure Exp = struct
240 240
241 datatype binder = 241 datatype binder =
242 RelC of string * Elab.kind 242 RelC of string * Elab.kind
243 | NamedC of string * Elab.kind 243 | NamedC of string * int * Elab.kind
244 | RelE of string * Elab.con 244 | RelE of string * Elab.con
245 | NamedE of string * Elab.con 245 | NamedE of string * Elab.con
246 246
247 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 247 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
248 let 248 let
390 390
391 structure Sgn = struct 391 structure Sgn = struct
392 392
393 datatype binder = 393 datatype binder =
394 RelC of string * Elab.kind 394 RelC of string * Elab.kind
395 | NamedC of string * Elab.kind 395 | NamedC of string * int * Elab.kind
396 | Str of string * Elab.sgn 396 | Str of string * Elab.sgn
397 | Sgn of string * Elab.sgn 397 | Sgn of string * Elab.sgn
398 398
399 fun mapfoldB {kind, con, sgn_item, sgn, bind} = 399 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
400 let 400 let
477 and sg' ctx (sAll as (s, loc)) = 477 and sg' ctx (sAll as (s, loc)) =
478 case s of 478 case s of
479 SgnConst sgis => 479 SgnConst sgis =>
480 S.map2 (ListUtil.mapfoldB (fn (ctx, si) => 480 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
481 (case #1 si of 481 (case #1 si of
482 SgiConAbs (x, _, k) => 482 SgiConAbs (x, n, k) =>
483 bind (ctx, NamedC (x, k)) 483 bind (ctx, NamedC (x, n, k))
484 | SgiCon (x, _, k, _) => 484 | SgiCon (x, n, k, _) =>
485 bind (ctx, NamedC (x, k)) 485 bind (ctx, NamedC (x, n, k))
486 | SgiDatatype (x, n, _, xncs) => 486 | SgiDatatype (x, n, _, xncs) =>
487 bind (ctx, NamedC (x, (KType, loc))) 487 bind (ctx, NamedC (x, n, (KType, loc)))
488 | SgiDatatypeImp (x, _, _, _, _, _, _) => 488 | SgiDatatypeImp (x, n, _, _, _, _, _) =>
489 bind (ctx, NamedC (x, (KType, loc))) 489 bind (ctx, NamedC (x, n, (KType, loc)))
490 | SgiVal _ => ctx 490 | SgiVal _ => ctx
491 | SgiStr (x, _, sgn) => 491 | SgiStr (x, _, sgn) =>
492 bind (ctx, Str (x, sgn)) 492 bind (ctx, Str (x, sgn))
493 | SgiSgn (x, _, sgn) => 493 | SgiSgn (x, _, sgn) =>
494 bind (ctx, Sgn (x, sgn)) 494 bind (ctx, Sgn (x, sgn))
495 | SgiConstraint _ => ctx 495 | SgiConstraint _ => ctx
496 | SgiTable _ => ctx 496 | SgiTable _ => ctx
497 | SgiClassAbs (x, _) => 497 | SgiClassAbs (x, n) =>
498 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) 498 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
499 | SgiClass (x, _, _) => 499 | SgiClass (x, n, _) =>
500 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))), 500 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
501 sgi ctx si)) ctx sgis, 501 sgi ctx si)) ctx sgis,
502 fn sgis' => 502 fn sgis' =>
503 (SgnConst sgis', loc)) 503 (SgnConst sgis', loc))
504 504
505 | SgnVar _ => S.return2 sAll 505 | SgnVar _ => S.return2 sAll
540 540
541 structure Decl = struct 541 structure Decl = struct
542 542
543 datatype binder = 543 datatype binder =
544 RelC of string * Elab.kind 544 RelC of string * Elab.kind
545 | NamedC of string * Elab.kind 545 | NamedC of string * int * Elab.kind
546 | RelE of string * Elab.con 546 | RelE of string * Elab.con
547 | NamedE of string * Elab.con 547 | NamedE of string * Elab.con
548 | Str of string * Elab.sgn 548 | Str of string * Elab.sgn
549 | Sgn of string * Elab.sgn 549 | Sgn of string * Elab.sgn
550 550
592 and mfst' ctx (strAll as (str, loc)) = 592 and mfst' ctx (strAll as (str, loc)) =
593 case str of 593 case str of
594 StrConst ds => 594 StrConst ds =>
595 S.map2 (ListUtil.mapfoldB (fn (ctx, d) => 595 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
596 (case #1 d of 596 (case #1 d of
597 DCon (x, _, k, _) => 597 DCon (x, n, k, _) =>
598 bind (ctx, NamedC (x, k)) 598 bind (ctx, NamedC (x, n, k))
599 | DDatatype (x, n, xs, xncs) => 599 | DDatatype (x, n, xs, xncs) =>
600 let 600 let
601 val ctx = bind (ctx, NamedC (x, (KType, loc))) 601 val ctx = bind (ctx, NamedC (x, n, (KType, loc)))
602 in 602 in
603 foldl (fn ((x, _, co), ctx) => 603 foldl (fn ((x, _, co), ctx) =>
604 let 604 let
605 val t = 605 val t =
606 case co of 606 case co of
619 bind (ctx, NamedE (x, t)) 619 bind (ctx, NamedE (x, t))
620 end) 620 end)
621 ctx xncs 621 ctx xncs
622 end 622 end
623 | DDatatypeImp (x, n, m, ms, x', _, _) => 623 | DDatatypeImp (x, n, m, ms, x', _, _) =>
624 bind (ctx, NamedC (x, (KType, loc))) 624 bind (ctx, NamedC (x, n, (KType, loc)))
625 | DVal (x, _, c, _) => 625 | DVal (x, _, c, _) =>
626 bind (ctx, NamedE (x, c)) 626 bind (ctx, NamedE (x, c))
627 | DValRec vis => 627 | DValRec vis =>
628 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis 628 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
629 | DSgn (x, _, sgn) => 629 | DSgn (x, _, sgn) =>
635 | DConstraint _ => ctx 635 | DConstraint _ => ctx
636 | DExport _ => ctx 636 | DExport _ => ctx
637 | DTable (tn, x, n, c) => 637 | DTable (tn, x, n, c) =>
638 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc), 638 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
639 c), loc))) 639 c), loc)))
640 | DClass (x, _, _) => 640 | DClass (x, n, _) =>
641 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) 641 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
642 | DDatabase _ => ctx, 642 | DDatabase _ => ctx,
643 mfd ctx d)) ctx ds, 643 mfd ctx d)) ctx ds,
644 fn ds' => (StrConst ds', loc)) 644 fn ds' => (StrConst ds', loc))
645 | StrVar _ => S.return2 strAll 645 | StrVar _ => S.return2 strAll
646 | StrProj (str, x) => 646 | StrProj (str, x) =>