This page is intended to have short snippets of common errors in Agda code, and how to fix these.
Termination checking and nested with
The function isSorted
takes a list and maybe produces a witness that list is sorted.
isSorted : (xs : List ℕ) → Option (Sorted xs) isSorted (x ∷ x' ∷ xs) with isLt x x' isSorted (x ∷ x' ∷ xs) | None = None isSorted (x ∷ x' ∷ xs) | Some a with isSorted (x' ∷ xs) isSorted (x ∷ x' ∷ xs) | Some a | None = None isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted) isSorted (x ∷ []) = Some singleton isSorted [] = Some empty
Agdas termination checker can't see that this termination check. The reason is how the with construct is desugared, it will internally create an auxiliary function and call this.
isSorted (x ∷ x' ∷ xs) = isSorted-aux x x' xs (isLt x x')
This auxiliary function will itself create one more (since we have a nested with) this time we have:
isSorted' x x' xs (Some a) = isSorted'' x x' xs a (isSorted (x' ∷ xs))
This call is not structurally smaller and Agdas termination checker complains. The solution is to make the recursive call earlier.
isSorted : (xs : List ℕ) → Option (Sorted xs) isSorted (x ∷ x' ∷ xs) with isLt x x' | isSorted (x' ∷ xs) isSorted (x ∷ x' ∷ xs) | None | _ = None isSorted (x ∷ x' ∷ xs) | Some xSmaller | None = None isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted) isSorted (x ∷ []) = Some singleton isSorted [] = Some empty
Page last modified on October 10, 2012, at 02:59 pm
Powered by
PmWiki