Внедрение Total Parsers в Idris на основе статьи на Agda

Я пытаюсь реализовать общие парсеры с Idris на основе этой статьи. Сначала я попытался реализовать более простой тип распознавателя 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

Это прекрасно работает, но я не могу понять, как определить первый пример из статьи. В Агде это:

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

Но я не могу заставить это работать в Идрисе:

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

производит

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

Он проверит тип, если вы ему немного поможете, например:

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

Но это отвергается проверкой целостности, как и другие варианты, такие как

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

Не помогает то, что я не совсем уверен, как связывается оператор ♯ в Agda.

Может ли кто-нибудь найти способ определить распознаватель левого и правого в Идрисе? Мое определение P неверно или моя попытка перевести функцию? Или проверка целостности Идриса просто не совсем подходит для этого коиндуктивного материала?


parsing dependent-type parser-combinators idris agda
person Vic Smith    schedule 01.12.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В настоящее время я пытаюсь перенести эту библиотеку, похоже, что Agda предполагает различные имплициты для Idris. Вот недостающие имплициты:

%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)
person oisdk    schedule 02.04.2017
comment
Это работает! Я так долго от этого не подходил, что мне потребуется немного времени, чтобы должным образом пересмотреть это и понять, почему это работает. Я приму, как только смогу это сделать. - person Vic Smith; 03.05.2017