Mercurial > urweb

comparison src/elaborate.sml @ 44:a9f3ce2d1b9b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating functor applications
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 17:04:08 -0400
parents d94c484337d0
children 44a1bc863f0f
comparison
equal deleted inserted replaced
43:d94c484337d0 44:a9f3ce2d1b9b
1012 eprefaces' [("Signature", p_sgn env sgn), 1012 eprefaces' [("Signature", p_sgn env sgn),
1013 ("Field", PD.string x)]) 1013 ("Field", PD.string x)])
1014 1014
1015 datatype str_error = 1015 datatype str_error =
1016 UnboundStr of ErrorMsg.span * string 1016 UnboundStr of ErrorMsg.span * string
1017 | NotFunctor of L'.sgn
1017 1018
1018 fun strError env err = 1019 fun strError env err =
1019 case err of 1020 case err of
1020 UnboundStr (loc, s) => 1021 UnboundStr (loc, s) =>
1021 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1022 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1023 | NotFunctor sgn =>
1024 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
1025 eprefaces' [("Signature", p_sgn env sgn)])
1022 1026
1023 val hnormSgn = E.hnormSgn 1027 val hnormSgn = E.hnormSgn
1024 1028
1025 fun elabSgn_item ((sgi, loc), env) = 1029 fun elabSgn_item ((sgi, loc), env) =
1026 let 1030 let
1277 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1281 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1278 | x => x) sgis), #2 sgn) 1282 | x => x) sgis), #2 sgn)
1279 | L'.SgnFun _ => sgn 1283 | L'.SgnFun _ => sgn
1280 | L'.SgnWhere _ => sgn 1284 | L'.SgnWhere _ => sgn
1281 1285
1286 fun selfifyAt env {str, sgn} =
1287 let
1288 fun self (str, _) =
1289 case str of
1290 L'.StrVar x => SOME (x, [])
1291 | L'.StrProj (str, x) =>
1292 (case self str of
1293 NONE => NONE
1294 | SOME (m, ms) => SOME (m, ms @ [x]))
1295 | _ => NONE
1296 in
1297 case self str of
1298 NONE => sgn
1299 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1300 end
1301
1282 fun elabDecl ((d, loc), env) = 1302 fun elabDecl ((d, loc), env) =
1283 let 1303 let
1284 1304
1285 in 1305 in
1286 resetKunif (); 1306 resetKunif ();
1361 | L.DStr (x, sgno, str) => 1381 | L.DStr (x, sgno, str) =>
1362 let 1382 let
1363 val formal = Option.map (elabSgn env) sgno 1383 val formal = Option.map (elabSgn env) sgno
1364 val (str', actual) = elabStr env str 1384 val (str', actual) = elabStr env str
1365 1385
1366 fun self (str, _) =
1367 case str of
1368 L'.StrVar x => SOME (x, [])
1369 | L'.StrProj (str, x) =>
1370 (case self str of
1371 NONE => NONE
1372 | SOME (m, ms) => SOME (m, ms @ [x]))
1373 | _ => NONE
1374
1375 val sgn' = case formal of 1386 val sgn' = case formal of
1376 NONE => 1387 NONE => selfifyAt env {str = str', sgn = actual}
1377 (case self str' of
1378 NONE => actual
1379 | SOME (str, strs) => selfify env {sgn = actual, str = str, strs = strs})
1380 | SOME formal => 1388 | SOME formal =>
1381 (subSgn env actual formal; 1389 (subSgn env actual formal;
1382 formal) 1390 formal)
1383 1391
1384 val (env', n) = E.pushStrNamed env x sgn' 1392 val (env', n) = E.pushStrNamed env x sgn'
1429 end 1437 end
1430 in 1438 in
1431 ((L'.StrFun (m, n, dom', formal, str'), loc), 1439 ((L'.StrFun (m, n, dom', formal, str'), loc),
1432 (L'.SgnFun (m, n, dom', formal), loc)) 1440 (L'.SgnFun (m, n, dom', formal), loc))
1433 end 1441 end
1442 | L.StrApp (str1, str2) =>
1443 let
1444 val (str1', sgn1) = elabStr env str1
1445 val (str2', sgn2) = elabStr env str2
1446 in
1447 case #1 (hnormSgn env sgn1) of
1448 L'.SgnError => (strerror, sgnerror)
1449 | L'.SgnFun (m, n, dom, ran) =>
1450 (subSgn env sgn2 dom;
1451 case #1 (hnormSgn env ran) of
1452 L'.SgnError => (strerror, sgnerror)
1453 | L'.SgnConst sgis =>
1454 ((L'.StrApp (str1', str2'), loc),
1455 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc))
1456 | _ => raise Fail "Unable to hnormSgn in functor application")
1457 | _ => (strError env (NotFunctor sgn1);
1458 (strerror, sgnerror))
1459 end
1434 1460
1435 val elabFile = ListUtil.foldlMap elabDecl 1461 val elabFile = ListUtil.foldlMap elabDecl
1436 1462
1437 end 1463 end