Mercurial > urweb

annotate src/elab_err.sml @ 2152:2d9e40e726f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adjust new [assert] to work properly from top.ur
author Adam Chlipala <adam@chlipala.net>
date Wed, 03 Jun 2015 09:55:37 -0400
parents 799be3911ce3
children
rev   line source
adam@1719 1 (* Copyright (c) 2008-2010, 2012, 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 p_kind = P.p_kind
adamc@623 40
adamc@623 41 datatype kind_error =
adamc@623 42 UnboundKind of ErrorMsg.span * string
adamc@623 43
adamc@623 44 fun kindError env err =
adamc@623 45 case err of
adamc@623 46 UnboundKind (loc, s) =>
adamc@623 47 ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
adamc@329 48
adamc@329 49 datatype kunify_error =
adamc@329 50 KOccursCheckFailed of kind * kind
adamc@329 51 | KIncompatible of kind * kind
adam@1639 52 | KScope of kind * kind
adamc@329 53
adamc@623 54 fun kunifyError env err =
adamc@329 55 case err of
adamc@329 56 KOccursCheckFailed (k1, k2) =>
adamc@329 57 eprefaces "Kind occurs check failed"
adamc@623 58 [("Kind 1", p_kind env k1),
adamc@623 59 ("Kind 2", p_kind env k2)]
adamc@329 60 | KIncompatible (k1, k2) =>
adamc@329 61 eprefaces "Incompatible kinds"
adamc@623 62 [("Kind 1", p_kind env k1),
adamc@623 63 ("Kind 2", p_kind env k2)]
adam@1639 64 | KScope (k1, k2) =>
adam@1639 65 eprefaces "Scoping prevents kind unification"
adam@1639 66 [("Kind 1", p_kind env k1),
adam@1639 67 ("Kind 2", p_kind env k2)]
adamc@329 68
adam@1714 69 fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
adamc@329 70
adamc@329 71 datatype con_error =
adamc@329 72 UnboundCon of ErrorMsg.span * string
adamc@329 73 | UnboundDatatype of ErrorMsg.span * string
adamc@329 74 | UnboundStrInCon of ErrorMsg.span * string
adam@1719 75 | WrongKind of con * kind * kind * E.env * kunify_error
adamc@329 76 | DuplicateField of ErrorMsg.span * string
adamc@329 77 | ProjBounds of con * int
adamc@329 78 | ProjMismatch of con * kind
adamc@329 79
adamc@329 80 fun conError env err =
adamc@329 81 case err of
adamc@329 82 UnboundCon (loc, s) =>
adamc@329 83 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@329 84 | UnboundDatatype (loc, s) =>
adamc@329 85 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
adamc@329 86 | UnboundStrInCon (loc, s) =>
adamc@329 87 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719 88 | WrongKind (c, k1, k2, env', kerr) =>
adamc@329 89 (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@329 90 eprefaces' [("Constructor", p_con env c),
adamc@623 91 ("Have kind", p_kind env k1),
adamc@623 92 ("Need kind", p_kind env k2)];
adam@1719 93 kunifyError env' kerr)
adamc@329 94 | DuplicateField (loc, s) =>
adamc@329 95 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@329 96 | ProjBounds (c, n) =>
adamc@329 97 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
adamc@329 98 eprefaces' [("Constructor", p_con env c),
adamc@329 99 ("Index", Print.PD.string (Int.toString n))])
adamc@329 100 | ProjMismatch (c, k) =>
adamc@329 101 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
adamc@329 102 eprefaces' [("Constructor", p_con env c),
adamc@623 103 ("Kind", p_kind env k)])
adamc@329 104
adamc@329 105 datatype cunify_error =
adam@1719 106 CKind of kind * kind * E.env * kunify_error
adamc@329 107 | COccursCheckFailed of con * con
adamc@329 108 | CIncompatible of con * con
adamc@329 109 | CExplicitness of con * con
adamc@413 110 | CKindof of kind * con * string
adam@1719 111 | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option
adam@1303 112 | TooLifty of ErrorMsg.span * ErrorMsg.span
adam@1303 113 | TooUnify of con * con
adam@1306 114 | TooDeep
adam@1639 115 | CScope of con * con
adamc@329 116
adam@1719 117 fun cunifyError env err : unit =
adamc@329 118 case err of
adam@1719 119 CKind (k1, k2, env', kerr) =>
adamc@329 120 (eprefaces "Kind unification failure"
adam@1582 121 [("Have", p_kind env k1),
adam@1582 122 ("Need", p_kind env k2)];
adam@1719 123 kunifyError env' kerr)
adamc@329 124 | COccursCheckFailed (c1, c2) =>
adamc@329 125 eprefaces "Constructor occurs check failed"
adam@1582 126 [("Have", p_con env c1),
adam@1582 127 ("Need", p_con env c2)]
adamc@329 128 | CIncompatible (c1, c2) =>
adamc@329 129 eprefaces "Incompatible constructors"
adam@1582 130 [("Have", p_con env c1),
adam@1582 131 ("Need", p_con env c2)]
adamc@329 132 | CExplicitness (c1, c2) =>
adamc@329 133 eprefaces "Differing constructor function explicitness"
adam@1582 134 [("Have", p_con env c1),
adam@1582 135 ("Need", p_con env c2)]
adamc@413 136 | CKindof (k, c, expected) =>
adamc@413 137 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
adamc@623 138 [("Kind", p_kind env k),
adamc@329 139 ("Con", p_con env c)]
adamc@1071 140 | CRecordFailure (c1, c2, fo) =>
adam@1359 141 (eprefaces "Can't unify record constructors"
adam@1582 142 (("Have", p_con env c1)
adam@1582 143 :: ("Need", p_con env c2)
adam@1359 144 :: (case fo of
adam@1359 145 NONE => []
adam@1359 146 | SOME (nm, t1, t2, _) =>
adam@1359 147 [("Field", p_con env nm),
adam@1359 148 ("Value 1", p_con env t1),
adam@1359 149 ("Value 2", p_con env t2)]));
adam@1359 150 case fo of
adam@1719 151 SOME (_, _, _, SOME (env', err')) => cunifyError env' err'
adam@1359 152 | _ => ())
adam@1303 153 | TooLifty (loc1, loc2) =>
adam@1303 154 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
adam@1303 155 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
adam@1303 156 | TooUnify (c1, c2) =>
adam@1303 157 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
adam@1303 158 eprefaces' [("Replacement", p_con env c1),
adam@1303 159 ("Body", p_con env c2)])
adam@1306 160 | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
adam@1639 161 | CScope (c1, c2) =>
adam@1639 162 eprefaces "Scoping prevents constructor unification"
adam@1639 163 [("Have", p_con env c1),
adam@1639 164 ("Need", p_con env c2)]
adamc@329 165
adamc@329 166 datatype exp_error =
adamc@329 167 UnboundExp of ErrorMsg.span * string
adamc@329 168 | UnboundStrInExp of ErrorMsg.span * string
adam@1719 169 | Unify of exp * con * con * E.env * cunify_error
adamc@339 170 | Unif of string * ErrorMsg.span * con
adamc@329 171 | WrongForm of string * exp * con
adamc@329 172 | IncompatibleCons of con * con
adamc@329 173 | DuplicatePatternVariable of ErrorMsg.span * string
adam@1719 174 | PatUnify of pat * con * con * E.env * cunify_error
adamc@329 175 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 176 | PatHasArg of ErrorMsg.span
adamc@329 177 | PatHasNoArg of ErrorMsg.span
adamc@819 178 | Inexhaustive of ErrorMsg.span * pat
adamc@329 179 | DuplicatePatField of ErrorMsg.span * string
adamc@329 180 | Unresolvable of ErrorMsg.span * con
adamc@329 181 | OutOfContext of ErrorMsg.span * (exp * con) option
adamc@329 182 | IllegalRec of string * exp
adam@2009 183 | IllegalFlex of Source.exp
adamc@329 184
adam@1714 185 val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
adam@1714 186 con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
adam@1714 187 exp = fn _ => fn e => e,
adam@1714 188 bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
adam@1714 189 | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
adam@1714 190 | (env, _) => env}
adam@1714 191
adam@1714 192 fun p_exp env e = P.p_exp env (simplExp env e)
adamc@329 193 val p_pat = P.p_pat
adamc@329 194
adamc@329 195 fun expError env err =
adamc@329 196 case err of
adamc@329 197 UnboundExp (loc, s) =>
adamc@329 198 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@329 199 | UnboundStrInExp (loc, s) =>
adamc@329 200 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719 201 | Unify (e, c1, c2, env', uerr) =>
adamc@329 202 (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@329 203 eprefaces' [("Expression", p_exp env e),
adamc@329 204 ("Have con", p_con env c1),
adamc@329 205 ("Need con", p_con env c2)];
adam@1719 206 cunifyError env' uerr)
adamc@339 207 | Unif (action, loc, c) =>
adamc@339 208 (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
adamc@329 209 eprefaces' [("Con", p_con env c)])
adamc@329 210 | WrongForm (variety, e, t) =>
adamc@329 211 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@329 212 eprefaces' [("Expression", p_exp env e),
adamc@329 213 ("Type", p_con env t)])
adamc@329 214 | IncompatibleCons (c1, c2) =>
adamc@329 215 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adam@1582 216 eprefaces' [("Have", p_con env c1),
adam@1582 217 ("Need", p_con env c2)])
adamc@329 218 | DuplicatePatternVariable (loc, s) =>
adamc@329 219 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
adam@1719 220 | PatUnify (p, c1, c2, env', uerr) =>
adamc@329 221 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
adamc@329 222 eprefaces' [("Pattern", p_pat env p),
adamc@329 223 ("Have con", p_con env c1),
adamc@329 224 ("Need con", p_con env c2)];
adam@1719 225 cunifyError env' uerr)
adamc@329 226 | UnboundConstructor (loc, ms, s) =>
adamc@329 227 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
adamc@329 228 | PatHasArg loc =>
adamc@329 229 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
adamc@329 230 | PatHasNoArg loc =>
adamc@329 231 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
adamc@819 232 | Inexhaustive (loc, p) =>
adamc@819 233 (ErrorMsg.errorAt loc "Inexhaustive 'case'";
adamc@819 234 eprefaces' [("Missed case", p_pat env p)])
adamc@329 235 | DuplicatePatField (loc, s) =>
adamc@329 236 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
adamc@329 237 | OutOfContext (loc, co) =>
adamc@329 238 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
adamc@329 239 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
adamc@329 240 ("Type", p_con env c)]) co)
adamc@329 241 | Unresolvable (loc, c) =>
adamc@329 242 (ErrorMsg.errorAt loc "Can't resolve type class instance";
adam@1742 243 eprefaces' ([("Class constraint", p_con env c)]
adam@1742 244 @ (case E.resolveFailureCause () of
adam@1742 245 NONE => []
adam@1778 246 | SOME c' => [("Reduced to unresolvable", p_con env c')]))(*;
adam@1778 247 app (fn (c, rs) => (eprefaces' [("CLASS", p_con env c)];
adam@1778 248 app (fn (c, e) => eprefaces' [("RULE", p_con env c),
adam@1778 249 ("IMPL", p_exp env e)]) rs))
adam@1778 250 (E.listClasses env)*))
adamc@329 251 | IllegalRec (x, e) =>
adamc@329 252 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
adamc@329 253 eprefaces' [("Variable", PD.string x),
adamc@329 254 ("Expression", p_exp env e)])
adam@2009 255 | IllegalFlex e =>
adam@2009 256 (ErrorMsg.errorAt (#2 e) "Flex record syntax (\"...\") only allowed in patterns";
adam@2009 257 eprefaces' [("Expression", SourcePrint.p_exp e)])
adamc@329 258
adamc@329 259
adamc@329 260 datatype decl_error =
adamc@329 261 KunifsRemain of decl list
adamc@329 262 | CunifsRemain of decl list
adamc@329 263 | Nonpositive of decl
adamc@329 264
adamc@329 265 fun lspan [] = ErrorMsg.dummySpan
adamc@329 266 | lspan ((_, loc) :: _) = loc
adamc@329 267
adam@1584 268 val baseLen = 2000
adam@1584 269
adam@1584 270 fun p_decl env d =
adam@1584 271 let
adam@1584 272 val fname = OS.FileSys.tmpName ()
adam@1584 273 val out' = TextIO.openOut fname
adam@1584 274 val out = Print.openOut {dst = out', wid = 80}
adam@1584 275
adam@1584 276 fun readFromFile () =
adam@1584 277 let
adam@1584 278 val inf = TextIO.openIn fname
adam@1584 279
adam@1584 280 fun loop acc =
adam@1584 281 case TextIO.inputLine inf of
adam@1584 282 NONE => String.concat (rev acc)
adam@1584 283 | SOME line => loop (line :: acc)
adam@1584 284 in
adam@1584 285 loop []
adam@1584 286 before TextIO.closeIn inf
adam@1584 287 end
adam@1584 288 in
adam@1584 289 Print.fprint out (P.p_decl env d);
adam@1584 290 TextIO.closeOut out';
adam@1584 291 let
adam@1584 292 val content = readFromFile ()
adam@1584 293 in
adam@1584 294 OS.FileSys.remove fname;
adam@1584 295 Print.PD.string (if size content <= baseLen then
adam@1584 296 content
adam@1584 297 else
adam@1584 298 let
adam@1584 299 val (befor, after) = Substring.position "<UNIF:" (Substring.full content)
adam@1584 300 in
adam@1584 301 if Substring.isEmpty after then
adam@1584 302 raise Fail "No unification variables in rendering"
adam@1584 303 else
adam@1584 304 Substring.concat [Substring.full "\n.....\n",
adam@1584 305 if Substring.size befor <= baseLen then
adam@1584 306 befor
adam@1584 307 else
adam@1584 308 Substring.slice (befor, Substring.size befor - baseLen, SOME baseLen),
adam@1584 309 if Substring.size after <= baseLen then
adam@1584 310 after
adam@1584 311 else
adam@1584 312 Substring.slice (after, 0, SOME baseLen),
adam@1584 313 Substring.full "\n.....\n"]
adam@1584 314 end)
adam@1584 315 end
adam@1584 316 end
adamc@329 317
adamc@329 318 fun declError env err =
adamc@329 319 case err of
adamc@329 320 KunifsRemain ds =>
adam@1521 321 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329 322 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 323 | CunifsRemain ds =>
adam@1521 324 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329 325 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 326 | Nonpositive d =>
adamc@329 327 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
adamc@329 328 eprefaces' [("Decl", p_decl env d)])
adamc@329 329
adamc@329 330 datatype sgn_error =
adamc@329 331 UnboundSgn of ErrorMsg.span * string
adamc@1000 332 | UnmatchedSgi of ErrorMsg.span * sgn_item
adam@1719 333 | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error
adam@1719 334 | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error
adamc@1000 335 | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
adam@1719 336 * (con * con * E.env * cunify_error) option
adamc@1000 337 | SgnWrongForm of ErrorMsg.span * sgn * sgn
adamc@329 338 | UnWhereable of sgn * string
adam@1719 339 | WhereWrongKind of kind * kind * E.env * kunify_error
adamc@329 340 | NotIncludable of sgn
adamc@329 341 | DuplicateCon of ErrorMsg.span * string
adamc@329 342 | DuplicateVal of ErrorMsg.span * string
adamc@329 343 | DuplicateSgn of ErrorMsg.span * string
adamc@329 344 | DuplicateStr of ErrorMsg.span * string
adamc@329 345 | NotConstraintsable of sgn
adamc@329 346
adamc@329 347 val p_sgn_item = P.p_sgn_item
adamc@329 348 val p_sgn = P.p_sgn
adamc@329 349
adamc@329 350 fun sgnError env err =
adamc@329 351 case err of
adamc@329 352 UnboundSgn (loc, s) =>
adamc@329 353 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@1000 354 | UnmatchedSgi (loc, sgi) =>
adamc@329 355 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@329 356 eprefaces' [("Item", p_sgn_item env sgi)])
adam@1719 357 | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) =>
adamc@1000 358 (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
adamc@329 359 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 360 ("Need", p_sgn_item env sgi2),
adamc@623 361 ("Kind 1", p_kind env k1),
adamc@623 362 ("Kind 2", p_kind env k2)];
adam@1719 363 kunifyError env' kerr)
adam@1719 364 | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) =>
adamc@1000 365 (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
adamc@329 366 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 367 ("Need", p_sgn_item env sgi2),
adamc@329 368 ("Con 1", p_con env c1),
adamc@329 369 ("Con 2", p_con env c2)];
adam@1719 370 cunifyError env' cerr)
adamc@1000 371 | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
adamc@1000 372 (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
adamc@329 373 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 374 ("Need", p_sgn_item env sgi2)];
adam@1719 375 Option.app (fn (c1, c2, env', ue) =>
adamc@329 376 (eprefaces "Unification error"
adam@1719 377 [("Con 1", p_con env' c1),
adam@1719 378 ("Con 2", p_con env' c2)];
adam@1719 379 cunifyError env' ue)) cerro)
adamc@1000 380 | SgnWrongForm (loc, sgn1, sgn2) =>
adamc@1000 381 (ErrorMsg.errorAt loc "Incompatible signatures:";
adamc@329 382 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@329 383 ("Sig 2", p_sgn env sgn2)])
adamc@329 384 | UnWhereable (sgn, x) =>
adamc@329 385 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@329 386 eprefaces' [("Signature", p_sgn env sgn),
adamc@329 387 ("Field", PD.string x)])
adam@1719 388 | WhereWrongKind (k1, k2, env', kerr) =>
adamc@329 389 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@623 390 eprefaces' [("Have", p_kind env k1),
adamc@623 391 ("Need", p_kind env k2)];
adam@1719 392 kunifyError env' kerr)
adamc@329 393 | NotIncludable sgn =>
adamc@329 394 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@329 395 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 396 | DuplicateCon (loc, s) =>
adamc@329 397 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@329 398 | DuplicateVal (loc, s) =>
adamc@329 399 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@329 400 | DuplicateSgn (loc, s) =>
adamc@329 401 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@329 402 | DuplicateStr (loc, s) =>
adamc@329 403 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@329 404 | NotConstraintsable sgn =>
adamc@329 405 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@329 406 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 407
adamc@329 408 datatype str_error =
adamc@329 409 UnboundStr of ErrorMsg.span * string
adamc@329 410 | NotFunctor of sgn
adamc@329 411 | FunctorRebind of ErrorMsg.span
adamc@329 412 | UnOpenable of sgn
adam@1719 413 | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error)
adamc@329 414 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 415 | NotDatatype of ErrorMsg.span
adamc@329 416
adamc@329 417 fun strError env err =
adamc@329 418 case err of
adamc@329 419 UnboundStr (loc, s) =>
adamc@329 420 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@329 421 | NotFunctor sgn =>
adamc@329 422 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@329 423 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 424 | FunctorRebind loc =>
adamc@329 425 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@329 426 | UnOpenable sgn =>
adamc@329 427 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@329 428 eprefaces' [("Signature", p_sgn env sgn)])
adam@1719 429 | NotType (loc, k, (k1, k2, env', ue)) =>
adamc@706 430 (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
adamc@623 431 eprefaces' [("Kind", p_kind env k),
adamc@623 432 ("Subkind 1", p_kind env k1),
adamc@623 433 ("Subkind 2", p_kind env k2)];
adam@1719 434 kunifyError env' ue)
adamc@329 435 | DuplicateConstructor (x, loc) =>
adamc@329 436 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@329 437 | NotDatatype loc =>
adamc@329 438 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@329 439
adamc@329 440 end