Mercurial > urweb
changeset 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 | 1b3f82b09bb0 |
| children | 1584fd8d16dd |
| files | src/elab_err.sml src/elab_ops.sig src/elab_ops.sml tests/league.ur |
| diffstat | 4 files changed, 192 insertions(+), 16 deletions(-) [+] |
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 =
--- a/src/elab_ops.sig Mon Apr 16 09:07:28 2012 -0400 +++ b/src/elab_ops.sig Mon Apr 16 09:46:42 2012 -0400 @@ -40,6 +40,7 @@ val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn val hnormCon : ElabEnv.env -> Elab.con -> Elab.con + val reduceCon : ElabEnv.env -> Elab.con -> Elab.con val identity : int ref val distribute : int ref
--- a/src/elab_ops.sml Mon Apr 16 09:07:28 2012 -0400 +++ b/src/elab_ops.sml Mon Apr 16 09:46:42 2012 -0400 @@ -324,4 +324,179 @@ | _ => cAll +fun reduceCon env (cAll as (c, loc)) = + case c of + TFun (c1, c2) => (TFun (reduceCon env c1, reduceCon env c2), loc) + | TCFun (exp, x, k, c) => (TCFun (exp, x, k, reduceCon env c), loc) + | TRecord c => (TRecord (reduceCon env c), loc) + | TDisjoint (c1, c2, c3) => (TDisjoint (reduceCon env c1, reduceCon env c2, reduceCon env c3), loc) + + | CRel _ => cAll + | CNamed xn => + (case E.lookupCNamed env xn of + (_, _, SOME c') => reduceCon env c' + | _ => cAll) + | CModProj _ => cAll + | CApp (c1, c2) => + let + val c1 = reduceCon env c1 + val c2 = reduceCon env c2 + fun default () = (CApp (c1, c2), loc) + in + case #1 c1 of + CAbs (x, k, cb) => + ((reduceCon env (subConInCon (0, c2) cb)) + handle SynUnif => default ()) + | CApp (c', f) => + let + val c' = reduceCon env c' + val f = reduceCon env f + in + case #1 c' of + CMap (ks as (k1, k2)) => + (case #1 c2 of + CRecord (_, []) => (CRecord (k2, []), loc) + | CRecord (_, (x, c) :: rest) => + reduceCon env + (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc) + | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => + let + val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) + in + reduceCon env + (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, rest''), loc)), loc) + end + | _ => + let + fun unconstraint c = + case reduceCon env c of + (TDisjoint (_, _, c), _) => unconstraint c + | c => c + + fun inc r = r := !r + 1 + + fun tryDistributivity () = + case reduceCon env c2 of + (CConcat (c1, c2), _) => + let + val c = (CMap ks, loc) + val c = (CApp (c, f), loc) + + val c1 = (CApp (c, c1), loc) + val c2 = (CApp (c, c2), loc) + val c = (CConcat (c1, c2), loc) + in + inc distribute; + reduceCon env c + end + | _ => default () + + fun tryFusion () = + case #1 (reduceCon env c2) of + CApp (f', r') => + (case #1 (reduceCon env f') of + CApp (f', inner_f) => + (case #1 (reduceCon env f') of + CMap (dom, _) => + let + val inner_f = liftConInCon 0 inner_f + val f = liftConInCon 0 f + + val f' = (CApp (inner_f, (CRel 0, loc)), loc) + val f' = (CApp (f, f'), loc) + val f' = (CAbs ("v", dom, f'), loc) + + val c = (CMap (dom, k2), loc) + val c = (CApp (c, f'), loc) + val c = (CApp (c, r'), loc) + in + inc fuse; + reduceCon env c + end + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity () + + fun tryIdentity () = + let + fun cunif () = + let + val r = ref (Unknown (fn _ => true)) + in + (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) + end + + val (vR, v) = cunif () + + val c = (CApp (f, v), loc) + in + case unconstraint c of + (CUnif (_, _, _, _, vR'), _) => + if vR' = vR then + (inc identity; + reduceCon env c2) + else + tryFusion () + | _ => tryFusion () + end + in + tryIdentity () + end) + | _ => default () + end + | _ => default () + end + | CAbs (x, k, b) => + let + val b = reduceCon (E.pushCRel env x k) b + fun default () = (CAbs (x, k, b), loc) + in + case #1 b of + CApp (f, (CRel 0, _)) => + if occurs f then + default () + else + reduceCon env (subConInCon (0, (CUnit, loc)) f) + | _ => default () + end + + | CKAbs (x, b) => (CKAbs (x, reduceCon (E.pushKRel env x) b), loc) + | CKApp (c1, k) => + (case reduceCon env c1 of + (CKAbs (_, body), _) => reduceCon env (subKindInCon (0, k) body) + | c1 => (CKApp (c1, k), loc)) + | TKFun (x, c) => (TKFun (x, reduceCon env c), loc) + + | CName _ => cAll + + | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (reduceCon env x, reduceCon env c)) xcs), loc) + | CConcat (c1, c2) => + let + val c1 = reduceCon env c1 + val c2 = reduceCon env c2 + in + case (c1, c2) of + ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => (CRecord (k, xcs1 @ xcs2), loc) + | ((CRecord (_, []), _), _) => c2 + | ((CConcat (c11, c12), loc), _) => reduceCon env (CConcat (c11, (CConcat (c12, c2), loc)), loc) + | (_, (CRecord (_, []), _)) => c1 + | _ => (CConcat (c1, c2), loc) + end + | CMap _ => cAll + + | CUnit => cAll + + | CTuple cs => (CTuple (map (reduceCon env) cs), loc) + | CProj (c, n) => + (case reduceCon env c of + (CTuple cs, _) => reduceCon env (List.nth (cs, n - 1)) + | c => (CProj (c, n), loc)) + + | CError => cAll + + | CUnif (nl, _, _, _, ref (Known c)) => reduceCon env (E.mliftConInCon nl c) + | CUnif _ => cAll + end