Mercurial > urweb

comparison src/elaborate.sml @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents fb0388f1180e
children 07eed8386f07
comparison
equal deleted inserted replaced
1590:60d438cdb3a5 1591:20f898c29525
1253 1253
1254 datatype constraint = 1254 datatype constraint =
1255 Disjoint of D.goal 1255 Disjoint of D.goal
1256 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span 1256 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
1257 1257
1258 fun relocConstraint loc c =
1259 case c of
1260 Disjoint (_, a, b, c, d) => Disjoint (loc, a, b, c, d)
1261 | TypeClass (a, b, c, _) => TypeClass (a, b, c, loc)
1262
1258 val enD = map Disjoint 1263 val enD = map Disjoint
1259 1264
1260 fun isClassOrFolder env cl = 1265 fun isClassOrFolder env cl =
1261 E.isClass env cl 1266 E.isClass env cl
1262 orelse case hnormCon env cl of 1267 orelse case hnormCon env cl of
1349 (e, t, enD gs @ gs') 1354 (e, t, enD gs @ gs')
1350 end 1355 end
1351 else 1356 else
1352 (e, t, []) 1357 (e, t, [])
1353 | t => (e, t, []) 1358 | t => (e, t, [])
1359
1360 val (e, t, gs) = case infer of
1361 L.DontInfer => unravelKind (t, e)
1362 | _ => unravel (t, e)
1354 in 1363 in
1355 case infer of 1364 ((#1 e, loc), (#1 t, loc), map (relocConstraint loc) gs)
1356 L.DontInfer => unravelKind (t, e)
1357 | _ => unravel (t, e)
1358 end 1365 end
1359 1366
1360 fun elabPat (pAll as (p, loc), (env, bound)) = 1367 fun elabPat (pAll as (p, loc), (env, bound)) =
1361 let 1368 let
1362 val perror = (L'.PWild, loc) 1369 val perror = (L'.PWild, loc)
1863 Constraints = #Constraints r, 1870 Constraints = #Constraints r,
1864 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r, 1871 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r,
1865 Mods = #Mods r} 1872 Mods = #Mods r}
1866 end 1873 end
1867 1874
1875 fun chaseUnifs c =
1876 case #1 c of
1877 L'.CUnif (_, _, _, _, ref (SOME c)) => chaseUnifs c
1878 | _ => c
1879
1868 fun elabExp (env, denv) (eAll as (e, loc)) = 1880 fun elabExp (env, denv) (eAll as (e, loc)) =
1869 let 1881 let
1870 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 1882 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
1871 (*val befor = Time.now ()*) 1883 (*val befor = Time.now ()*)
1872 1884
1931 val () = checkCon env e2' t2 dom 1943 val () = checkCon env e2' t2 dom
1932 1944
1933 val ef = (L'.EApp (e1', e2'), loc) 1945 val ef = (L'.EApp (e1', e2'), loc)
1934 val (ef, et, gs3) = 1946 val (ef, et, gs3) =
1935 case findHead e1 e1' of 1947 case findHead e1 e1' of
1936 NONE => (ef, ran, []) 1948 NONE => (ef, (#1 (chaseUnifs ran), loc), [])
1937 | SOME infer => elabHead (env, denv) infer ef ran 1949 | SOME infer => elabHead (env, denv) infer ef ran
1938 in 1950 in
1939 (ef, et, gs1 @ gs2 @ gs3) 1951 (ef, et, gs1 @ gs2 @ gs3)
1940 end 1952 end
1941 | L.EAbs (x, to, e) => 1953 | L.EAbs (x, to, e) =>
1981 ("et", p_con env oldEt), 1993 ("et", p_con env oldEt),
1982 ("x", PD.string x), 1994 ("x", PD.string x),
1983 ("eb", p_con (E.pushCRel env x k) eb), 1995 ("eb", p_con (E.pushCRel env x k) eb),
1984 ("c", p_con env c'), 1996 ("c", p_con env c'),
1985 ("eb'", p_con env eb')];*) 1997 ("eb'", p_con env eb')];*)
1986 (ef, eb', gs1 @ enD gs2 @ gs3) 1998 (ef, (#1 eb', loc), gs1 @ enD gs2 @ gs3)
1987 end 1999 end
1988 2000
1989 | _ => 2001 | _ =>
1990 (expError env (WrongForm ("constructor function", e', et)); 2002 (expError env (WrongForm ("constructor function", e', et));
1991 (eerror, cerror, [])) 2003 (eerror, cerror, []))
2038 val c2 = cunif (loc, (L'.KRecord k2, loc)) 2050 val c2 = cunif (loc, (L'.KRecord k2, loc))
2039 val t' = cunif (loc, ktype) 2051 val t' = cunif (loc, ktype)
2040 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) 2052 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
2041 val gs2 = D.prove env denv (c1, c2, loc) 2053 val gs2 = D.prove env denv (c1, c2, loc)
2042 in 2054 in
2043 (e', t', enD gs2 @ gs1) 2055 (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1)
2044 end 2056 end
2045 2057
2046 | L.ERecord xes => 2058 | L.ERecord xes =>
2047 let 2059 let
2048 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 2060 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
2913 val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All)); 2925 val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All));
2914 env)) 2926 env))
2915 in 2927 in
2916 case sgi of 2928 case sgi of
2917 L'.SgiConAbs (x, n2, k2) => 2929 L'.SgiConAbs (x, n2, k2) =>
2918 seek (fn (env, sgi1All as (sgi1, _)) => 2930 seek (fn (env, sgi1All as (sgi1, loc)) =>
2919 let 2931 let
2920 fun found (x', n1, k1, co1) = 2932 fun found (x', n1, k1, co1) =
2921 if x = x' then 2933 if x = x' then
2922 let 2934 let
2923 val () = unifyKinds env k1 k2 2935 val () = unifyKinds env k1 k2
2924 handle KUnify (k1, k2, err) => 2936 handle KUnify (k1, k2, err) =>
2925 sgnError env (SgiWrongKind (strLoc, sgi1All, k1, 2937 sgnError env (SgiWrongKind (loc, sgi1All, k1,
2926 sgi2All, k2, err)) 2938 sgi2All, k2, err))
2927 val env = E.pushCNamedAs env x n1 k1 co1 2939 val env = E.pushCNamedAs env x n1 k1 co1
2928 in 2940 in
2929 SOME (if n1 = n2 then 2941 SOME (if n1 = n2 then
2930 env 2942 env
2967 | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c) 2979 | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c)
2968 | _ => NONE 2980 | _ => NONE
2969 end) 2981 end)
2970 2982
2971 | L'.SgiCon (x, n2, k2, c2) => 2983 | L'.SgiCon (x, n2, k2, c2) =>
2972 seek (fn (env, sgi1All as (sgi1, _)) => 2984 seek (fn (env, sgi1All as (sgi1, loc)) =>
2973 let 2985 let
2974 fun found (x', n1, k1, c1) = 2986 fun found (x', n1, k1, c1) =
2975 if x = x' then 2987 if x = x' then
2976 let 2988 let
2977 val c2 = sub2 c2 2989 val c2 = sub2 c2
2989 end 3001 end
2990 in 3002 in
2991 (unifyCons env loc c1 c2; 3003 (unifyCons env loc c1 c2;
2992 good ()) 3004 good ())
2993 handle CUnify (c1, c2, err) => 3005 handle CUnify (c1, c2, err) =>
2994 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, 3006 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
2995 sgi2All, c2, err)); 3007 sgi2All, c2, err));
2996 good ()) 3008 good ())
2997 end 3009 end
2998 else 3010 else
2999 NONE 3011 NONE
3004 | _ => NONE 3016 | _ => NONE
3005 end) 3017 end)
3006 3018
3007 | L'.SgiDatatype dts2 => 3019 | L'.SgiDatatype dts2 =>
3008 let 3020 let
3009 fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = 3021 fun found' (sgi1All as (_, loc), (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) =
3010 if x1 <> x2 then 3022 if x1 <> x2 then
3011 NONE 3023 NONE
3012 else 3024 else
3013 let 3025 let
3014 fun mismatched ue = 3026 fun mismatched ue =
3015 (sgnError env (SgiMismatchedDatatypes (strLoc, sgi1All, sgi2All, ue)); 3027 (sgnError env (SgiMismatchedDatatypes (loc, sgi1All, sgi2All, ue));
3016 SOME env) 3028 SOME env)
3017 3029
3018 val k = (L'.KType, loc) 3030 val k = (L'.KType, loc)
3019 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 3031 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
3020 3032
3093 | _ => NONE 3105 | _ => NONE
3094 end) 3106 end)
3095 end 3107 end
3096 3108
3097 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => 3109 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
3098 seek (fn (env, sgi1All as (sgi1, _)) => 3110 seek (fn (env, sgi1All as (sgi1, loc)) =>
3099 case sgi1 of 3111 case sgi1 of
3100 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => 3112 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
3101 if x = x' then 3113 if x = x' then
3102 let 3114 let
3103 val k = (L'.KType, loc) 3115 val k = (L'.KType, loc)
3115 end 3127 end
3116 in 3128 in
3117 (unifyCons env loc t1 t2; 3129 (unifyCons env loc t1 t2;
3118 good ()) 3130 good ())
3119 handle CUnify (c1, c2, err) => 3131 handle CUnify (c1, c2, err) =>
3120 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err)); 3132 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
3121 good ()) 3133 good ())
3122 end 3134 end
3123 else 3135 else
3124 NONE 3136 NONE
3125 3137
3126 | _ => NONE) 3138 | _ => NONE)
3127 3139
3128 | L'.SgiVal (x, n2, c2) => 3140 | L'.SgiVal (x, n2, c2) =>
3129 seek (fn (env, sgi1All as (sgi1, _)) => 3141 seek (fn (env, sgi1All as (sgi1, loc)) =>
3130 case sgi1 of 3142 case sgi1 of
3131 L'.SgiVal (x', n1, c1) => 3143 L'.SgiVal (x', n1, c1) =>
3132 if x = x' then 3144 if x = x' then
3133 ((*prefaces "val" [("x", PD.string x), 3145 ((*prefaces "val" [("x", PD.string x),
3134 ("n1", PD.string (Int.toString n1)), 3146 ("n1", PD.string (Int.toString n1)),
3136 ("c2", p_con env c2), 3148 ("c2", p_con env c2),
3137 ("c2'", p_con env (sub2 c2))];*) 3149 ("c2'", p_con env (sub2 c2))];*)
3138 unifyCons env loc c1 (sub2 c2); 3150 unifyCons env loc c1 (sub2 c2);
3139 SOME env) 3151 SOME env)
3140 handle CUnify (c1, c2, err) => 3152 handle CUnify (c1, c2, err) =>
3141 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err)); 3153 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
3142 SOME env) 3154 SOME env)
3143 else 3155 else
3144 NONE 3156 NONE
3145 | _ => NONE) 3157 | _ => NONE)
3146 3158
3147 | L'.SgiStr (x, n2, sgn2) => 3159 | L'.SgiStr (x, n2, sgn2) =>
3148 seek (fn (env, sgi1All as (sgi1, _)) => 3160 seek (fn (env, sgi1All as (sgi1, loc)) =>
3149 case sgi1 of 3161 case sgi1 of
3150 L'.SgiStr (x', n1, sgn1) => 3162 L'.SgiStr (x', n1, sgn1) =>
3151 if x = x' then 3163 if x = x' then
3152 let 3164 let
3153 val () = subSgn' counterparts env strLoc sgn1 sgn2 3165 val () = subSgn' counterparts env loc sgn1 sgn2
3154 val env = E.pushStrNamedAs env x n1 sgn1 3166 val env = E.pushStrNamedAs env x n1 sgn1
3155 val env = if n1 = n2 then 3167 val env = if n1 = n2 then
3156 env 3168 env
3157 else 3169 else
3158 E.pushStrNamedAs env x n2 3170 E.pushStrNamedAs env x n2
3164 else 3176 else
3165 NONE 3177 NONE
3166 | _ => NONE) 3178 | _ => NONE)
3167 3179
3168 | L'.SgiSgn (x, n2, sgn2) => 3180 | L'.SgiSgn (x, n2, sgn2) =>
3169 seek (fn (env, sgi1All as (sgi1, _)) => 3181 seek (fn (env, sgi1All as (sgi1, loc)) =>
3170 case sgi1 of 3182 case sgi1 of
3171 L'.SgiSgn (x', n1, sgn1) => 3183 L'.SgiSgn (x', n1, sgn1) =>
3172 if x = x' then 3184 if x = x' then
3173 let 3185 let
3174 val () = subSgn' counterparts env strLoc sgn1 sgn2 3186 val () = subSgn' counterparts env loc sgn1 sgn2
3175 val () = subSgn' counterparts env strLoc sgn2 sgn1 3187 val () = subSgn' counterparts env loc sgn2 sgn1
3176 3188
3177 val env = E.pushSgnNamedAs env x n2 sgn2 3189 val env = E.pushSgnNamedAs env x n2 sgn2
3178 val env = if n1 = n2 then 3190 val env = if n1 = n2 then
3179 env 3191 env
3180 else 3192 else
3186 else 3198 else
3187 NONE 3199 NONE
3188 | _ => NONE) 3200 | _ => NONE)
3189 3201
3190 | L'.SgiConstraint (c2, d2) => 3202 | L'.SgiConstraint (c2, d2) =>
3191 seek (fn (env, sgi1All as (sgi1, _)) => 3203 seek (fn (env, sgi1All as (sgi1, loc)) =>
3192 case sgi1 of 3204 case sgi1 of
3193 L'.SgiConstraint (c1, d1) => 3205 L'.SgiConstraint (c1, d1) =>
3194 if consEq env loc (c1, c2) 3206 if consEq env loc (c1, c2)
3195 andalso consEq env loc (d1, d2) then 3207 andalso consEq env loc (d1, d2) then
3196 SOME env 3208 SOME env
3197 else 3209 else
3198 NONE 3210 NONE
3199 | _ => NONE) 3211 | _ => NONE)
3200 3212
3201 | L'.SgiClassAbs (x, n2, k2) => 3213 | L'.SgiClassAbs (x, n2, k2) =>
3202 seek (fn (env, sgi1All as (sgi1, _)) => 3214 seek (fn (env, sgi1All as (sgi1, loc)) =>
3203 let 3215 let
3204 fun found (x', n1, k1, co) = 3216 fun found (x', n1, k1, co) =
3205 if x = x' then 3217 if x = x' then
3206 let 3218 let
3207 val () = unifyKinds env k1 k2 3219 val () = unifyKinds env k1 k2
3208 handle KUnify (k1, k2, err) => 3220 handle KUnify (k1, k2, err) =>
3209 sgnError env (SgiWrongKind (strLoc, sgi1All, k1, 3221 sgnError env (SgiWrongKind (loc, sgi1All, k1,
3210 sgi2All, k2, err)) 3222 sgi2All, k2, err))
3211 3223
3212 val env = E.pushCNamedAs env x n1 k1 co 3224 val env = E.pushCNamedAs env x n1 k1 co
3213 in 3225 in
3214 SOME (if n1 = n2 then 3226 SOME (if n1 = n2 then
3224 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE) 3236 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
3225 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c) 3237 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
3226 | _ => NONE 3238 | _ => NONE
3227 end) 3239 end)
3228 | L'.SgiClass (x, n2, k2, c2) => 3240 | L'.SgiClass (x, n2, k2, c2) =>
3229 seek (fn (env, sgi1All as (sgi1, _)) => 3241 seek (fn (env, sgi1All as (sgi1, loc)) =>
3230 let 3242 let
3231 fun found (x', n1, k1, c1) = 3243 fun found (x', n1, k1, c1) =
3232 if x = x' then 3244 if x = x' then
3233 let 3245 let
3234 val () = unifyKinds env k1 k2 3246 val () = unifyKinds env k1 k2
3235 handle KUnify (k1, k2, err) => 3247 handle KUnify (k1, k2, err) =>
3236 sgnError env (SgiWrongKind (strLoc, sgi1All, k1, 3248 sgnError env (SgiWrongKind (loc, sgi1All, k1,
3237 sgi2All, k2, err)) 3249 sgi2All, k2, err))
3238 3250
3239 val c2 = sub2 c2 3251 val c2 = sub2 c2
3240 3252
3241 fun good () = 3253 fun good () =
3251 end 3263 end
3252 in 3264 in
3253 (unifyCons env loc c1 c2; 3265 (unifyCons env loc c1 c2;
3254 good ()) 3266 good ())
3255 handle CUnify (c1, c2, err) => 3267 handle CUnify (c1, c2, err) =>
3256 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, 3268 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
3257 sgi2All, c2, err)); 3269 sgi2All, c2, err));
3258 good ()) 3270 good ())
3259 end 3271 end
3260 else 3272 else
3261 NONE 3273 NONE