I am trying to implement total parsers with Idris, based on this paper. First I tried to implement the more basic recogniser type P
:
Tok : Type
Tok = Char
mutual
data P : Bool -> Type where
fail : P False
empty : P True
sat : (Tok -> Bool) -> P False
(<|>) : P n -> P m -> P (n || m)
(.) : LazyP m n -> LazyP n m -> P (n && m)
nonempty : P n -> P False
cast : (n = m) -> P n -> P m
LazyP : Bool -> Bool -> Type
LazyP False n = Lazy (P n)
LazyP True n = P n
DelayP : P n -> LazyP b n
DelayP {b = False} x = Delay x
DelayP {b = True } x = x
ForceP : LazyP b n -> P n
ForceP {b = False} x = Force x
ForceP {b = True } x = x
Forced : LazyP b n -> Bool
Forced {b = b} _ = b
This works fine, but I cannot work out how to define the first example from the paper. In Agda it is:
left-right : P false
left-right = ♯ left-right . ♯ left-right
But I cannot get this to work in Idris:
lr : P False
lr = (Delay lr . Delay lr)
produces
Can't unify
Lazy' t (P False)
with
LazyP n m
It will typecheck if you give it some help, like this:
lr : P False
lr = (the (LazyP False False) (Delay lr)) . (the (LazyP False False) (Delay lr))
But this is rejected by the totality checker, as are other variants like
lr : P False
lr = Delay (the (LazyP True False) lr) . (the (LazyP False False) (Delay lr))
It doesn't help that I'm not entirely sure how the ♯
operator binds in Agda.
Can anyone see a way to get define the left-right recogniser in Idris? Is my definition of P
wrong, or my attempt at translating the function? Or is Idris's totality checker just not quite up to this coinductive stuff?
Currently trying to port this library myself, it seems like Agda infers different implicits to Idris. These are the missing implicits:
%default total
mutual
data P : Bool -> Type where
Fail : P False
Empty : P True
Tok : Char -> P False
(<|>) : P n -> P m -> P (n || m)
(.) : {n,m: Bool} -> LazyP m n -> LazyP n m -> P (n && m)
LazyP : Bool -> Bool -> Type
LazyP False n = Inf (P n)
LazyP True n = P n
lr : P False
lr = (.) {n=False} {m=False} (Delay lr) (Delay lr)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With