Mercurial > urweb
changeset 2094:0d898b086bbe
Improve wildify heuristic for finding record type-class witnesses
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 23 Dec 2014 13:42:20 -0500 |
parents | c647f113ba3e |
children | d9f918b79b5a |
files | src/elaborate.sml |
diffstat | 1 files changed, 14 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Dec 23 12:24:38 2014 -0500 +++ b/src/elaborate.sml Tue Dec 23 13:42:20 2014 -0500 @@ -3699,19 +3699,23 @@ fun should t = let val t = normClassConstraint env' t + + fun shouldR c = + case hnormCon env' c of + (L'.CApp (f, _), _) => + (case hnormCon env' f of + (L'.CApp (f, cl), loc) => + (case hnormCon env' f of + (L'.CMap _, _) => isClassOrFolder env' cl + | _ => false) + | _ => false) + | (L'.CConcat (c1, c2), _) => + shouldR c1 orelse shouldR c2 + | c => false in case #1 t of L'.CApp (f, _) => isClassOrFolder env' f - | L'.TRecord t => - (case hnormCon env' t of - (L'.CApp (f, _), _) => - (case hnormCon env' f of - (L'.CApp (f, cl), loc) => - (case hnormCon env' f of - (L'.CMap _, _) => isClassOrFolder env' cl - | _ => false) - | _ => false) - | _ => false) + | L'.TRecord t => shouldR t | _ => false end in