Mercurial > urweb

comparison src/explify.sml @ 805:e2780d2f4afc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:14:17 -0400
parents 8688e01ae469
children 0e554bfd6d6a
comparison
equal deleted inserted replaced
804:10fe57e4a8c2 805:e2780d2f4afc
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 (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
141 map (fn (x, n, co) => 141 map (fn (x, n, co) =>
142 (x, n, Option.map explifyCon co)) xncs), loc) 142 (x, n, Option.map explifyCon co)) xncs), loc)*)
143 | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
143 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => 144 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
144 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) =>
145 (x, n, Option.map explifyCon co)) xncs), loc) 146 (x, n, Option.map explifyCon co)) xncs), loc)
146 | 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)
147 | 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)
161 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) 162 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
162 163
163 fun explifyDecl (d, loc : EM.span) = 164 fun explifyDecl (d, loc : EM.span) =
164 case d of 165 case d of
165 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)
166 | L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs, 167 (*| L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
167 map (fn (x, n, co) => 168 map (fn (x, n, co) =>
168 (x, n, Option.map explifyCon co)) xncs), loc) 169 (x, n, Option.map explifyCon co)) xncs), loc)*)
170 | L.DDatatype _ => raise Fail "Explify DDatatype"
169 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => 171 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
170 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs, 172 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
171 map (fn (x, n, co) => 173 map (fn (x, n, co) =>
172 (x, n, Option.map explifyCon co)) xncs), loc) 174 (x, n, Option.map explifyCon co)) xncs), loc)
173 | 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)