Тип проверки Агды взрывается - PullRequest
0 голосов
/ 11 февраля 2019

Следующий код предназначен для описания C / C ++ -подобных перечислений, которые могут занимать 4 байта, хотя все, что они должны содержать, это всего лишь несколько различных альтернатив.

open import Prelude.Bool
open import Prelude.Nat
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Numeric.Nat.Pow renaming (_^′_ to _^_)

data Enum : Set where
  makeEnum : (size : Nat) → (variants : Nat) → 
             .{{ _ : (variants < size) ≡ true }} → Enum

five : Enum
five = makeEnum (2 ^ 32) 5

data Expr : (t : Enum) → Set where
  constant : (x : Nat) → Expr five

Пока все хорошо.Все тип проверяет красиво.Однако добавление следующих строк

func : ∀ {t} → Expr t → Bool
func (constant x) = false

, которые, кажется, ничего не делают, приводит к невозможности проверки типа и истощению всех системных ресурсов.

Я неЯ не вижу ничего, кроме аргумента экземпляра, который может привести к этому, но это, кажется, не согласуется с тем фактом, что Agda способна как решить, так и проверить тип следующего

5<2³² : (5 < 2 ^ 32) ≡ true
5<2³² = refl

в кратчайшие сроки.Так что же происходит?

1 Ответ

0 голосов
/ 12 февраля 2019

На вопрос ответил Джеспер Кокс.Оказывается, это была ошибка компилятора, которая будет исправлена ​​в следующей версии Agda.

Обновление : ошибка уже исправлена ​​в основной ветке.

...