Mercurial > urweb

comparison src/elaborate.sml @ 41:1405d8c26790

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Beginning of functor elaboration
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 16:04:28 -0400
parents e3d3c2791105
children b3fbbc6cb1e5
comparison
equal deleted inserted replaced
40:e3d3c2791105 41:1405d8c26790
966 datatype sgn_error = 966 datatype sgn_error =
967 UnboundSgn of ErrorMsg.span * string 967 UnboundSgn of ErrorMsg.span * string
968 | UnmatchedSgi of L'.sgn_item 968 | UnmatchedSgi of L'.sgn_item
969 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 969 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
970 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error 970 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
971 | SgnWrongForm of L'.sgn * L'.sgn
971 972
972 fun sgnError env err = 973 fun sgnError env err =
973 case err of 974 case err of
974 UnboundSgn (loc, s) => 975 UnboundSgn (loc, s) =>
975 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 976 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
988 eprefaces' [("Item 1", p_sgn_item env sgi1), 989 eprefaces' [("Item 1", p_sgn_item env sgi1),
989 ("Item 2", p_sgn_item env sgi2), 990 ("Item 2", p_sgn_item env sgi2),
990 ("Con 1", p_con env c1), 991 ("Con 1", p_con env c1),
991 ("Con 2", p_con env c2)]; 992 ("Con 2", p_con env c2)];
992 cunifyError env cerr) 993 cunifyError env cerr)
994 | SgnWrongForm (sgn1, sgn2) =>
995 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
996 eprefaces' [("Sig 1", p_sgn env sgn1),
997 ("Sig 2", p_sgn env sgn2)])
993 998
994 datatype str_error = 999 datatype str_error =
995 UnboundStr of ErrorMsg.span * string 1000 UnboundStr of ErrorMsg.span * string
996 1001
997 fun strError env err = 1002 fun strError env err =
1095 (case E.lookupSgn env x of 1100 (case E.lookupSgn env x of
1096 NONE => 1101 NONE =>
1097 (sgnError env (UnboundSgn (loc, x)); 1102 (sgnError env (UnboundSgn (loc, x));
1098 (L'.SgnError, loc)) 1103 (L'.SgnError, loc))
1099 | SOME (n, sgis) => (L'.SgnVar n, loc)) 1104 | SOME (n, sgis) => (L'.SgnVar n, loc))
1100 | L.SgnFun _ => raise Fail "Elaborate functor sig" 1105 | L.SgnFun (m, dom, ran) =>
1106 let
1107 val dom' = elabSgn env dom
1108 val (env', n) = E.pushStrNamed env m dom'
1109 val ran' = elabSgn env' ran
1110 in
1111 (L'.SgnFun (m, n, dom', ran'), loc)
1112 end
1101 1113
1102 fun sgiOfDecl (d, loc) = 1114 fun sgiOfDecl (d, loc) =
1103 case d of 1115 case d of
1104 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) 1116 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
1105 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) 1117 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
1109 fun hnormSgn env (all as (sgn, _)) = 1121 fun hnormSgn env (all as (sgn, _)) =
1110 case sgn of 1122 case sgn of
1111 L'.SgnError => all 1123 L'.SgnError => all
1112 | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n)) 1124 | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n))
1113 | L'.SgnConst _ => all 1125 | L'.SgnConst _ => all
1126 | L'.SgnFun _ => all
1114 1127
1115 fun subSgn env sgn1 (sgn2 as (_, loc2)) = 1128 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
1116 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1129 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1117 (L'.SgnError, _) => () 1130 (L'.SgnError, _) => ()
1118 | (_, L'.SgnError) => () 1131 | (_, L'.SgnError) => ()
1119
1120 | (L'.SgnVar n, _) => raise Fail "subSgn: Variable remains"
1121 | (_, L'.SgnVar n) => raise Fail "subSgn: Variable remains"
1122 1132
1123 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 1133 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1124 let 1134 let
1125 fun folder (sgi2All as (sgi, _), env) = 1135 fun folder (sgi2All as (sgi, _), env) =
1126 let 1136 let
1140 in 1150 in
1141 case sgi of 1151 case sgi of
1142 L'.SgiConAbs (x, n2, k2) => 1152 L'.SgiConAbs (x, n2, k2) =>
1143 seek (fn sgi1All as (sgi1, _) => 1153 seek (fn sgi1All as (sgi1, _) =>
1144 let 1154 let
1145 fun found (x, n1, k1, co1) = 1155 fun found (x', n1, k1, co1) =
1146 let 1156 if x = x' then
1147 val () = unifyKinds k1 k2 1157 let
1148 handle KUnify (k1, k2, err) => 1158 val () = unifyKinds k1 k2
1149 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 1159 handle KUnify (k1, k2, err) =>
1150 val env = E.pushCNamedAs env x n1 k1 co1 1160 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
1151 in 1161 val env = E.pushCNamedAs env x n1 k1 co1
1152 SOME (if n1 = n2 then 1162 in
1153 env 1163 SOME (if n1 = n2 then
1154 else 1164 env
1155 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) 1165 else
1156 end 1166 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
1167 end
1168 else
1169 NONE
1157 in 1170 in
1158 case sgi1 of 1171 case sgi1 of
1159 L'.SgiConAbs (x, n1, k1) => found (x, n1, k1, NONE) 1172 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
1160 | L'.SgiCon (x, n1, k1, c1) => found (x, n1, k1, SOME c1) 1173 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
1161 | _ => NONE 1174 | _ => NONE
1162 end) 1175 end)
1163 1176
1164 | L'.SgiCon (x, n2, k2, c2) => 1177 | L'.SgiCon (x, n2, k2, c2) =>
1165 seek (fn sgi1All as (sgi1, _) => 1178 seek (fn sgi1All as (sgi1, _) =>
1166 case sgi1 of 1179 case sgi1 of
1167 L'.SgiCon (x, n1, k1, c1) => 1180 L'.SgiCon (x', n1, k1, c1) =>
1168 let 1181 if x = x' then
1169 val () = unifyCons env c1 c2 1182 let
1170 handle CUnify (c1, c2, err) => 1183 val () = unifyCons env c1 c2
1171 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) 1184 handle CUnify (c1, c2, err) =>
1172 in 1185 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
1173 SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) 1186 in
1174 end 1187 SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
1188 end
1189 else
1190 NONE
1175 | _ => NONE) 1191 | _ => NONE)
1176 1192
1177 | L'.SgiVal (x, n2, c2) => 1193 | L'.SgiVal (x, n2, c2) =>
1178 seek (fn sgi1All as (sgi1, _) => 1194 seek (fn sgi1All as (sgi1, _) =>
1179 case sgi1 of 1195 case sgi1 of
1180 L'.SgiVal (x, n1, c1) => 1196 L'.SgiVal (x', n1, c1) =>
1181 let 1197 if x = x' then
1182 val () = unifyCons env c1 c2 1198 let
1183 handle CUnify (c1, c2, err) => 1199 val () = unifyCons env c1 c2
1184 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) 1200 handle CUnify (c1, c2, err) =>
1185 in 1201 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
1186 SOME env 1202 in
1187 end 1203 SOME env
1204 end
1205 else
1206 NONE
1188 | _ => NONE) 1207 | _ => NONE)
1189 1208
1190 | L'.SgiStr (x, n2, sgn2) => 1209 | L'.SgiStr (x, n2, sgn2) =>
1191 seek (fn sgi1All as (sgi1, _) => 1210 seek (fn sgi1All as (sgi1, _) =>
1192 case sgi1 of 1211 case sgi1 of
1193 L'.SgiStr (x, n1, sgn1) => 1212 L'.SgiStr (x', n1, sgn1) =>
1194 (subSgn env sgn1 sgn2; 1213 if x = x' then
1195 SOME env) 1214 (subSgn env sgn1 sgn2;
1215 SOME env)
1216 else
1217 NONE
1196 | _ => NONE) 1218 | _ => NONE)
1197 (* Add type equations between structures here some day. *) 1219 (* Add type equations between structures here some day. *)
1198 end 1220 end
1199 in 1221 in
1200 ignore (foldl folder env sgis2) 1222 ignore (foldl folder env sgis2)
1201 end 1223 end
1224
1225 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
1226 (subSgn env dom2 dom1;
1227 subSgn env ran1 ran2)
1228
1229 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1202 1230
1203 fun selfify env {str, strs, sgn} = 1231 fun selfify env {str, strs, sgn} =
1204 case #1 (hnormSgn env sgn) of 1232 case #1 (hnormSgn env sgn) of
1205 L'.SgnError => sgn 1233 L'.SgnError => sgn
1206 | L'.SgnVar _ => sgn 1234 | L'.SgnVar _ => sgn
1209 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 1237 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1210 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1238 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1211 | (L'.SgiStr (x, n, sgn), loc) => 1239 | (L'.SgiStr (x, n, sgn), loc) =>
1212 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1240 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1213 | x => x) sgis), #2 sgn) 1241 | x => x) sgis), #2 sgn)
1242 | L'.SgnFun _ => sgn
1214 1243
1215 fun elabDecl ((d, loc), env) = 1244 fun elabDecl ((d, loc), env) =
1216 let 1245 let
1217 1246
1218 in 1247 in
1342 case E.projectStr env {str = str', sgn = sgn, field = x} of 1371 case E.projectStr env {str = str', sgn = sgn, field = x} of
1343 NONE => (strError env (UnboundStr (loc, x)); 1372 NONE => (strError env (UnboundStr (loc, x));
1344 (strerror, sgnerror)) 1373 (strerror, sgnerror))
1345 | SOME sgn => ((L'.StrProj (str', x), loc), sgn) 1374 | SOME sgn => ((L'.StrProj (str', x), loc), sgn)
1346 end 1375 end
1347 | L.StrFun _ => raise Fail "Elaborate functor" 1376 | L.StrFun (m, dom, ranO, str) =>
1377 let
1378 val dom' = elabSgn env dom
1379 val (env', n) = E.pushStrNamed env m dom'
1380 val (str', actual) = elabStr env' str
1381
1382 val formal =
1383 case ranO of
1384 NONE => actual
1385 | SOME ran =>
1386 let
1387 val ran' = elabSgn env ran
1388 in
1389 subSgn env' actual ran';
1390 ran'
1391 end
1392 in
1393 ((L'.StrFun (m, n, dom', formal, str'), loc),
1394 (L'.SgnFun (m, n, dom', formal), loc))
1395 end
1348 1396
1349 val elabFile = ListUtil.foldlMap elabDecl 1397 val elabFile = ListUtil.foldlMap elabDecl
1350 1398
1351 end 1399 end