Mercurial > urweb

comparison src/elaborate.sml @ 31:1c91c5e6840f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple signature matching
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Jun 2008 17:16:20 -0400
parents e6ccf961d8a3
children 0ff8c2728634
comparison
equal deleted inserted replaced
30:e6ccf961d8a3 31:1c91c5e6840f
133 val ktype_record = (L'.KRecord ktype, dummy) 133 val ktype_record = (L'.KRecord ktype, dummy)
134 134
135 val cerror = (L'.CError, dummy) 135 val cerror = (L'.CError, dummy)
136 val kerror = (L'.KError, dummy) 136 val kerror = (L'.KError, dummy)
137 val eerror = (L'.EError, dummy) 137 val eerror = (L'.EError, dummy)
138 val sgnerror = (L'.SgnError, dummy)
139 val strerror = (L'.StrError, dummy)
138 140
139 local 141 local
140 val count = ref 0 142 val count = ref 0
141 in 143 in
142 144
862 eprefaces' [("Constructor", p_con env c)]) 864 eprefaces' [("Constructor", p_con env c)])
863 | CunifsRemainExp (loc, e) => 865 | CunifsRemainExp (loc, e) =>
864 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression"; 866 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
865 eprefaces' [("Expression", p_exp env e)]) 867 eprefaces' [("Expression", p_exp env e)])
866 868
867 fun elabDecl env (d, loc) = 869 datatype sgn_error =
870 UnboundSgn of ErrorMsg.span * string
871 | UnmatchedSgi of L'.sgn_item
872 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
873 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
874
875 fun sgnError env err =
876 case err of
877 UnboundSgn (loc, s) =>
878 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
879 | UnmatchedSgi (sgi as (_, loc)) =>
880 (ErrorMsg.errorAt loc "Unmatched signature item";
881 eprefaces' [("Item", p_sgn_item env sgi)])
882 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
883 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
884 eprefaces' [("Item 1", p_sgn_item env sgi1),
885 ("Item 2", p_sgn_item env sgi2),
886 ("Kind 1", p_kind k1),
887 ("Kind 2", p_kind k2)];
888 kunifyError kerr)
889 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
890 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
891 eprefaces' [("Item 1", p_sgn_item env sgi1),
892 ("Item 2", p_sgn_item env sgi2),
893 ("Con 1", p_con env c1),
894 ("Con 2", p_con env c2)];
895 cunifyError env cerr)
896
897 datatype str_error =
898 UnboundStr of ErrorMsg.span * string
899
900 fun strError env err =
901 case err of
902 UnboundStr (loc, s) =>
903 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
904
905
906 fun elabSgn_item ((sgi, loc), env) =
907 let
908
909 in
910 resetKunif ();
911 resetCunif ();
912 case sgi of
913 L.SgiConAbs (x, k) =>
914 let
915 val k' = elabKind k
916
917 val (env', n) = E.pushCNamed env x k' NONE
918 in
919 if ErrorMsg.anyErrors () then
920 ()
921 else (
922 if kunifsInKind k' then
923 declError env (KunifsRemainKind (loc, k'))
924 else
925 ()
926 );
927
928 ((L'.SgiConAbs (x, n, k'), loc), env')
929 end
930
931 | L.SgiCon (x, ko, c) =>
932 let
933 val k' = case ko of
934 NONE => kunif ()
935 | SOME k => elabKind k
936
937 val (c', ck) = elabCon env c
938 val (env', n) = E.pushCNamed env x k' (SOME c')
939 in
940 checkKind env c' ck k';
941
942 if ErrorMsg.anyErrors () then
943 ()
944 else (
945 if kunifsInKind k' then
946 declError env (KunifsRemainKind (loc, k'))
947 else
948 ();
949
950 if kunifsInCon c' then
951 declError env (KunifsRemainCon (loc, c'))
952 else
953 ()
954 );
955
956 ((L'.SgiCon (x, n, k', c'), loc), env')
957 end
958
959 | L.SgiVal (x, c) =>
960 let
961 val (c', ck) = elabCon env c
962
963 val (env', n) = E.pushENamed env x c'
964 in
965 unifyKinds ck ktype;
966
967 if ErrorMsg.anyErrors () then
968 ()
969 else (
970 if kunifsInCon c' then
971 declError env (KunifsRemainCon (loc, c'))
972 else
973 ()
974 );
975
976 ((L'.SgiVal (x, n, c'), loc), env')
977 end
978
979 | L.SgiStr (x, sgn) =>
980 let
981 val sgn' = elabSgn env sgn
982 val (env', n) = E.pushStrNamed env x sgn'
983 in
984 ((L'.SgiStr (x, n, sgn'), loc), env')
985 end
986
987 end
988
989 and elabSgn env (sgn, loc) =
990 case sgn of
991 L.SgnConst sgis =>
992 let
993 val (sgis', _) = ListUtil.foldlMap elabSgn_item env sgis
994 in
995 (L'.SgnConst sgis', loc)
996 end
997 | L.SgnVar x =>
998 (case E.lookupSgn env x of
999 NONE =>
1000 (sgnError env (UnboundSgn (loc, x));
1001 (L'.SgnError, loc))
1002 | SOME (n, sgis) => (L'.SgnVar n, loc))
1003
1004 fun sgiOfDecl (d, loc) =
1005 case d of
1006 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
1007 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
1008 | L'.DSgn _ => NONE
1009 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
1010
1011 fun subSgn env (all1 as (sgn1, _)) (all2 as (sgn2, loc2)) =
1012 case (sgn1, sgn2) of
1013 (L'.SgnError, _) => ()
1014 | (_, L'.SgnError) => ()
1015
1016 | (L'.SgnVar n, _) =>
1017 subSgn env (#2 (E.lookupSgnNamed env n)) all2
1018 | (_, L'.SgnVar n) =>
1019 subSgn env all1 (#2 (E.lookupSgnNamed env n))
1020
1021 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1022 let
1023 fun folder (sgi2All as (sgi, _), env) =
1024 let
1025 fun seek p =
1026 let
1027 fun seek env ls =
1028 case ls of
1029 [] => (sgnError env (UnmatchedSgi sgi2All);
1030 env)
1031 | h :: t =>
1032 case p h of
1033 NONE => seek (E.sgiBinds env h) t
1034 | SOME env => env
1035 in
1036 seek env sgis1
1037 end
1038 in
1039 case sgi of
1040 L'.SgiConAbs (x, n2, k2) =>
1041 seek (fn sgi1All as (sgi1, _) =>
1042 let
1043 fun found (x, n1, k1, co1) =
1044 let
1045 val () = unifyKinds k1 k2
1046 handle KUnify (k1, k2, err) =>
1047 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
1048 val env = E.pushCNamedAs env x n1 k1 co1
1049 in
1050 SOME (if n1 = n2 then
1051 env
1052 else
1053 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
1054 end
1055 in
1056 case sgi1 of
1057 L'.SgiConAbs (x, n1, k1) => found (x, n1, k1, NONE)
1058 | L'.SgiCon (x, n1, k1, c1) => found (x, n1, k1, SOME c1)
1059 | _ => NONE
1060 end)
1061
1062 | L'.SgiCon (x, n2, k2, c2) =>
1063 seek (fn sgi1All as (sgi1, _) =>
1064 case sgi1 of
1065 L'.SgiCon (x, n1, k1, c1) =>
1066 let
1067 val () = unifyCons env c1 c2
1068 handle CUnify (c1, c2, err) =>
1069 sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err))
1070 in
1071 SOME (E.pushCNamedAs env x n2 k2 (SOME c2))
1072 end
1073 | _ => NONE)
1074
1075 | _ => raise Fail "Not ready for more sig matching"
1076 end
1077 in
1078 ignore (foldl folder env sgis2)
1079 end
1080
1081
1082 fun elabDecl ((d, loc), env) =
868 let 1083 let
869 1084
870 in 1085 in
871 resetKunif (); 1086 resetKunif ();
872 resetCunif (); 1087 resetCunif ();
894 declError env (KunifsRemainCon (loc, c')) 1109 declError env (KunifsRemainCon (loc, c'))
895 else 1110 else
896 () 1111 ()
897 ); 1112 );
898 1113
899 (env', 1114 ((L'.DCon (x, n, k', c'), loc), env')
900 (L'.DCon (x, n, k', c'), loc))
901 end 1115 end
902 | L.DVal (x, co, e) => 1116 | L.DVal (x, co, e) =>
903 let 1117 let
904 val (c', ck) = case co of 1118 val (c', ck) = case co of
905 NONE => (cunif ktype, ktype) 1119 NONE => (cunif ktype, ktype)
931 if cunifsInExp e' then 1145 if cunifsInExp e' then
932 declError env (CunifsRemainExp (loc, e')) 1146 declError env (CunifsRemainExp (loc, e'))
933 else 1147 else
934 ()); 1148 ());
935 1149
936 (env', 1150 ((L'.DVal (x, n, c', e'), loc), env')
937 (L'.DVal (x, n, c', e'), loc))
938 end 1151 end
939 1152
940 | L.DSgn _ => raise Fail "Not ready to elaborate signature" 1153 | L.DSgn (x, sgn) =>
941 | L.DStr _ => raise Fail "Not ready to elaborate structure" 1154 let
1155 val sgn' = elabSgn env sgn
1156 val (env', n) = E.pushSgnNamed env x sgn'
1157 in
1158 ((L'.DSgn (x, n, sgn'), loc), env')
1159 end
1160
1161 | L.DStr (x, sgno, str) =>
1162 let
1163 val formal = Option.map (elabSgn env) sgno
1164 val (str', actual) = elabStr env str
1165
1166 val sgn' = case formal of
1167 NONE => actual
1168 | SOME formal =>
1169 (subSgn env actual formal;
1170 formal)
1171
1172 val (env', n) = E.pushStrNamed env x sgn'
1173 in
1174 ((L'.DStr (x, n, sgn', str'), loc), env')
1175 end
942 end 1176 end
943 1177
944 fun elabFile env ds = 1178 and elabStr env (str, loc) =
945 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds 1179 case str of
1180 L.StrConst ds =>
1181 let
1182 val (ds', env') = ListUtil.foldlMap elabDecl env ds
1183 val sgis = List.mapPartial sgiOfDecl ds'
1184 in
1185 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
1186 end
1187 | L.StrVar x =>
1188 (case E.lookupStr env x of
1189 NONE =>
1190 (strError env (UnboundStr (loc, x));
1191 (strerror, sgnerror))
1192 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
1193
1194 val elabFile = ListUtil.foldlMap elabDecl
946 1195
947 end 1196 end