Mercurial > urweb
diff src/elab_err.sml @ 1714:d6c45026240d
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 |
line wrap: on
line diff
--- a/src/elab_err.sml Mon Apr 16 09:07:28 2012 -0400 +++ b/src/elab_err.sml Mon Apr 16 09:46:42 2012 -0400 @@ -36,20 +36,6 @@ open Print structure P = ElabPrint -val simplCon = U.Con.mapB {kind = fn _ => fn k => k, - con = fn env => fn c => - let - val c = (c, ErrorMsg.dummySpan) - val c' = ElabOps.hnormCon env c - in - (*prefaces "simpl" [("c", P.p_con env c), - ("c'", P.p_con env c')];*) - #1 c' - end, - bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k - | (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co - | (env, _) => env} - val p_kind = P.p_kind datatype kind_error = @@ -80,7 +66,7 @@ [("Kind 1", p_kind env k1), ("Kind 2", p_kind env k2)] -fun p_con env c = P.p_con env (simplCon env c) +fun p_con env c = P.p_con env (ElabOps.reduceCon env c) datatype con_error = UnboundCon of ErrorMsg.span * string @@ -195,7 +181,14 @@ | OutOfContext of ErrorMsg.span * (exp * con) option | IllegalRec of string * exp -val p_exp = P.p_exp +val simplExp = U.Exp.mapB {kind = fn _ => fn k => k, + con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)), + exp = fn _ => fn e => e, + bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k + | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co + | (env, _) => env} + +fun p_exp env e = P.p_exp env (simplExp env e) val p_pat = P.p_pat fun expError env err =