Mercurial > urweb

annotate src/elab_err.sml @ 428:3ca00463de20

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make *_w function prototypes match header file
author adamc@hnf.impredicative.com
date Fri, 24 Oct 2008 19:59:17 -0400
parents 6a0e54400805
children 588b9d16b00a
rev   line source
adamc@329 1 (* Copyright (c) 2008, Adam Chlipala
adamc@329 2 * All rights reserved.
adamc@329 3 *
adamc@329 4 * Redistribution and use in source and binary forms, with or without
adamc@329 5 * modification, are permitted provided that the following conditions are met:
adamc@329 6 *
adamc@329 7 * - Redistributions of source code must retain the above copyright notice,
adamc@329 8 * this list of conditions and the following disclaimer.
adamc@329 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@329 10 * this list of conditions and the following disclaimer in the documentation
adamc@329 11 * and/or other materials provided with the distribution.
adamc@329 12 * - The names of contributors may not be used to endorse or promote products
adamc@329 13 * derived from this software without specific prior written permission.
adamc@329 14 *
adamc@329 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@329 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@329 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@329 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@329 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@329 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@329 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@329 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@329 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@329 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@329 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@329 26 *)
adamc@329 27
adamc@329 28 structure ElabErr :> ELAB_ERR = struct
adamc@329 29
adamc@329 30 structure L = Source
adamc@329 31 open Elab
adamc@329 32
adamc@329 33 structure E = ElabEnv
adamc@329 34 structure U = ElabUtil
adamc@329 35
adamc@329 36 open Print
adamc@329 37 structure P = ElabPrint
adamc@329 38
adamc@329 39 val simplCon = U.Con.mapB {kind = fn k => k,
adamc@329 40 con = fn env => fn c =>
adamc@329 41 let
adamc@329 42 val c = (c, ErrorMsg.dummySpan)
adamc@329 43 val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c
adamc@329 44 in
adamc@329 45 (*prefaces "simpl" [("c", P.p_con env c),
adamc@329 46 ("c'", P.p_con env c')];*)
adamc@329 47 #1 c'
adamc@329 48 end,
adamc@329 49 bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
adamc@329 50 | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
adamc@329 51
adamc@329 52 val p_kind = P.p_kind
adamc@329 53
adamc@329 54 datatype kunify_error =
adamc@329 55 KOccursCheckFailed of kind * kind
adamc@329 56 | KIncompatible of kind * kind
adamc@329 57
adamc@329 58 fun kunifyError err =
adamc@329 59 case err of
adamc@329 60 KOccursCheckFailed (k1, k2) =>
adamc@329 61 eprefaces "Kind occurs check failed"
adamc@329 62 [("Kind 1", p_kind k1),
adamc@329 63 ("Kind 2", p_kind k2)]
adamc@329 64 | KIncompatible (k1, k2) =>
adamc@329 65 eprefaces "Incompatible kinds"
adamc@329 66 [("Kind 1", p_kind k1),
adamc@329 67 ("Kind 2", p_kind k2)]
adamc@329 68
adamc@329 69
adamc@329 70 fun p_con env c = P.p_con env (simplCon env c)
adamc@329 71
adamc@329 72 datatype con_error =
adamc@329 73 UnboundCon of ErrorMsg.span * string
adamc@329 74 | UnboundDatatype of ErrorMsg.span * string
adamc@329 75 | UnboundStrInCon of ErrorMsg.span * string
adamc@329 76 | WrongKind of con * kind * kind * kunify_error
adamc@329 77 | DuplicateField of ErrorMsg.span * string
adamc@329 78 | ProjBounds of con * int
adamc@329 79 | ProjMismatch of con * kind
adamc@329 80
adamc@329 81 fun conError env err =
adamc@329 82 case err of
adamc@329 83 UnboundCon (loc, s) =>
adamc@329 84 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@329 85 | UnboundDatatype (loc, s) =>
adamc@329 86 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
adamc@329 87 | UnboundStrInCon (loc, s) =>
adamc@329 88 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@329 89 | WrongKind (c, k1, k2, kerr) =>
adamc@329 90 (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@329 91 eprefaces' [("Constructor", p_con env c),
adamc@329 92 ("Have kind", p_kind k1),
adamc@329 93 ("Need kind", p_kind k2)];
adamc@329 94 kunifyError kerr)
adamc@329 95 | DuplicateField (loc, s) =>
adamc@329 96 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@329 97 | ProjBounds (c, n) =>
adamc@329 98 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
adamc@329 99 eprefaces' [("Constructor", p_con env c),
adamc@329 100 ("Index", Print.PD.string (Int.toString n))])
adamc@329 101 | ProjMismatch (c, k) =>
adamc@329 102 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
adamc@329 103 eprefaces' [("Constructor", p_con env c),
adamc@329 104 ("Kind", p_kind k)])
adamc@329 105
adamc@329 106
adamc@329 107 datatype cunify_error =
adamc@329 108 CKind of kind * kind * kunify_error
adamc@329 109 | COccursCheckFailed of con * con
adamc@329 110 | CIncompatible of con * con
adamc@329 111 | CExplicitness of con * con
adamc@413 112 | CKindof of kind * con * string
adamc@329 113 | CRecordFailure of con * con
adamc@329 114
adamc@329 115 fun cunifyError env err =
adamc@329 116 case err of
adamc@329 117 CKind (k1, k2, kerr) =>
adamc@329 118 (eprefaces "Kind unification failure"
adamc@329 119 [("Kind 1", p_kind k1),
adamc@329 120 ("Kind 2", p_kind k2)];
adamc@329 121 kunifyError kerr)
adamc@329 122 | COccursCheckFailed (c1, c2) =>
adamc@329 123 eprefaces "Constructor occurs check failed"
adamc@329 124 [("Con 1", p_con env c1),
adamc@329 125 ("Con 2", p_con env c2)]
adamc@329 126 | CIncompatible (c1, c2) =>
adamc@329 127 eprefaces "Incompatible constructors"
adamc@329 128 [("Con 1", p_con env c1),
adamc@329 129 ("Con 2", p_con env c2)]
adamc@329 130 | CExplicitness (c1, c2) =>
adamc@329 131 eprefaces "Differing constructor function explicitness"
adamc@329 132 [("Con 1", p_con env c1),
adamc@329 133 ("Con 2", p_con env c2)]
adamc@413 134 | CKindof (k, c, expected) =>
adamc@413 135 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
adamc@329 136 [("Kind", p_kind k),
adamc@329 137 ("Con", p_con env c)]
adamc@329 138 | CRecordFailure (c1, c2) =>
adamc@329 139 eprefaces "Can't unify record constructors"
adamc@329 140 [("Summary 1", p_con env c1),
adamc@329 141 ("Summary 2", p_con env c2)]
adamc@329 142
adamc@329 143 datatype exp_error =
adamc@329 144 UnboundExp of ErrorMsg.span * string
adamc@329 145 | UnboundStrInExp of ErrorMsg.span * string
adamc@329 146 | Unify of exp * con * con * cunify_error
adamc@339 147 | Unif of string * ErrorMsg.span * con
adamc@329 148 | WrongForm of string * exp * con
adamc@329 149 | IncompatibleCons of con * con
adamc@329 150 | DuplicatePatternVariable of ErrorMsg.span * string
adamc@329 151 | PatUnify of pat * con * con * cunify_error
adamc@329 152 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 153 | PatHasArg of ErrorMsg.span
adamc@329 154 | PatHasNoArg of ErrorMsg.span
adamc@329 155 | Inexhaustive of ErrorMsg.span
adamc@329 156 | DuplicatePatField of ErrorMsg.span * string
adamc@329 157 | Unresolvable of ErrorMsg.span * con
adamc@329 158 | OutOfContext of ErrorMsg.span * (exp * con) option
adamc@329 159 | IllegalRec of string * exp
adamc@329 160
adamc@329 161 val p_exp = P.p_exp
adamc@329 162 val p_pat = P.p_pat
adamc@329 163
adamc@329 164 fun expError env err =
adamc@329 165 case err of
adamc@329 166 UnboundExp (loc, s) =>
adamc@329 167 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@329 168 | UnboundStrInExp (loc, s) =>
adamc@329 169 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@329 170 | Unify (e, c1, c2, uerr) =>
adamc@329 171 (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@329 172 eprefaces' [("Expression", p_exp env e),
adamc@329 173 ("Have con", p_con env c1),
adamc@329 174 ("Need con", p_con env c2)];
adamc@329 175 cunifyError env uerr)
adamc@339 176 | Unif (action, loc, c) =>
adamc@339 177 (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
adamc@329 178 eprefaces' [("Con", p_con env c)])
adamc@329 179 | WrongForm (variety, e, t) =>
adamc@329 180 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@329 181 eprefaces' [("Expression", p_exp env e),
adamc@329 182 ("Type", p_con env t)])
adamc@329 183 | IncompatibleCons (c1, c2) =>
adamc@329 184 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adamc@329 185 eprefaces' [("Con 1", p_con env c1),
adamc@329 186 ("Con 2", p_con env c2)])
adamc@329 187 | DuplicatePatternVariable (loc, s) =>
adamc@329 188 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
adamc@329 189 | PatUnify (p, c1, c2, uerr) =>
adamc@329 190 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
adamc@329 191 eprefaces' [("Pattern", p_pat env p),
adamc@329 192 ("Have con", p_con env c1),
adamc@329 193 ("Need con", p_con env c2)];
adamc@329 194 cunifyError env uerr)
adamc@329 195 | UnboundConstructor (loc, ms, s) =>
adamc@329 196 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
adamc@329 197 | PatHasArg loc =>
adamc@329 198 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
adamc@329 199 | PatHasNoArg loc =>
adamc@329 200 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
adamc@329 201 | Inexhaustive loc =>
adamc@329 202 ErrorMsg.errorAt loc "Inexhaustive 'case'"
adamc@329 203 | DuplicatePatField (loc, s) =>
adamc@329 204 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
adamc@329 205 | OutOfContext (loc, co) =>
adamc@329 206 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
adamc@329 207 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
adamc@329 208 ("Type", p_con env c)]) co)
adamc@329 209 | Unresolvable (loc, c) =>
adamc@329 210 (ErrorMsg.errorAt loc "Can't resolve type class instance";
adamc@329 211 eprefaces' [("Class constraint", p_con env c)])
adamc@329 212 | IllegalRec (x, e) =>
adamc@329 213 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
adamc@329 214 eprefaces' [("Variable", PD.string x),
adamc@329 215 ("Expression", p_exp env e)])
adamc@329 216
adamc@329 217
adamc@329 218 datatype decl_error =
adamc@329 219 KunifsRemain of decl list
adamc@329 220 | CunifsRemain of decl list
adamc@329 221 | Nonpositive of decl
adamc@329 222
adamc@329 223 fun lspan [] = ErrorMsg.dummySpan
adamc@329 224 | lspan ((_, loc) :: _) = loc
adamc@329 225
adamc@329 226 val p_decl = P.p_decl
adamc@329 227
adamc@329 228 fun declError env err =
adamc@329 229 case err of
adamc@329 230 KunifsRemain ds =>
adamc@329 231 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
adamc@329 232 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 233 | CunifsRemain ds =>
adamc@329 234 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
adamc@329 235 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 236 | Nonpositive d =>
adamc@329 237 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
adamc@329 238 eprefaces' [("Decl", p_decl env d)])
adamc@329 239
adamc@329 240 datatype sgn_error =
adamc@329 241 UnboundSgn of ErrorMsg.span * string
adamc@329 242 | UnmatchedSgi of sgn_item
adamc@329 243 | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
adamc@329 244 | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
adamc@329 245 | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
adamc@329 246 | SgnWrongForm of sgn * sgn
adamc@329 247 | UnWhereable of sgn * string
adamc@329 248 | WhereWrongKind of kind * kind * kunify_error
adamc@329 249 | NotIncludable of sgn
adamc@329 250 | DuplicateCon of ErrorMsg.span * string
adamc@329 251 | DuplicateVal of ErrorMsg.span * string
adamc@329 252 | DuplicateSgn of ErrorMsg.span * string
adamc@329 253 | DuplicateStr of ErrorMsg.span * string
adamc@329 254 | NotConstraintsable of sgn
adamc@329 255
adamc@329 256 val p_sgn_item = P.p_sgn_item
adamc@329 257 val p_sgn = P.p_sgn
adamc@329 258
adamc@329 259 fun sgnError env err =
adamc@329 260 case err of
adamc@329 261 UnboundSgn (loc, s) =>
adamc@329 262 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@329 263 | UnmatchedSgi (sgi as (_, loc)) =>
adamc@329 264 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@329 265 eprefaces' [("Item", p_sgn_item env sgi)])
adamc@329 266 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
adamc@329 267 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
adamc@329 268 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 269 ("Need", p_sgn_item env sgi2),
adamc@329 270 ("Kind 1", p_kind k1),
adamc@329 271 ("Kind 2", p_kind k2)];
adamc@329 272 kunifyError kerr)
adamc@329 273 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
adamc@329 274 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
adamc@329 275 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 276 ("Need", p_sgn_item env sgi2),
adamc@329 277 ("Con 1", p_con env c1),
adamc@329 278 ("Con 2", p_con env c2)];
adamc@329 279 cunifyError env cerr)
adamc@329 280 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
adamc@329 281 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
adamc@329 282 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 283 ("Need", p_sgn_item env sgi2)];
adamc@329 284 Option.app (fn (c1, c2, ue) =>
adamc@329 285 (eprefaces "Unification error"
adamc@329 286 [("Con 1", p_con env c1),
adamc@329 287 ("Con 2", p_con env c2)];
adamc@329 288 cunifyError env ue)) cerro)
adamc@329 289 | SgnWrongForm (sgn1, sgn2) =>
adamc@329 290 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
adamc@329 291 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@329 292 ("Sig 2", p_sgn env sgn2)])
adamc@329 293 | UnWhereable (sgn, x) =>
adamc@329 294 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@329 295 eprefaces' [("Signature", p_sgn env sgn),
adamc@329 296 ("Field", PD.string x)])
adamc@329 297 | WhereWrongKind (k1, k2, kerr) =>
adamc@329 298 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@329 299 eprefaces' [("Have", p_kind k1),
adamc@329 300 ("Need", p_kind k2)];
adamc@329 301 kunifyError kerr)
adamc@329 302 | NotIncludable sgn =>
adamc@329 303 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@329 304 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 305 | DuplicateCon (loc, s) =>
adamc@329 306 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@329 307 | DuplicateVal (loc, s) =>
adamc@329 308 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@329 309 | DuplicateSgn (loc, s) =>
adamc@329 310 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@329 311 | DuplicateStr (loc, s) =>
adamc@329 312 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@329 313 | NotConstraintsable sgn =>
adamc@329 314 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@329 315 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 316
adamc@329 317 datatype str_error =
adamc@329 318 UnboundStr of ErrorMsg.span * string
adamc@329 319 | NotFunctor of sgn
adamc@329 320 | FunctorRebind of ErrorMsg.span
adamc@329 321 | UnOpenable of sgn
adamc@329 322 | NotType of kind * (kind * kind * kunify_error)
adamc@329 323 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 324 | NotDatatype of ErrorMsg.span
adamc@329 325
adamc@329 326 fun strError env err =
adamc@329 327 case err of
adamc@329 328 UnboundStr (loc, s) =>
adamc@329 329 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@329 330 | NotFunctor sgn =>
adamc@329 331 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@329 332 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 333 | FunctorRebind loc =>
adamc@329 334 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@329 335 | UnOpenable sgn =>
adamc@329 336 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@329 337 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 338 | NotType (k, (k1, k2, ue)) =>
adamc@329 339 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
adamc@329 340 eprefaces' [("Kind", p_kind k),
adamc@329 341 ("Subkind 1", p_kind k1),
adamc@329 342 ("Subkind 2", p_kind k2)];
adamc@329 343 kunifyError ue)
adamc@329 344 | DuplicateConstructor (x, loc) =>
adamc@329 345 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@329 346 | NotDatatype loc =>
adamc@329 347 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@329 348
adamc@329 349 end