Mercurial > urweb

comparison src/elaborate.sml @ 43:d94c484337d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Subtyping for functor signatures
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 16:43:24 -0400
parents b3fbbc6cb1e5
children a9f3ce2d1b9b
comparison
equal deleted inserted replaced
42:b3fbbc6cb1e5 43:d94c484337d0
393 c 393 c
394 (*| L'.CUnif _ => raise SynUnif*) 394 (*| L'.CUnif _ => raise SynUnif*)
395 | _ => c, 395 | _ => c,
396 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) 396 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
397 | (ctx, _) => ctx} 397 | (ctx, _) => ctx}
398
399 fun subStrInSgn (m1, m2) =
400 U.Sgn.map {kind = fn k => k,
401 con = fn c as L'.CModProj (m1', ms, x) =>
402 if m1 = m1' then
403 L'.CModProj (m2, ms, x)
404 else
405 c
406 | c => c,
407 sgn_item = fn sgi => sgi,
408 sgn = fn sgn => sgn}
398 409
399 type record_summary = { 410 type record_summary = {
400 fields : (L'.con * L'.con) list, 411 fields : (L'.con * L'.con) list,
401 unifs : (L'.con * L'.con option ref) list, 412 unifs : (L'.con * L'.con option ref) list,
402 others : L'.con list 413 others : L'.con list
1239 in 1250 in
1240 ignore (foldl folder env sgis2) 1251 ignore (foldl folder env sgis2)
1241 end 1252 end
1242 1253
1243 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => 1254 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
1244 (subSgn env dom2 dom1; 1255 let
1245 subSgn env ran1 ran2) 1256 val ran1 =
1257 if n1 = n2 then
1258 ran1
1259 else
1260 subStrInSgn (n1, n2) ran1
1261 in
1262 subSgn env dom2 dom1;
1263 subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2
1264 end
1246 1265
1247 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1266 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1248 1267
1249 fun selfify env {str, strs, sgn} = 1268 fun selfify env {str, strs, sgn} =
1250 case #1 (hnormSgn env sgn) of 1269 case #1 (hnormSgn env sgn) of