Mercurial > urweb

comparison src/corify.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children 9bbf4d383381
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
427 fun corifyPat st (p, loc) = 427 fun corifyPat st (p, loc) =
428 case p of 428 case p of
429 L.PWild => (L'.PWild, loc) 429 L.PWild => (L'.PWild, loc)
430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) 430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
431 | L.PPrim p => (L'.PPrim p, loc) 431 | L.PPrim p => (L'.PPrim p, loc)
432 | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc) 432 | L.PCon (dk, pc, ts, po) => raise Fail "Corify PCon" (*(L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)*)
433 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) 433 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
434 434
435 fun corifyExp st (e, loc) = 435 fun corifyExp st (e, loc) =
436 case e of 436 case e of
437 L.EPrim p => (L'.EPrim p, loc) 437 L.EPrim p => (L'.EPrim p, loc)
510 let 510 let
511 val (st, n) = St.bindCon st x n 511 val (st, n) = St.bindCon st x n
512 in 512 in
513 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 513 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
514 end 514 end
515 | L.DDatatype (x, n, xncs) => 515 | L.DDatatype (x, n, xs, xncs) => raise Fail "Corify DDatatype"
516 let 516 (*let
517 val (st, n) = St.bindCon st x n 517 val (st, n) = St.bindCon st x n
518 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 518 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
519 let 519 let
520 val st = St.bindConstructor st x n (L'.PConVar n) 520 val st = St.bindConstructor st x n (L'.PConVar n)
521 val st = St.bindConstructorVal st x n 521 val st = St.bindConstructorVal st x n
539 in 539 in
540 (L'.DVal (x, n, t, e, ""), loc) 540 (L'.DVal (x, n, t, e, ""), loc)
541 end) xncs 541 end) xncs
542 in 542 in
543 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) 543 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
544 end 544 end*)
545 | L.DDatatypeImp (x, n, m1, ms, s, xncs) => 545 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => raise Fail "Corify DDatatypeImp"
546 let 546 (*let
547 val (st, n) = St.bindCon st x n 547 val (st, n) = St.bindCon st x n
548 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 548 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
549 549
550 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms 550 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
551 val (_, {inner, ...}) = corifyStr (m, st) 551 val (_, {inner, ...}) = corifyStr (m, st)
569 in 569 in
570 (L'.DVal (x, n, t, e, x), loc) 570 (L'.DVal (x, n, t, e, x), loc)
571 end) xncs 571 end) xncs
572 in 572 in
573 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) 573 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
574 end 574 end*)
575 | L.DVal (x, n, t, e) => 575 | L.DVal (x, n, t, e) =>
576 let 576 let
577 val (st, n) = St.bindVal st x n 577 val (st, n) = St.bindVal st x n
578 val s = 578 val s =
579 if String.isPrefix "wrap_" x then 579 if String.isPrefix "wrap_" x then
646 cmap, 646 cmap,
647 conmap, 647 conmap,
648 st) 648 st)
649 end 649 end
650 650
651 | L.SgiDatatype (x, n, xnts) => 651 | L.SgiDatatype (x, n, xs, xnts) => raise Fail "Corify FFI SgiDatatype"
652 let 652 (*let
653 val dk = ExplUtil.classifyDatatype xnts 653 val dk = ExplUtil.classifyDatatype xnts
654 val (st, n') = St.bindCon st x n 654 val (st, n') = St.bindCon st x n
655 val (xnts, (ds', st, cmap, conmap)) = 655 val (xnts, (ds', st, cmap, conmap)) =
656 ListUtil.foldlMap 656 ListUtil.foldlMap
657 (fn ((x', n, to), (ds', st, cmap, conmap)) => 657 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
696 in 696 in
697 (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds, 697 (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds,
698 cmap, 698 cmap,
699 conmap, 699 conmap,
700 st) 700 st)
701 end 701 end*)
702 702
703 | L.SgiVal (x, _, c) => 703 | L.SgiVal (x, _, c) =>
704 (ds, 704 (ds,
705 SM.insert (cmap, x, corifyCon st c), 705 SM.insert (cmap, x, corifyCon st c),
706 conmap, 706 conmap,
809 end 809 end
810 810
811 fun maxName ds = foldl (fn ((d, _), n) => 811 fun maxName ds = foldl (fn ((d, _), n) =>
812 case d of 812 case d of
813 L.DCon (_, n', _, _) => Int.max (n, n') 813 L.DCon (_, n', _, _) => Int.max (n, n')
814 | L.DDatatype (_, n', _) => Int.max (n, n') 814 | L.DDatatype (_, n', _, _) => Int.max (n, n')
815 | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n') 815 | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
816 | L.DVal (_, n', _, _) => Int.max (n, n') 816 | L.DVal (_, n', _, _) => Int.max (n, n')
817 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis 817 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
818 | L.DSgn (_, n', _) => Int.max (n, n') 818 | L.DSgn (_, n', _) => Int.max (n, n')
819 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) 819 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
820 | L.DFfiStr (_, n', _) => Int.max (n, n') 820 | L.DFfiStr (_, n', _) => Int.max (n, n')