Mercurial > urweb
comparison src/elab_util.sml @ 1795:d28adceef22a
Allow type class instances with hypotheses via local ('let') definitions
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 25 Jul 2012 14:04:59 -0400 |
parents | 4a03aa3251cb |
children | bb942416bf1c |
comparison
equal
deleted
inserted
replaced
1794:4671afac15af | 1795:d28adceef22a |
---|---|
565 fun mapfold {kind = fk, con = fc, exp = fe} = | 565 fun mapfold {kind = fk, con = fc, exp = fe} = |
566 mapfoldB {kind = fn () => fk, | 566 mapfoldB {kind = fn () => fk, |
567 con = fn () => fc, | 567 con = fn () => fc, |
568 exp = fn () => fe, | 568 exp = fn () => fe, |
569 bind = fn ((), _) => ()} () | 569 bind = fn ((), _) => ()} () |
570 | |
571 fun existsB {kind, con, exp, bind} ctx e = | |
572 case mapfoldB {kind = fn ctx => fn k => fn () => | |
573 if kind (ctx, k) then | |
574 S.Return () | |
575 else | |
576 S.Continue (k, ()), | |
577 con = fn ctx => fn c => fn () => | |
578 if con (ctx, c) then | |
579 S.Return () | |
580 else | |
581 S.Continue (c, ()), | |
582 exp = fn ctx => fn e => fn () => | |
583 if exp (ctx, e) then | |
584 S.Return () | |
585 else | |
586 S.Continue (e, ()), | |
587 bind = bind} ctx e () of | |
588 S.Return _ => true | |
589 | S.Continue _ => false | |
570 | 590 |
571 fun exists {kind, con, exp} k = | 591 fun exists {kind, con, exp} k = |
572 case mapfold {kind = fn k => fn () => | 592 case mapfold {kind = fn k => fn () => |
573 if kind k then | 593 if kind k then |
574 S.Return () | 594 S.Return () |