Mercurial > urweb
changeset 2109:f42fea631c1d
Improve wildification for records of type-class witnesses
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 28 Jan 2015 08:47:04 -0500 |
| parents | 1f1575eff4b9 |
| children | 9e9c915f554c |
| files | src/elaborate.sml |
| diffstat | 1 files changed, 16 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jan 22 11:26:24 2015 -0500 +++ b/src/elaborate.sml Wed Jan 28 08:47:04 2015 -0500 @@ -3697,6 +3697,21 @@ | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) + fun isClassOrFolder' env (c : L'.con) = + case #1 c of + L'.CAbs (x, k, c) => + let + val env = E.pushCRel env x k + + fun toHead (c : L'.con) = + case #1 c of + L'.CApp (c, _) => toHead c + | _ => isClassOrFolder env c + in + toHead (hnormCon env c) + end + | _ => isClassOrFolder env c + fun buildNeeded env sgis = #1 (foldl (fn ((sgi, loc), (nd, env')) => (case sgi of @@ -3715,7 +3730,7 @@ (case hnormCon env' f of (L'.CApp (f, cl), loc) => (case hnormCon env' f of - (L'.CMap _, _) => isClassOrFolder env' cl + (L'.CMap _, _) => isClassOrFolder' env' cl | _ => false) | _ => false) | (L'.CConcat (c1, c2), _) =>