Mercurial > urweb

comparison src/elaborate.sml @ 42:b3fbbc6cb1e5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating 'where'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 16:35:40 -0400
parents 1405d8c26790
children d94c484337d0
comparison
equal deleted inserted replaced
41:1405d8c26790 42:b3fbbc6cb1e5
237 ((L'.CRel n, loc), k) 237 ((L'.CRel n, loc), k)
238 | E.Named (n, k) => 238 | E.Named (n, k) =>
239 ((L'.CNamed n, loc), k)) 239 ((L'.CNamed n, loc), k))
240 | L.CVar (m1 :: ms, s) => 240 | L.CVar (m1 :: ms, s) =>
241 (case E.lookupStr env m1 of 241 (case E.lookupStr env m1 of
242 NONE => (conError env (UnboundStrInCon (loc, s)); 242 NONE => (conError env (UnboundStrInCon (loc, m1));
243 (cerror, kerror)) 243 (cerror, kerror))
244 | SOME (n, sgn) => 244 | SOME (n, sgn) =>
245 let 245 let
246 val (str, sgn) = foldl (fn (m, (str, sgn)) => 246 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
247 case E.projectStr env {sgn = sgn, str = str, field = m} of 247 case E.projectStr env {sgn = sgn, str = str, field = m} of
822 (eerror, cerror)) 822 (eerror, cerror))
823 | E.Rel (n, t) => ((L'.ERel n, loc), t) 823 | E.Rel (n, t) => ((L'.ERel n, loc), t)
824 | E.Named (n, t) => ((L'.ENamed n, loc), t)) 824 | E.Named (n, t) => ((L'.ENamed n, loc), t))
825 | L.EVar (m1 :: ms, s) => 825 | L.EVar (m1 :: ms, s) =>
826 (case E.lookupStr env m1 of 826 (case E.lookupStr env m1 of
827 NONE => (expError env (UnboundStrInExp (loc, s)); 827 NONE => (expError env (UnboundStrInExp (loc, m1));
828 (eerror, cerror)) 828 (eerror, cerror))
829 | SOME (n, sgn) => 829 | SOME (n, sgn) =>
830 let 830 let
831 val (str, sgn) = foldl (fn (m, (str, sgn)) => 831 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
832 case E.projectStr env {sgn = sgn, str = str, field = m} of 832 case E.projectStr env {sgn = sgn, str = str, field = m} of
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 | SgnWrongForm of L'.sgn * L'.sgn
972 | UnWhereable of L'.sgn * string
972 973
973 fun sgnError env err = 974 fun sgnError env err =
974 case err of 975 case err of
975 UnboundSgn (loc, s) => 976 UnboundSgn (loc, s) =>
976 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 977 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
993 cunifyError env cerr) 994 cunifyError env cerr)
994 | SgnWrongForm (sgn1, sgn2) => 995 | SgnWrongForm (sgn1, sgn2) =>
995 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; 996 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
996 eprefaces' [("Sig 1", p_sgn env sgn1), 997 eprefaces' [("Sig 1", p_sgn env sgn1),
997 ("Sig 2", p_sgn env sgn2)]) 998 ("Sig 2", p_sgn env sgn2)])
999 | UnWhereable (sgn, x) =>
1000 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
1001 eprefaces' [("Signature", p_sgn env sgn),
1002 ("Field", PD.string x)])
998 1003
999 datatype str_error = 1004 datatype str_error =
1000 UnboundStr of ErrorMsg.span * string 1005 UnboundStr of ErrorMsg.span * string
1001 1006
1002 fun strError env err = 1007 fun strError env err =
1003 case err of 1008 case err of
1004 UnboundStr (loc, s) => 1009 UnboundStr (loc, s) =>
1005 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1010 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1006 1011
1012 val hnormSgn = E.hnormSgn
1007 1013
1008 fun elabSgn_item ((sgi, loc), env) = 1014 fun elabSgn_item ((sgi, loc), env) =
1009 let 1015 let
1010 1016
1011 in 1017 in
1108 val (env', n) = E.pushStrNamed env m dom' 1114 val (env', n) = E.pushStrNamed env m dom'
1109 val ran' = elabSgn env' ran 1115 val ran' = elabSgn env' ran
1110 in 1116 in
1111 (L'.SgnFun (m, n, dom', ran'), loc) 1117 (L'.SgnFun (m, n, dom', ran'), loc)
1112 end 1118 end
1119 | L.SgnWhere (sgn, x, c) =>
1120 let
1121 val sgn' = elabSgn env sgn
1122 val (c', ck) = elabCon env c
1123 in
1124 case #1 (hnormSgn env sgn') of
1125 L'.SgnError => sgnerror
1126 | L'.SgnConst sgis =>
1127 if List.exists (fn (L'.SgiConAbs (x, _, k), _) =>
1128 (unifyKinds k ck;
1129 true)
1130 | _ => false) sgis then
1131 (L'.SgnWhere (sgn', x, c'), loc)
1132 else
1133 (sgnError env (UnWhereable (sgn', x));
1134 sgnerror)
1135 | _ => (sgnError env (UnWhereable (sgn', x));
1136 sgnerror)
1137 end
1113 1138
1114 fun sgiOfDecl (d, loc) = 1139 fun sgiOfDecl (d, loc) =
1115 case d of 1140 case d of
1116 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) 1141 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
1117 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) 1142 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
1118 | L'.DSgn _ => NONE 1143 | L'.DSgn _ => NONE
1119 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) 1144 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
1120
1121 fun hnormSgn env (all as (sgn, _)) =
1122 case sgn of
1123 L'.SgnError => all
1124 | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n))
1125 | L'.SgnConst _ => all
1126 | L'.SgnFun _ => all
1127 1145
1128 fun subSgn env sgn1 (sgn2 as (_, loc2)) = 1146 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
1129 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 1147 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1130 (L'.SgnError, _) => () 1148 (L'.SgnError, _) => ()
1131 | (_, L'.SgnError) => () 1149 | (_, L'.SgnError) => ()
1238 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1256 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1239 | (L'.SgiStr (x, n, sgn), loc) => 1257 | (L'.SgiStr (x, n, sgn), loc) =>
1240 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1258 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1241 | x => x) sgis), #2 sgn) 1259 | x => x) sgis), #2 sgn)
1242 | L'.SgnFun _ => sgn 1260 | L'.SgnFun _ => sgn
1261 | L'.SgnWhere _ => sgn
1243 1262
1244 fun elabDecl ((d, loc), env) = 1263 fun elabDecl ((d, loc), env) =
1245 let 1264 let
1246 1265
1247 in 1266 in
1382 val formal = 1401 val formal =
1383 case ranO of 1402 case ranO of
1384 NONE => actual 1403 NONE => actual
1385 | SOME ran => 1404 | SOME ran =>
1386 let 1405 let
1387 val ran' = elabSgn env ran 1406 val ran' = elabSgn env' ran
1388 in 1407 in
1389 subSgn env' actual ran'; 1408 subSgn env' actual ran';
1390 ran' 1409 ran'
1391 end 1410 end
1392 in 1411 in