Mercurial > urweb

comparison src/elaborate.sml @ 2109:f42fea631c1d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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