Mercurial > urweb

comparison src/elaborate.sml @ 58:fd8a81ecd598

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
include
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 18:17:21 -0400
parents d3cc191cb25f
children abb2b32c19fb
comparison
equal deleted inserted replaced
57:618b7054f931 58:fd8a81ecd598
975 | UnmatchedSgi of L'.sgn_item 975 | UnmatchedSgi of L'.sgn_item
976 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 976 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
977 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error 977 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
978 | SgnWrongForm of L'.sgn * L'.sgn 978 | SgnWrongForm of L'.sgn * L'.sgn
979 | UnWhereable of L'.sgn * string 979 | UnWhereable of L'.sgn * string
980 | NotIncludable of L'.sgn
980 981
981 fun sgnError env err = 982 fun sgnError env err =
982 case err of 983 case err of
983 UnboundSgn (loc, s) => 984 UnboundSgn (loc, s) =>
984 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 985 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
1005 ("Sig 2", p_sgn env sgn2)]) 1006 ("Sig 2", p_sgn env sgn2)])
1006 | UnWhereable (sgn, x) => 1007 | UnWhereable (sgn, x) =>
1007 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; 1008 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
1008 eprefaces' [("Signature", p_sgn env sgn), 1009 eprefaces' [("Signature", p_sgn env sgn),
1009 ("Field", PD.string x)]) 1010 ("Field", PD.string x)])
1011 | NotIncludable sgn =>
1012 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
1013 eprefaces' [("Signature", p_sgn env sgn)])
1010 1014
1011 datatype str_error = 1015 datatype str_error =
1012 UnboundStr of ErrorMsg.span * string 1016 UnboundStr of ErrorMsg.span * string
1013 | NotFunctor of L'.sgn 1017 | NotFunctor of L'.sgn
1014 | FunctorRebind of ErrorMsg.span 1018 | FunctorRebind of ErrorMsg.span
1045 declError env (KunifsRemainKind (loc, k')) 1049 declError env (KunifsRemainKind (loc, k'))
1046 else 1050 else
1047 () 1051 ()
1048 ); 1052 );
1049 1053
1050 ((L'.SgiConAbs (x, n, k'), loc), env') 1054 ([(L'.SgiConAbs (x, n, k'), loc)], env')
1051 end 1055 end
1052 1056
1053 | L.SgiCon (x, ko, c) => 1057 | L.SgiCon (x, ko, c) =>
1054 let 1058 let
1055 val k' = case ko of 1059 val k' = case ko of
1073 declError env (KunifsRemainCon (loc, c')) 1077 declError env (KunifsRemainCon (loc, c'))
1074 else 1078 else
1075 () 1079 ()
1076 ); 1080 );
1077 1081
1078 ((L'.SgiCon (x, n, k', c'), loc), env') 1082 ([(L'.SgiCon (x, n, k', c'), loc)], env')
1079 end 1083 end
1080 1084
1081 | L.SgiVal (x, c) => 1085 | L.SgiVal (x, c) =>
1082 let 1086 let
1083 val (c', ck) = elabCon env c 1087 val (c', ck) = elabCon env c
1093 declError env (KunifsRemainCon (loc, c')) 1097 declError env (KunifsRemainCon (loc, c'))
1094 else 1098 else
1095 () 1099 ()
1096 ); 1100 );
1097 1101
1098 ((L'.SgiVal (x, n, c'), loc), env') 1102 ([(L'.SgiVal (x, n, c'), loc)], env')
1099 end 1103 end
1100 1104
1101 | L.SgiStr (x, sgn) => 1105 | L.SgiStr (x, sgn) =>
1102 let 1106 let
1103 val sgn' = elabSgn env sgn 1107 val sgn' = elabSgn env sgn
1104 val (env', n) = E.pushStrNamed env x sgn' 1108 val (env', n) = E.pushStrNamed env x sgn'
1105 in 1109 in
1106 ((L'.SgiStr (x, n, sgn'), loc), env') 1110 ([(L'.SgiStr (x, n, sgn'), loc)], env')
1107 end 1111 end
1108 1112
1113 | L.SgiInclude sgn =>
1114 let
1115 val sgn' = elabSgn env sgn
1116 in
1117 case #1 (hnormSgn env sgn') of
1118 L'.SgnConst sgis =>
1119 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
1120 | _ => (sgnError env (NotIncludable sgn');
1121 ([], env))
1122 end
1109 end 1123 end
1110 1124
1111 and elabSgn env (sgn, loc) = 1125 and elabSgn env (sgn, loc) =
1112 case sgn of 1126 case sgn of
1113 L.SgnConst sgis => 1127 L.SgnConst sgis =>
1114 let 1128 let
1115 val (sgis', _) = ListUtil.foldlMap elabSgn_item env sgis 1129 val (sgis', _) = ListUtil.foldlMapConcat elabSgn_item env sgis
1116 in 1130 in
1117 (L'.SgnConst sgis', loc) 1131 (L'.SgnConst sgis', loc)
1118 end 1132 end
1119 | L.SgnVar x => 1133 | L.SgnVar x =>
1120 (case E.lookupSgn env x of 1134 (case E.lookupSgn env x of