Implementacja wszystkich analizatorów składni w Idris na podstawie dokumentu o Agdzie

Question

Próbuję zaimplementować parsery całkowite z Idrisem, oparte na this paper. Najpierw próbował wdrożyć bardziej podstawowy typ rozpoznającym 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 

Działa to dobrze, ale nie mogę dowiedzieć się, jak zdefiniować pierwszy przykład z papieru. W Agda to:

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

Ale nie mogę uzyskać to do pracy w Idris:

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

produkuje

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

Będzie typecheck jeśli dać mu jakąś pomoc, na przykład:

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

Ale to jest odrzucenie ed przez sprawdzający totalności, jak również inne warianty, takie jak

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

to nie pomaga, że ​​nie jestem do końca pewien, jak operator ♯ wiąże w Agda.

Czy każdy może znaleźć sposób, aby zdefiniować lewy-prawy rozpoznawcę w Idris? Czy moja definicja P jest błędna, czy moja próba tłumaczenia funkcji? Czy też sprawdzanie totalizmu w Idrisie nie jest do końca zgodne z tym coinductive stuff?

Answer 1

Obecnie próbuje przesłać tę bibliotekę samodzielnie, wydaje się, że Agda wprowadza różne implikacje do Idris. Oto brakujące implikacje:

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