Implementierung Gesamt Parser in Idris Basierend auf einem Papier auf Agda

Question

Ich versuche, Parser mit Idris basierend auf this paper zu implementieren. Zuerst habe ich versucht, den grundlegen Erkenner Typen P zu implementieren:

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 

Dies funktioniert gut, aber ich kann nicht herausfinden, wie das erste Beispiel aus dem Papier zu definieren. In Agda ist es:

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

Aber ich kann dies in Idris arbeiten nicht bekommen:

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

produziert

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

Es wird typecheck, wenn Sie es etwas Hilfe geben, wie folgt aus:

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

Aber das ist abzulehnen ed durch die Gesamtheit checker, als andere Varianten sind wie

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

Es hilft nicht, dass ich nicht ganz sicher bin, wie der ♯ Operator in Agda bindet.

Kann jemand einen Weg sehen, den links-rechts-Erkenner in Idris zu definieren? Ist meine Definition von P falsch oder mein Versuch, die Funktion zu übersetzen? Oder ist Idris 'totaler Checker einfach nicht auf dieses coinductive Zeug?

Answer 1

Derzeit versuche ich, diese Bibliothek selbst zu portieren, es scheint, als ob Agda verschiedene Implikationen mit Idris hat. Dies sind die fehlenden 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)