Mercurial > urweb

comparison src/expl_util.sml @ 806:0e554bfd6d6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:22:05 -0400
parents 354800878b4d
children 1aa9629e3a4c
comparison
equal deleted inserted replaced
805:e2780d2f4afc 806:0e554bfd6d6a
451 S.bind2 (kind ctx k, 451 S.bind2 (kind ctx k,
452 fn k' => 452 fn k' =>
453 S.map2 (con ctx c, 453 S.map2 (con ctx c,
454 fn c' => 454 fn c' =>
455 (SgiCon (x, n, k', c'), loc))) 455 (SgiCon (x, n, k', c'), loc)))
456 | SgiDatatype (x, n, xs, xncs) => 456 | SgiDatatype dts =>
457 S.map2 (ListUtil.mapfold (fn (x, n, c) => 457 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
458 case c of 458 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
459 NONE => S.return2 (x, n, c) 459 case c of
460 | SOME c => 460 NONE => S.return2 (x, n, c)
461 S.map2 (con ctx c, 461 | SOME c =>
462 fn c' => (x, n, SOME c'))) xncs, 462 S.map2 (con ctx c,
463 fn xncs' => 463 fn c' => (x, n, SOME c'))) xncs,
464 (SgiDatatype (x, n, xs, xncs'), loc)) 464 fn xncs' => (x, n, xs, xncs'))) dts,
465 fn dts' =>
466 (SgiDatatype dts', loc))
465 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => 467 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
466 S.map2 (ListUtil.mapfold (fn (x, n, c) => 468 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
467 case c of 469 case c of
468 NONE => S.return2 (x, n, c) 470 NONE => S.return2 (x, n, c)
469 | SOME c => 471 | SOME c =>
494 (case #1 si of 496 (case #1 si of
495 SgiConAbs (x, _, k) => 497 SgiConAbs (x, _, k) =>
496 bind (ctx, NamedC (x, k)) 498 bind (ctx, NamedC (x, k))
497 | SgiCon (x, _, k, _) => 499 | SgiCon (x, _, k, _) =>
498 bind (ctx, NamedC (x, k)) 500 bind (ctx, NamedC (x, k))
499 | SgiDatatype (x, n, _, xncs) => 501 | SgiDatatype dts =>
500 bind (ctx, NamedC (x, (KType, loc))) 502 foldl (fn ((x, _, ks, _), ctx) =>
503 let
504 val k' = (KType, loc)
505 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
506 k' ks
507 in
508 bind (ctx, NamedC (x, k))
509 end) ctx dts
501 | SgiDatatypeImp (x, _, _, _, _, _, _) => 510 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
502 bind (ctx, NamedC (x, (KType, loc))) 511 bind (ctx, NamedC (x, (KType, loc)))
503 | SgiVal _ => ctx 512 | SgiVal _ => ctx
504 | SgiStr (x, _, sgn) => 513 | SgiStr (x, _, sgn) =>
505 bind (ctx, Str (x, sgn)) 514 bind (ctx, Str (x, sgn))