Implementazione di parser totali in Idris basato su un documento su Agda

Question

Sto cercando di implementare i parser totali con Idris, in base a this paper. Ho cercato di attuare il tipo riconoscitore più fondamentale 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 

Questo funziona bene, ma non riesco a capire come definire il primo esempio dalla carta. In Agda è:

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

Ma io non posso farlo funzionare in Idris:

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

produce

Can't unify 
    Lazy' t (P False) 
with 
    LazyP n m 

Sarà TYPECHECK se si dà un po 'di aiuto, in questo modo:

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

Ma questo è rifiutato cato dal correttore totalità, come lo sono le altre varianti come

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

Non aiuta che io non sono del tutto sicuro di come l'operatore ♯ si lega a Agda.

Qualcuno può vedere un modo per definire il riconoscitore left-right in Idris? La mia definizione di P è errata o il mio tentativo di tradurre la funzione? O il controllore di totalità di Idris non è proprio all'altezza di questa roba coinduttiva?

Answer 1

Attualmente sto provando a portare questa libreria da solo, sembra che Agda deduca diversi impliciti per Idris. Questi sono gli impliciti mancanti:

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