Могу ли я использовать нормальную форму значения, чтобы избежать неполных совпадений с образцом в Agda? - PullRequest
Новая
       11

Могу ли я использовать нормальную форму значения, чтобы избежать неполных совпадений с образцом в Agda?

1 голос
/ 28 мая 2019

В следующей программе Agda я получаю предупреждение о пропущенном регистре в определении one, несмотря на то, что myList соответствует только регистру cons. 

open import Data.Nat

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))

one : ℕ
one with myList 
... | (cons x xs) = x

Incomplete pattern matching for .test.with-16. Missing
cases:
  one | nil

Я знаю, что это звучит немного запутанно, но есть ли способ определить one в терминах myList, не сталкиваясь с ошибками "неполного сопоставления с образцом"?

Этот пример является упрощением моей первоначальной задачи, которая основана на домашнем задании и использует несколько более сложные типы. В этом случае "myList" - это большое значение, вычисляемое умной функцией из небольшого ввода. Если я вычислю нормальную форму "myList" с помощью Emacs 'Agda Mode (C-c C-n), я смогу извлечь из нее значение "one" и вставить его в свою программу. Однако это значение занимает несколько десятков строк при распечатке, поэтому я бродил, если есть способ напрямую определить "one" в терминах "myList", не сталкиваясь с неполной ошибкой сопоставления с образцом.

Ответы [ 2 ]

3 голосов
/ 28 мая 2019

Если вы используете with e, тогда e извлекается (например, лямбда-абстракция) из цели и контекста, и вас просят продолжить, как если бы у вас была переменная вместо самой e.Таким образом, следующее сопоставление с образцом вообще не учитывает значение myList (что довольно нелогично, но просто является синтаксическим сахаром для создания вспомогательного определения с одним дополнительным аргументом).

Однако вы можете написать следующее: 

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

myList : List ℕ
myList = 1 ∷ 2 ∷ 3 ∷ []

head : {n : ℕ} {ns : List ℕ} (xs : List ℕ) → n ∷ ns ≡ xs → ℕ
head (x ∷ xs) refl = x

one : ℕ
one = head myList refl

Вы также можете посмотреть шаблон inspect в стандартной библиотеке для более общего решения этой проблемы.

2 голосов
/ 30 мая 2019

Вы можете отразить значение на уровне типа, а затем сопоставить шаблон с ним. Выглядит так: 

open import Data.Nat

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))

data Sing {α} {A : Set α} : A -> Set where
  sing : ∀ x -> Sing x

one : ℕ
one with sing myList
... | sing (cons x (cons _ (cons _ nil))) = x
...