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 ()