comparison src/explify.sml @ 1864:1aa9629e3a4c

Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
author Adam Chlipala <adam@chlipala.net>
date Mon, 19 Aug 2013 12:25:32 -0400
parents bb942416bf1c
children 403f0cc65b9c
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
160 and explifySgn (sgn, loc) = 160 and explifySgn (sgn, loc) =
161 case sgn of 161 case sgn of
162 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc) 162 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
163 | L.SgnVar n => (L'.SgnVar n, loc) 163 | L.SgnVar n => (L'.SgnVar n, loc)
164 | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc) 164 | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
165 | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc) 165 | L.SgnWhere (sgn, ms, x, c) => (L'.SgnWhere (explifySgn sgn, ms, x, explifyCon c), loc)
166 | L.SgnProj x => (L'.SgnProj x, loc) 166 | L.SgnProj x => (L'.SgnProj x, loc)
167 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) 167 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
168 168
169 fun explifyDecl (d, loc : EM.span) = 169 fun explifyDecl (d, loc : EM.span) =
170 case d of 170 case d of