Mercurial > urweb

comparison src/corify.sml @ 198:ab86aa858e6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'Option' datatype encoding
author Adam Chlipala <adamc@hcoop.net>
date Sat, 09 Aug 2008 19:23:31 -0400
parents df5fd8f6913a
children 0343557355fc
comparison
equal deleted inserted replaced
197:b1b9bcfd8c42 198:ab86aa858e6c
530 val co = Option.map (corifyCon st) co 530 val co = Option.map (corifyCon st) co
531 in 531 in
532 ((x, n, co), st) 532 ((x, n, co), st)
533 end) st xncs 533 end) st xncs
534 534
535 val dk = CoreUtil.classifyDatatype xncs 535 val dk = ElabUtil.classifyDatatype xncs
536 val t = (L'.CNamed n, loc) 536 val t = (L'.CNamed n, loc)
537 val nxs = length xs - 1 537 val nxs = length xs - 1
538 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs 538 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
539 val k = (L'.KType, loc) 539 val k = (L'.KType, loc)
540 val dcons = map (fn (x, n, to) => 540 val dcons = map (fn (x, n, to) =>
672 end 672 end
673 673
674 | L.SgiDatatype (x, n, xs, xnts) => 674 | L.SgiDatatype (x, n, xs, xnts) =>
675 let 675 let
676 val k = (L'.KType, loc) 676 val k = (L'.KType, loc)
677 val dk = ExplUtil.classifyDatatype xnts 677 val dk = ElabUtil.classifyDatatype xnts
678 val (st, n') = St.bindCon st x n 678 val (st, n') = St.bindCon st x n
679 val (xnts, (ds', st, cmap, conmap)) = 679 val (xnts, (ds', st, cmap, conmap)) =
680 ListUtil.foldlMap 680 ListUtil.foldlMap
681 (fn ((x', n, to), (ds', st, cmap, conmap)) => 681 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
682 let 682 let