Mercurial > urweb
comparison src/explify.sml @ 806:0e554bfd6d6a
Mutual datatypes through Corify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 15:22:05 -0400 |
parents | e2780d2f4afc |
children | 7f871c03e3a1 |
comparison
equal
deleted
inserted
replaced
805:e2780d2f4afc | 806:0e554bfd6d6a |
---|---|
135 | 135 |
136 fun explifySgi (sgi, loc) = | 136 fun explifySgi (sgi, loc) = |
137 case sgi of | 137 case sgi of |
138 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) | 138 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) |
139 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) | 139 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) |
140 (*| L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs, | 140 | L.SgiDatatype dts => SOME (L'.SgiDatatype (map (fn (x, n, xs, xncs) => |
141 map (fn (x, n, co) => | 141 (x, n, xs, |
142 (x, n, Option.map explifyCon co)) xncs), loc)*) | 142 map (fn (x, n, co) => |
143 | L.SgiDatatype _ => raise Fail "Explify SgiDatatype" | 143 (x, n, Option.map explifyCon co)) xncs)) dts), loc) |
144 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => | 144 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => |
145 SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) => | 145 SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) => |
146 (x, n, Option.map explifyCon co)) xncs), loc) | 146 (x, n, Option.map explifyCon co)) xncs), loc) |
147 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) | 147 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) |
148 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) | 148 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) |
162 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) | 162 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) |
163 | 163 |
164 fun explifyDecl (d, loc : EM.span) = | 164 fun explifyDecl (d, loc : EM.span) = |
165 case d of | 165 case d of |
166 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) | 166 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) |
167 (*| L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs, | 167 | L.DDatatype dts => SOME (L'.DDatatype (map (fn (x, n, xs, xncs) => |
168 map (fn (x, n, co) => | 168 (x, n, xs, |
169 (x, n, Option.map explifyCon co)) xncs), loc)*) | 169 map (fn (x, n, co) => |
170 | L.DDatatype _ => raise Fail "Explify DDatatype" | 170 (x, n, Option.map explifyCon co)) xncs)) dts), loc) |
171 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => | 171 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => |
172 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs, | 172 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs, |
173 map (fn (x, n, co) => | 173 map (fn (x, n, co) => |
174 (x, n, Option.map explifyCon co)) xncs), loc) | 174 (x, n, Option.map explifyCon co)) xncs), loc) |
175 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) | 175 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) |