Hi,
I've been staring at this takewhile.epi (in examples/) for some time and
while epigram turns it green I remain mostly yellow about it.
If I am correct it is supposed to demostrate that one can have more than
one index on a datatype (also that we can establish invariants not just
preserve them)
------------------------------------------------------------------------------
( as : List A ! ( as : List
A !
! !
! !
! P : all a : A => * ! ! p : Prefix as asbs ; q : ListAll P
as !
data !--------------------! where
!----------------------------------------!
! Takewhile as P : * ) ! tw as p q : Takewhile asbs
P )
------------------------------------------------------------------------------
ie takewhile can have a much more informative type than it has in
Haskell: the predicate P holds for all elements of the prefix. The
definition of Prefix however is puzzling:
------------------------------------------------------------------------------
( as, asbs : List
A !
( as, asbs !
! !
! : List A ! ! p : Prefix as asbs ; a
: A !
data !-----------! where (--------------! ;
!-----------------------------!
! Prefix ! ! pnil : ! ! pcons p a
: !
! % as asbs ! ! Prefix nil ! ! Prefix (cons a
as) !
! : * ) ! % bs ) ! % (cons a
asbs) )
------------------------------------------------------------------------------
What is bs doing in the pnil case? nil is a prefix of any list? I
changed it to 'as' just to see what happens and everything remained green!
------------------------------------------------------------------------------
( as : List A ; d : Dec (P a) ; r : Takewhile as P
!
let
!----------------------------------------------------!
! takewhileaux as d r : Takewhile (cons a as) P
)
takewhileaux as d r <= case
r
{ takewhileaux asbs d (tw as p q) <= case
d
{ takewhileaux asbs (yes a) (tw as p q) => tw ? (pcons p ?)
(lcons a q)
takewhileaux asbs (no f) (tw as p q) => tw nil pnil
lnil
}
}
------------------------------------------------------------------------------
The confusion arose when I tried to fill in the question marks in the
definition of takewhileaux. VFL says you can use ? if Epigram can figure
out what goes there...but I couldn't!
Tried
1. (pcons p a) from the typing of (pcons): it's yellow.
2. pnil (wrong but it seemed to be worth trying) : yellow
... and a few more possiblities
and I concluded that ?s should not remain after elaboration! Is there
any way of convincing epigram to spit back the term it found appropriate
instead of the ?? And could I please have an example which demonstrates
it works: inspect takewhile ?????.
Thanks, Laszlo
