Mercurial > urweb
diff src/corify.sml @ 806:0e554bfd6d6a
Mutual datatypes through Corify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 May 2009 15:22:05 -0400 |
| parents | 3b7e46790fa7 |
| children | 61a1f5c5ae2c |
line wrap: on
line diff
--- a/src/corify.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/corify.sml Sat May 16 15:22:05 2009 -0400 @@ -621,7 +621,8 @@ in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end - | L.DDatatype (x, n, xs, xncs) => + | L.DDatatype _ => raise Fail "Corify DDatatype" + (*| L.DDatatype (x, n, xs, xncs) => let val (st, n) = St.bindCon st x n val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => @@ -658,7 +659,7 @@ end) xncs in ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) - end + end*) | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => let val (st, n) = St.bindCon st x n @@ -795,7 +796,8 @@ trans) end - | L.SgiDatatype (x, n, xs, xnts) => + | L.SgiDatatype _ => raise Fail "Corify SgiDatatype" + (*| L.SgiDatatype (x, n, xs, xnts) => let val k = (L'.KType, loc) val dk = ElabUtil.classifyDatatype xnts @@ -856,7 +858,7 @@ conmap, st, trans) - end + end*) | L.SgiVal (x, _, c) => let @@ -1061,7 +1063,7 @@ fun maxName ds = foldl (fn ((d, _), n) => case d of L.DCon (_, n', _, _) => Int.max (n, n') - | L.DDatatype (_, n', _, _) => Int.max (n, n') + | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n') | L.DVal (_, n', _, _) => Int.max (n, n') | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis