Mercurial > urweb
comparison src/elaborate.sml @ 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 | 32e2752390ad |
children | 010ce27228f1 |
comparison
equal
deleted
inserted
replaced
2108:1f1575eff4b9 | 2109:f42fea631c1d |
---|---|
3695 NONE => NONE | 3695 NONE => NONE |
3696 | SOME c' => SOME (L.TRecord c', loc)) | 3696 | SOME c' => SOME (L.TRecord c', loc)) |
3697 | 3697 |
3698 | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) | 3698 | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) |
3699 | 3699 |
3700 fun isClassOrFolder' env (c : L'.con) = | |
3701 case #1 c of | |
3702 L'.CAbs (x, k, c) => | |
3703 let | |
3704 val env = E.pushCRel env x k | |
3705 | |
3706 fun toHead (c : L'.con) = | |
3707 case #1 c of | |
3708 L'.CApp (c, _) => toHead c | |
3709 | _ => isClassOrFolder env c | |
3710 in | |
3711 toHead (hnormCon env c) | |
3712 end | |
3713 | _ => isClassOrFolder env c | |
3714 | |
3700 fun buildNeeded env sgis = | 3715 fun buildNeeded env sgis = |
3701 #1 (foldl (fn ((sgi, loc), (nd, env')) => | 3716 #1 (foldl (fn ((sgi, loc), (nd, env')) => |
3702 (case sgi of | 3717 (case sgi of |
3703 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) | 3718 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) |
3704 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k) | 3719 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k) |
3713 case hnormCon env' c of | 3728 case hnormCon env' c of |
3714 (L'.CApp (f, _), _) => | 3729 (L'.CApp (f, _), _) => |
3715 (case hnormCon env' f of | 3730 (case hnormCon env' f of |
3716 (L'.CApp (f, cl), loc) => | 3731 (L'.CApp (f, cl), loc) => |
3717 (case hnormCon env' f of | 3732 (case hnormCon env' f of |
3718 (L'.CMap _, _) => isClassOrFolder env' cl | 3733 (L'.CMap _, _) => isClassOrFolder' env' cl |
3719 | _ => false) | 3734 | _ => false) |
3720 | _ => false) | 3735 | _ => false) |
3721 | (L'.CConcat (c1, c2), _) => | 3736 | (L'.CConcat (c1, c2), _) => |
3722 shouldR c1 orelse shouldR c2 | 3737 shouldR c1 orelse shouldR c2 |
3723 | c => false | 3738 | c => false |