Mercurial > urweb

comparison src/elab_err.sml @ 1714:d6c45026240d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Do a lot more type simplification for error messages
author Adam Chlipala <adam@chlipala.net>
date Mon, 16 Apr 2012 09:46:42 -0400
parents 6c00d8af6239
children 0bafdfae2ac7
comparison
equal deleted inserted replaced
1713:1b3f82b09bb0 1714:d6c45026240d
34 structure U = ElabUtil 34 structure U = ElabUtil
35 35
36 open Print 36 open Print
37 structure P = ElabPrint 37 structure P = ElabPrint
38 38
39 val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
40 con = fn env => fn c =>
41 let
42 val c = (c, ErrorMsg.dummySpan)
43 val c' = ElabOps.hnormCon env c
44 in
45 (*prefaces "simpl" [("c", P.p_con env c),
46 ("c'", P.p_con env c')];*)
47 #1 c'
48 end,
49 bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
50 | (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
51 | (env, _) => env}
52
53 val p_kind = P.p_kind 39 val p_kind = P.p_kind
54 40
55 datatype kind_error = 41 datatype kind_error =
56 UnboundKind of ErrorMsg.span * string 42 UnboundKind of ErrorMsg.span * string
57 43
78 | KScope (k1, k2) => 64 | KScope (k1, k2) =>
79 eprefaces "Scoping prevents kind unification" 65 eprefaces "Scoping prevents kind unification"
80 [("Kind 1", p_kind env k1), 66 [("Kind 1", p_kind env k1),
81 ("Kind 2", p_kind env k2)] 67 ("Kind 2", p_kind env k2)]
82 68
83 fun p_con env c = P.p_con env (simplCon env c) 69 fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
84 70
85 datatype con_error = 71 datatype con_error =
86 UnboundCon of ErrorMsg.span * string 72 UnboundCon of ErrorMsg.span * string
87 | UnboundDatatype of ErrorMsg.span * string 73 | UnboundDatatype of ErrorMsg.span * string
88 | UnboundStrInCon of ErrorMsg.span * string 74 | UnboundStrInCon of ErrorMsg.span * string
193 | DuplicatePatField of ErrorMsg.span * string 179 | DuplicatePatField of ErrorMsg.span * string
194 | Unresolvable of ErrorMsg.span * con 180 | Unresolvable of ErrorMsg.span * con
195 | OutOfContext of ErrorMsg.span * (exp * con) option 181 | OutOfContext of ErrorMsg.span * (exp * con) option
196 | IllegalRec of string * exp 182 | IllegalRec of string * exp
197 183
198 val p_exp = P.p_exp 184 val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
185 con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
186 exp = fn _ => fn e => e,
187 bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
188 | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
189 | (env, _) => env}
190
191 fun p_exp env e = P.p_exp env (simplExp env e)
199 val p_pat = P.p_pat 192 val p_pat = P.p_pat
200 193
201 fun expError env err = 194 fun expError env err =
202 case err of 195 case err of
203 UnboundExp (loc, s) => 196 UnboundExp (loc, s) =>