Mercurial > urweb

comparison src/elaborate.sml @ 174:7ee424760d2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating module constructor patterns; parsing record patterns
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 11:28:55 -0400
parents 8221b95cc24c
children b2d752455182
comparison
equal deleted inserted replaced
173:8221b95cc24c 174:7ee424760d2f
810 | Unif of string * L'.con 810 | Unif of string * L'.con
811 | WrongForm of string * L'.exp * L'.con 811 | WrongForm of string * L'.exp * L'.con
812 | IncompatibleCons of L'.con * L'.con 812 | IncompatibleCons of L'.con * L'.con
813 | DuplicatePatternVariable of ErrorMsg.span * string 813 | DuplicatePatternVariable of ErrorMsg.span * string
814 | PatUnify of L'.pat * L'.con * L'.con * cunify_error 814 | PatUnify of L'.pat * L'.con * L'.con * cunify_error
815 | UnboundConstructor of ErrorMsg.span * string 815 | UnboundConstructor of ErrorMsg.span * string list * string
816 | PatHasArg of ErrorMsg.span 816 | PatHasArg of ErrorMsg.span
817 | PatHasNoArg of ErrorMsg.span 817 | PatHasNoArg of ErrorMsg.span
818 | Inexhaustive of ErrorMsg.span 818 | Inexhaustive of ErrorMsg.span
819 819
820 fun expError env err = 820 fun expError env err =
846 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern"; 846 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
847 eprefaces' [("Pattern", p_pat env p), 847 eprefaces' [("Pattern", p_pat env p),
848 ("Have con", p_con env c1), 848 ("Have con", p_con env c1),
849 ("Need con", p_con env c2)]; 849 ("Need con", p_con env c2)];
850 cunifyError env uerr) 850 cunifyError env uerr)
851 | UnboundConstructor (loc, s) => 851 | UnboundConstructor (loc, ms, s) =>
852 ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern") 852 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
853 | PatHasArg loc => 853 | PatHasArg loc =>
854 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument" 854 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
855 | PatHasNoArg loc => 855 | PatHasNoArg loc =>
856 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument" 856 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
857 | Inexhaustive loc => 857 | Inexhaustive loc =>
956 end 956 end
957 in 957 in
958 unravel (t, e) 958 unravel (t, e)
959 end 959 end
960 960
961 fun elabPat (pAll as (p, loc), (env, bound)) = 961 fun elabPat (pAll as (p, loc), (env, denv, bound)) =
962 let 962 let
963 val perror = (L'.PWild, loc) 963 val perror = (L'.PWild, loc)
964 val terror = (L'.CError, loc) 964 val terror = (L'.CError, loc)
965 val pterror = (perror, terror) 965 val pterror = (perror, terror)
966 val rerror = (pterror, (env, bound)) 966 val rerror = (pterror, (env, bound))
970 case (po, to) of 970 case (po, to) of
971 (NONE, SOME _) => (expError env (PatHasNoArg loc); 971 (NONE, SOME _) => (expError env (PatHasNoArg loc);
972 rerror) 972 rerror)
973 | (SOME _, NONE) => (expError env (PatHasArg loc); 973 | (SOME _, NONE) => (expError env (PatHasArg loc);
974 rerror) 974 rerror)
975 | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), (L'.CNamed dn, loc)), 975 | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), dn),
976 (env, bound)) 976 (env, bound))
977 | (SOME p, SOME t) => 977 | (SOME p, SOME t) =>
978 let 978 let
979 val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) 979 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
980 in 980 in
981 (((L'.PCon (pc, SOME p'), loc), (L'.CNamed dn, loc)), 981 (((L'.PCon (pc, SOME p'), loc), dn),
982 (env, bound)) 982 (env, bound))
983 end 983 end
984 in 984 in
985 case p of 985 case p of
986 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))), 986 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
998 end 998 end
999 | L.PPrim p => (((L'.PPrim p, loc), primType env p), 999 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
1000 (env, bound)) 1000 (env, bound))
1001 | L.PCon ([], x, po) => 1001 | L.PCon ([], x, po) =>
1002 (case E.lookupConstructor env x of 1002 (case E.lookupConstructor env x of
1003 NONE => (expError env (UnboundConstructor (loc, x)); 1003 NONE => (expError env (UnboundConstructor (loc, [], x));
1004 rerror) 1004 rerror)
1005 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn)) 1005 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc)))
1006 | L.PCon _ => raise Fail "uhoh" 1006 | L.PCon (m1 :: ms, x, po) =>
1007 (case E.lookupStr env m1 of
1008 NONE => (expError env (UnboundStrInExp (loc, m1));
1009 rerror)
1010 | SOME (n, sgn) =>
1011 let
1012 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1013 case E.projectStr env {sgn = sgn, str = str, field = m} of
1014 NONE => raise Fail "typeof: Unknown substructure"
1015 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1016 ((L'.StrVar n, loc), sgn) ms
1017 in
1018 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
1019 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
1020 rerror)
1021 | SOME (_, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn)
1022 end)
1023
1024 | L.PRecord _ => raise Fail "Elaborate PRecord"
1007 end 1025 end
1008 1026
1009 datatype coverage = 1027 datatype coverage =
1010 Wild 1028 Wild
1011 | None 1029 | None
1014 fun exhaustive (env, denv, t, ps) = 1032 fun exhaustive (env, denv, t, ps) =
1015 let 1033 let
1016 fun pcCoverage pc = 1034 fun pcCoverage pc =
1017 case pc of 1035 case pc of
1018 L'.PConVar n => n 1036 L'.PConVar n => n
1019 | _ => raise Fail "uh oh^2" 1037 | L'.PConProj (m1, ms, x) =>
1038 let
1039 val (str, sgn) = E.chaseMpath env (m1, ms)
1040 in
1041 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
1042 NONE => raise Fail "exhaustive: Can't project constructor"
1043 | SOME (n, _, _) => n
1044 end
1020 1045
1021 fun coverage (p, _) = 1046 fun coverage (p, _) =
1022 case p of 1047 case p of
1023 L'.PWild => Wild 1048 L'.PWild => Wild
1024 | L'.PVar _ => Wild 1049 | L'.PVar _ => Wild
1047 None => (false, []) 1072 None => (false, [])
1048 | Wild => (true, []) 1073 | Wild => (true, [])
1049 | Datatype cm => 1074 | Datatype cm =>
1050 let 1075 let
1051 val ((t, _), gs) = hnormCon (env, denv) t 1076 val ((t, _), gs) = hnormCon (env, denv) t
1077
1078 fun dtype cons =
1079 foldl (fn ((_, n, to), (total, gs)) =>
1080 case IM.find (cm, n) of
1081 NONE => (false, gs)
1082 | SOME c' =>
1083 case to of
1084 NONE => (total, gs)
1085 | SOME t' =>
1086 let
1087 val (total, gs') = isTotal (c', t')
1088 in
1089 (total, gs' @ gs)
1090 end)
1091 (true, gs) cons
1052 in 1092 in
1053 case t of 1093 case t of
1054 L'.CNamed n => 1094 L'.CNamed n =>
1055 let 1095 let
1056 val dt = E.lookupDatatype env n 1096 val dt = E.lookupDatatype env n
1057 val cons = E.constructors dt 1097 val cons = E.constructors dt
1058 in 1098 in
1059 foldl (fn ((_, n, to), (total, gs)) => 1099 dtype cons
1060 case IM.find (cm, n) of 1100 end
1061 NONE => (false, gs) 1101 | L'.CModProj (m1, ms, x) =>
1062 | SOME c' => 1102 let
1063 case to of 1103 val (str, sgn) = E.chaseMpath env (m1, ms)
1064 NONE => (total, gs) 1104 in
1065 | SOME t' => 1105 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
1066 let 1106 NONE => raise Fail "isTotal: Can't project datatype"
1067 val (total, gs') = isTotal (c', t') 1107 | SOME cons => dtype cons
1068 in
1069 (total, gs' @ gs)
1070 end)
1071 (true, gs) cons
1072 end 1108 end
1073 | L'.CError => (true, gs) 1109 | L'.CError => (true, gs)
1074 | _ => raise Fail "isTotal: Not a datatype" 1110 | _ => raise Fail "isTotal: Not a datatype"
1075 end 1111 end
1076 in 1112 in
1293 val (e', et, gs1) = elabExp (env, denv) e 1329 val (e', et, gs1) = elabExp (env, denv) e
1294 val result = cunif (loc, (L'.KType, loc)) 1330 val result = cunif (loc, (L'.KType, loc))
1295 val (pes', gs) = ListUtil.foldlMap 1331 val (pes', gs) = ListUtil.foldlMap
1296 (fn ((p, e), gs) => 1332 (fn ((p, e), gs) =>
1297 let 1333 let
1298 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) 1334 val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty))
1299 1335
1300 val gs1 = checkPatCon (env, denv) p' pt et 1336 val gs1 = checkPatCon (env, denv) p' pt et
1301 val (e', et, gs2) = elabExp (env, denv) e 1337 val (e', et, gs2) = elabExp (env, denv) e
1302 val gs3 = checkCon (env, denv) e' et result 1338 val gs3 = checkCon (env, denv) e' et result
1303 in 1339 in