Mercurial > urweb

comparison src/explify.sml @ 806:0e554bfd6d6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)