Implementing paper-based total parsers in Idris in Agde

Question

I am trying to implement common parsers with Idris based on this article . At first I tried to implement a more basic type of recognizer 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 mn -> LazyP nm -> 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 bn DelayP {b = False} x = Delay x DelayP {b = True } x = x ForceP : LazyP bn -> P n ForceP {b = False} x = Force x ForceP {b = True } x = x Forced : LazyP bn -> Bool Forced {b = b} _ = b 

This works fine, but I can't figure out how to determine the first example from the article. In Agda it is:

 left-right : P false left-right = ♯ left-right . ♯ left-right 

But I can't get this to work in Idris:

 lr : P False lr = (Delay lr . Delay lr) 

produces

 Can't unify Lazy' t (P False) with LazyP nm 

This will be typecheck if you give it some help, for example:

 lr : P False lr = (the (LazyP False False) (Delay lr)) . (the (LazyP False False) (Delay lr)) 

But this is rejected by integrity checking, like other options like

 lr : P False lr = Delay (the (LazyP True False) lr) . (the (LazyP False False) (Delay lr)) 

This does not help, I'm not quite sure how the ♯ operator communicates in Agda.

Can anyone see a way to define left right in Idris? Is my definition of P incorrect, or my attempt to translate a function? Or is this Idris integrity check not quite suitable for this co-inductive material?

Answer 1

Currently, trying to transfer this library on his own, it seems that Agda gives Idris different implications. These are the missing implications:

 %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 mn -> LazyP nm -> 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)