[Agda] certain report

[Andreas Abel]

See below.

On 19.08.13 5:58 PM, Sergei Meshveliani wrote:
> open import Level            using (Level) renaming (zero to 0L)
> open import Function         using (case_of_)
> open import Relation.Nullary using (Dec; yes; no)
> open import Relation.Unary   using (Decidable)
> open import Relation.Binary  using (Rel; Setoid; module Setoid;
>                                      DecSetoid; module DecSetoid)
> open import Relation.Binary.Core using (_Respects_)
> open import Data.Empty    using (⊥-elim)
> open import Data.Maybe    using (Maybe; just; nothing)
> open import Data.Product  using (_×_; _,_)
> open import Data.List     using (List; []; _∷_)
> open import Data.List.Any using (Any; module Any)
>
> -------------------------------------------------------------------------
> toMaybe' : ∀ {p} {C : Set} {P : C → Set p} → Decidable P → C → Maybe C
> toMaybe' P? x  with P? x
> ...                      | yes _ =  just x
> ...                      | _     =  nothing
>
> record Triple {p} {C : Set} {P : C → Set p} (P? : Decidable P) : Set 0L
>    where
>    constructor trp
>
>    field  X : C
>
>    P?x : Dec (P X)
>    P?x = P? X
>    mb : Maybe C
>    mb = toMaybe' P? X
>
> filterTriples : ∀ {p} {C : Set} {P : C → Set p} {P? : Decidable P} →
>                                      List (Triple P?) → List (Triple P?)
> filterTriples []      = []
> filterTriples (t ∷ ts)  with  Triple.P?x t
> ...                      | yes _ =  t ∷ (filterTriples ts)
> ...                      | no _  =  filterTriples ts
>
> open Triple
>
> foo : ∀ {l p} (A : Setoid 0L l) →
>    let
>       open Setoid A using (_≈_) renaming (Carrier to C)
>    in
>    (P : C → Set p) → (P? : Decidable P) → P Respects _≈_ → (x : C) →
>    P x → (ts : List (Triple P?)) → Any (\ t → x ≈ (X t)) ts →
>                        Any (\ t → x ≈ (X t)) (filterTriples {P? = P?} ts)
>
> open Any
>
> foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt)
>
>             with P?x t
> ...      | yes q = _
>
> {-
>     = case P?x t of \
>                  { (no ¬Px-t) → let PX-t : P (X t)
>                                     PX-t = pCong x=Xt Px
>                                 in  ⊥-elim (¬Px-t PX-t)
>                    (yes q) → _

                    ^ Here is a ; missing

>                  }
> -}
> -----------------------------------------------------------------------
>
> 1. The report is of kind
>
> Inaccessible (dotted) patterns from the parent clause must also be
> inaccessible in the with clause, when checking the pattern {trp},
> when checking that the clause
> foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt) with P?x t
> foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt) | yes q = _
> has type
> ...

This is fixed in the darcs version of Agda.

> 2. Comment out the two lines of  `with'  and un-comment the `case'
> variant.
> The report is
>
>    Not in scope:
>       q at /home/mechvel/doconA/0.03/source/demoTest/Report.agda:61,29-30
>    when scope checking q
>
> Why not in scope?  Here it must be a value  q : P (X t).

You forgot a semicolon to separated the clauses of an extended lambda.

> 2.1. Change `q' to `_'
>       The report is
>       "Incomplete pattern matching for .extendedlambda0.
>        Missing cases: ... "

The case for 'there' is missing.


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/