Mercurial > urweb

comparison src/elaborate.sml @ 91:4327abd52997

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basic XML stuff
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 16:26:28 -0400
parents 94ef20a31550
children 1a4c51fa615c
comparison
equal deleted inserted replaced
90:94ef20a31550 91:4327abd52997
904 in 904 in
905 unravel (t, e) 905 unravel (t, e)
906 end 906 end
907 907
908 fun elabExp (env, denv) (e, loc) = 908 fun elabExp (env, denv) (e, loc) =
909 case e of 909 let
910 L.EAnnot (e, t) => 910 fun doApp (e1, e2) =
911 let 911 let
912 val (e', et, gs1) = elabExp (env, denv) e 912 val (e1', t1, gs1) = elabExp (env, denv) e1
913 val (t', _, gs2) = elabCon (env, denv) t 913 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
914 val gs3 = checkCon (env, denv) e' et t' 914 val (e2', t2, gs3) = elabExp (env, denv) e2
915 in 915
916 (e', t', gs1 @ gs2 @ gs3) 916 val dom = cunif (loc, ktype)
917 end 917 val ran = cunif (loc, ktype)
918 918 val t = (L'.TFun (dom, ran), dummy)
919 | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) 919
920 | L.EVar ([], s) => 920 val gs4 = checkCon (env, denv) e1' t1 t
921 (case E.lookupE env s of 921 val gs5 = checkCon (env, denv) e2' t2 dom
922 E.NotBound => 922 in
923 (expError env (UnboundExp (loc, s)); 923 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
924 (eerror, cerror, [])) 924 end
925 | E.Rel (n, t) => ((L'.ERel n, loc), t, []) 925 in
926 | E.Named (n, t) => ((L'.ENamed n, loc), t, [])) 926 case e of
927 | L.EVar (m1 :: ms, s) => 927 L.EAnnot (e, t) =>
928 (case E.lookupStr env m1 of 928 let
929 NONE => (expError env (UnboundStrInExp (loc, m1)); 929 val (e', et, gs1) = elabExp (env, denv) e
930 (eerror, cerror, [])) 930 val (t', _, gs2) = elabCon (env, denv) t
931 | SOME (n, sgn) => 931 val gs3 = checkCon (env, denv) e' et t'
932 let 932 in
933 val (str, sgn) = foldl (fn (m, (str, sgn)) => 933 (e', t', gs1 @ gs2 @ gs3)
934 case E.projectStr env {sgn = sgn, str = str, field = m} of 934 end
935 NONE => (conError env (UnboundStrInCon (loc, m)); 935
936 (strerror, sgnerror)) 936 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
937 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 937 | L.EVar ([], s) =>
938 ((L'.StrVar n, loc), sgn) ms 938 (case E.lookupE env s of
939 939 E.NotBound =>
940 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of 940 (expError env (UnboundExp (loc, s));
941 NONE => (expError env (UnboundExp (loc, s)); 941 (eerror, cerror, []))
942 cerror) 942 | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
943 | SOME t => t 943 | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
944 in 944 | L.EVar (m1 :: ms, s) =>
945 ((L'.EModProj (n, ms, s), loc), t, []) 945 (case E.lookupStr env m1 of
946 end) 946 NONE => (expError env (UnboundStrInExp (loc, m1));
947 947 (eerror, cerror, []))
948 | L.EApp (e1, e2) => 948 | SOME (n, sgn) =>
949 let 949 let
950 val (e1', t1, gs1) = elabExp (env, denv) e1 950 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
951 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 951 case E.projectStr env {sgn = sgn, str = str, field = m} of
952 val (e2', t2, gs3) = elabExp (env, denv) e2 952 NONE => (conError env (UnboundStrInCon (loc, m));
953 953 (strerror, sgnerror))
954 val dom = cunif (loc, ktype) 954 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
955 val ran = cunif (loc, ktype) 955 ((L'.StrVar n, loc), sgn) ms
956 val t = (L'.TFun (dom, ran), dummy) 956
957 957 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
958 val gs4 = checkCon (env, denv) e1' t1 t 958 NONE => (expError env (UnboundExp (loc, s));
959 val gs5 = checkCon (env, denv) e2' t2 dom 959 cerror)
960 in 960 | SOME t => t
961 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5) 961 in
962 end 962 ((L'.EModProj (n, ms, s), loc), t, [])
963 | L.EAbs (x, to, e) => 963 end)
964 let 964
965 val (t', gs1) = case to of 965 | L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) =>
966 NONE => (cunif (loc, ktype), []) 966 let
967 | SOME t => 967 val (xml1', t1, gs1) = elabExp (env, denv) xml1
968 let 968 val (xml2', t2, gs2) = elabExp (env, denv) xml2
969 val (t', tk, gs) = elabCon (env, denv) t 969
970 in 970 val kunit = (L'.KUnit, loc)
971 checkKind env t' tk ktype; 971 val k = (L'.KRecord kunit, loc)
972 (t', gs) 972
973 end 973 val basis =
974 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e 974 case E.lookupStr env "Basis" of
975 in 975 NONE => raise Fail "elabExp: Unbound Basis"
976 ((L'.EAbs (x, t', et, e'), loc), 976 | SOME (n, _) => n
977 (L'.TFun (t', et), loc), 977
978 gs1 @ gs2) 978 fun xml () =
979 end
980 | L.ECApp (e, c) =>
981 let
982 val (e', et, gs1) = elabExp (env, denv) e
983 val (e', et, gs2) = elabHead (env, denv) e' et
984 val (c', ck, gs3) = elabCon (env, denv) c
985 val ((et', _), gs4) = hnormCon (env, denv) et
986 in
987 case et' of
988 L'.CError => (eerror, cerror, [])
989 | L'.TCFun (_, _, k, eb) =>
990 let
991 val () = checkKind env c' ck k
992 val eb' = subConInCon (0, c') eb
993 handle SynUnif => (expError env (Unif ("substitution", eb));
994 cerror)
995 in
996 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
997 end
998
999 | L'.CUnif _ =>
1000 (expError env (Unif ("application", et));
1001 (eerror, cerror, []))
1002
1003 | _ =>
1004 (expError env (WrongForm ("constructor function", e', et));
1005 (eerror, cerror, []))
1006 end
1007 | L.ECAbs (expl, x, k, e) =>
1008 let
1009 val expl' = elabExplicitness expl
1010 val k' = elabKind k
1011 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
1012 in
1013 ((L'.ECAbs (expl', x, k', e'), loc),
1014 (L'.TCFun (expl', x, k', et), loc),
1015 gs)
1016 end
1017
1018 | L.EDisjoint (c1, c2, e) =>
1019 let
1020 val (c1', k1, gs1) = elabCon (env, denv) c1
1021 val (c2', k2, gs2) = elabCon (env, denv) c2
1022
1023 val ku1 = kunif loc
1024 val ku2 = kunif loc
1025
1026 val (denv', gs3) = D.assert env denv (c1', c2')
1027 val (e', t, gs4) = elabExp (env, denv') e
1028 in
1029 checkKind env c1' k1 (L'.KRecord ku1, loc);
1030 checkKind env c2' k2 (L'.KRecord ku2, loc);
1031
1032 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
1033 end
1034
1035 | L.ERecord xes =>
1036 let
1037 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
1038 let
1039 val (x', xk, gs1) = elabCon (env, denv) x
1040 val (e', et, gs2) = elabExp (env, denv) e
1041 in
1042 checkKind env x' xk kname;
1043 ((x', e', et), gs1 @ gs2 @ gs)
1044 end)
1045 [] xes
1046
1047 val k = (L'.KType, loc)
1048
1049 fun prove (xets, gs) =
1050 case xets of
1051 [] => gs
1052 | (x, _, t) :: rest =>
1053 let 979 let
1054 val xc = (x, t) 980 val ns = cunif (loc, k)
1055 val r1 = (L'.CRecord (k, [xc]), loc)
1056 val gs = foldl (fn ((x', _, t'), gs) =>
1057 let
1058 val xc' = (x', t')
1059 val r2 = (L'.CRecord (k, [xc']), loc)
1060 in
1061 D.prove env denv (r1, r2, loc) @ gs
1062 end)
1063 gs rest
1064 in 981 in
1065 prove (rest, gs) 982 (ns, (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), ns), loc))
1066 end 983 end
1067 in 984
1068 ((L'.ERecord xes', loc), 985 val (ns1, c1) = xml ()
1069 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc), 986 val (ns2, c2) = xml ()
1070 prove (xes', gs)) 987
1071 end 988 val gs3 = checkCon (env, denv) xml1' t1 c1
1072 989 val gs4 = checkCon (env, denv) xml2' t2 c2
1073 | L.EField (e, c) => 990
1074 let 991 val (ns1, gs5) = hnormCon (env, denv) ns1
1075 val (e', et, gs1) = elabExp (env, denv) e 992 val (ns2, gs6) = hnormCon (env, denv) ns2
1076 val (c', ck, gs2) = elabCon (env, denv) c 993
1077 994 val cemp = (L'.CRecord (kunit, []), loc)
1078 val ft = cunif (loc, ktype) 995
1079 val rest = cunif (loc, ktype_record) 996 val (shared, ctx1, ctx2) =
1080 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 997 case (#1 ns1, #1 ns2) of
1081 998 (L'.CRecord (_, ns1), L'.CRecord (_, ns2)) =>
1082 val gs3 = 999 let
1083 checkCon (env, denv) e' et 1000 val ns = List.filter (fn ((nm, _), _) =>
1084 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 1001 case nm of
1085 val gs4 = D.prove env denv (first, rest, loc) 1002 L'.CName s =>
1086 in 1003 List.exists (fn ((L'.CName s', _), _) => s' = s
1087 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4) 1004 | _ => false) ns2
1088 end 1005 | _ => false) ns1
1089 1006 in
1090 | L.EFold => 1007 ((L'.CRecord (kunit, ns), loc), cunif (loc, k), cunif (loc, k))
1091 let 1008 end
1092 val dom = kunif loc 1009 | (_, L'.CRecord _) => (ns2, cemp, cemp)
1093 in 1010 | _ => (ns1, cemp, cemp)
1094 ((L'.EFold dom, loc), foldType (dom, loc), []) 1011
1095 end 1012 val ns1' = (L'.CConcat (shared, ctx1), loc)
1013 val ns2' = (L'.CConcat (shared, ctx2), loc)
1014
1015 val e = (L'.EModProj (basis, [], "join"), loc)
1016 val e = (L'.ECApp (e, shared), loc)
1017 val e = (L'.ECApp (e, ctx1), loc)
1018 val e = (L'.ECApp (e, ctx2), loc)
1019 val e = (L'.EApp (e, xml1'), loc)
1020 val e = (L'.EApp (e, xml2'), loc)
1021
1022 val t = (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), shared), loc)
1023
1024 fun doUnify (ns, ns') =
1025 let
1026 fun setEmpty c =
1027 let
1028 val ((c, _), gs) = hnormCon (env, denv) c
1029 in
1030 case c of
1031 L'.CUnif (_, _, _, r) =>
1032 (r := SOME cemp;
1033 gs)
1034 | L'.CConcat (_, c') => setEmpty c' @ gs
1035 | _ => gs
1036 end
1037
1038 val gs1 = unifyCons (env, denv) ns ns'
1039 val gs2 = setEmpty ns'
1040 val gs3 = unifyCons (env, denv) ns ns'
1041 in
1042 gs1 @ gs2 @ gs3
1043 end
1044
1045 val gs7 = doUnify (ns1, ns1')
1046 val gs8 = doUnify (ns2, ns2')
1047 in
1048 (e, t, (loc, env, denv, shared, ctx1)
1049 :: (loc, env, denv, shared, ctx2)
1050 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
1051 end
1052
1053 | L.EApp (e1, e2) =>
1054 let
1055 val (e1', t1, gs1) = elabExp (env, denv) e1
1056 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1057 val (e2', t2, gs3) = elabExp (env, denv) e2
1058
1059 val dom = cunif (loc, ktype)
1060 val ran = cunif (loc, ktype)
1061 val t = (L'.TFun (dom, ran), dummy)
1062
1063 val gs4 = checkCon (env, denv) e1' t1 t
1064 val gs5 = checkCon (env, denv) e2' t2 dom
1065 in
1066 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
1067 end
1068 | L.EAbs (x, to, e) =>
1069 let
1070 val (t', gs1) = case to of
1071 NONE => (cunif (loc, ktype), [])
1072 | SOME t =>
1073 let
1074 val (t', tk, gs) = elabCon (env, denv) t
1075 in
1076 checkKind env t' tk ktype;
1077 (t', gs)
1078 end
1079 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
1080 in
1081 ((L'.EAbs (x, t', et, e'), loc),
1082 (L'.TFun (t', et), loc),
1083 gs1 @ gs2)
1084 end
1085 | L.ECApp (e, c) =>
1086 let
1087 val (e', et, gs1) = elabExp (env, denv) e
1088 val (e', et, gs2) = elabHead (env, denv) e' et
1089 val (c', ck, gs3) = elabCon (env, denv) c
1090 val ((et', _), gs4) = hnormCon (env, denv) et
1091 in
1092 case et' of
1093 L'.CError => (eerror, cerror, [])
1094 | L'.TCFun (_, _, k, eb) =>
1095 let
1096 val () = checkKind env c' ck k
1097 val eb' = subConInCon (0, c') eb
1098 handle SynUnif => (expError env (Unif ("substitution", eb));
1099 cerror)
1100 in
1101 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
1102 end
1103
1104 | L'.CUnif _ =>
1105 (expError env (Unif ("application", et));
1106 (eerror, cerror, []))
1107
1108 | _ =>
1109 (expError env (WrongForm ("constructor function", e', et));
1110 (eerror, cerror, []))
1111 end
1112 | L.ECAbs (expl, x, k, e) =>
1113 let
1114 val expl' = elabExplicitness expl
1115 val k' = elabKind k
1116 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
1117 in
1118 ((L'.ECAbs (expl', x, k', e'), loc),
1119 (L'.TCFun (expl', x, k', et), loc),
1120 gs)
1121 end
1122
1123 | L.EDisjoint (c1, c2, e) =>
1124 let
1125 val (c1', k1, gs1) = elabCon (env, denv) c1
1126 val (c2', k2, gs2) = elabCon (env, denv) c2
1127
1128 val ku1 = kunif loc
1129 val ku2 = kunif loc
1130
1131 val (denv', gs3) = D.assert env denv (c1', c2')
1132 val (e', t, gs4) = elabExp (env, denv') e
1133 in
1134 checkKind env c1' k1 (L'.KRecord ku1, loc);
1135 checkKind env c2' k2 (L'.KRecord ku2, loc);
1136
1137 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
1138 end
1139
1140 | L.ERecord xes =>
1141 let
1142 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
1143 let
1144 val (x', xk, gs1) = elabCon (env, denv) x
1145 val (e', et, gs2) = elabExp (env, denv) e
1146 in
1147 checkKind env x' xk kname;
1148 ((x', e', et), gs1 @ gs2 @ gs)
1149 end)
1150 [] xes
1151
1152 val k = (L'.KType, loc)
1153
1154 fun prove (xets, gs) =
1155 case xets of
1156 [] => gs
1157 | (x, _, t) :: rest =>
1158 let
1159 val xc = (x, t)
1160 val r1 = (L'.CRecord (k, [xc]), loc)
1161 val gs = foldl (fn ((x', _, t'), gs) =>
1162 let
1163 val xc' = (x', t')
1164 val r2 = (L'.CRecord (k, [xc']), loc)
1165 in
1166 D.prove env denv (r1, r2, loc) @ gs
1167 end)
1168 gs rest
1169 in
1170 prove (rest, gs)
1171 end
1172 in
1173 ((L'.ERecord xes', loc),
1174 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
1175 prove (xes', gs))
1176 end
1177
1178 | L.EField (e, c) =>
1179 let
1180 val (e', et, gs1) = elabExp (env, denv) e
1181 val (c', ck, gs2) = elabCon (env, denv) c
1182
1183 val ft = cunif (loc, ktype)
1184 val rest = cunif (loc, ktype_record)
1185 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1186
1187 val gs3 =
1188 checkCon (env, denv) e' et
1189 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1190 val gs4 = D.prove env denv (first, rest, loc)
1191 in
1192 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
1193 end
1194
1195 | L.EFold =>
1196 let
1197 val dom = kunif loc
1198 in
1199 ((L'.EFold dom, loc), foldType (dom, loc), [])
1200 end
1201 end
1096 1202
1097 1203
1098 datatype decl_error = 1204 datatype decl_error =
1099 KunifsRemain of ErrorMsg.span 1205 KunifsRemain of L'.decl list
1100 | CunifsRemain of ErrorMsg.span 1206 | CunifsRemain of L'.decl list
1207
1208 fun lspan [] = ErrorMsg.dummySpan
1209 | lspan ((_, loc) :: _) = loc
1101 1210
1102 fun declError env err = 1211 fun declError env err =
1103 case err of 1212 case err of
1104 KunifsRemain loc => 1213 KunifsRemain ds =>
1105 ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration" 1214 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
1106 | CunifsRemain loc => 1215 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1107 ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration" 1216 | CunifsRemain ds =>
1217 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
1218 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1108 1219
1109 datatype sgn_error = 1220 datatype sgn_error =
1110 UnboundSgn of ErrorMsg.span * string 1221 UnboundSgn of ErrorMsg.span * string
1111 | UnmatchedSgi of L'.sgn_item 1222 | UnmatchedSgi of L'.sgn_item
1112 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 1223 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
1962 in 2073 in
1963 if ErrorMsg.anyErrors () then 2074 if ErrorMsg.anyErrors () then
1964 () 2075 ()
1965 else ( 2076 else (
1966 if List.exists kunifsInDecl ds then 2077 if List.exists kunifsInDecl ds then
1967 declError env (KunifsRemain (#2 d)) 2078 declError env (KunifsRemain ds)
1968 else 2079 else
1969 (); 2080 ();
1970 2081
1971 case ListUtil.search cunifsInDecl ds of 2082 case ListUtil.search cunifsInDecl ds of
1972 NONE => () 2083 NONE => ()
1973 | SOME loc => 2084 | SOME loc =>
1974 declError env (CunifsRemain loc) 2085 declError env (CunifsRemain ds)
1975 ); 2086 );
1976 2087
1977 (ds, (env, gs)) 2088 (ds, (env, gs))
1978 end 2089 end
1979 2090