[Agda] matching to Sum

[Andreas Abel]

The type  hasrepetition A xs  is not a datatype unless it can be 
reduced (in case xs is a [] or a cons).  In your case, it did not 
reduce, since the coverage checker did not split on xs due to the 
missing [] case.


On 2013-10-15 11:13, Sergei Meshveliani wrote:
> On Tue, 2013-10-15 at 01:07 +0200, Andreas Abel wrote:
>> The pattern matching is incomplete.  It works with complete pattern
>> matching:
>>
>> cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) = inj₂ (inj₁ y∈xs)
>> cons-hasRepetition A x (y ∷ xs) (inj₂ h)   = inj₂ (inj₂ h)
>> cons-hasRepetition A x [] (Level.lift ())
>
> I see. Thank you
>
> Does the checker report need improvement?
> ("Incomplete pattern matching"
>  rather than
>  "Cannot split on argument of non-datatype"
> ).
>
> I often advance with implementation by doing the first pattern.
> After I get "Incomplete pattern matching", I see that the given 
> patterns
> are checked, and start with the next pattern.
>
> And in this case I was mislead.
> Where is an argument of non-datatype?
>
> Regards,
>
> ------
> Sergei
>
>
>>
>> On 12.10.2013 21:38, Sergei Meshveliani wrote:
>> > Please, why the pattern  (inj₁ y∈xs)   below is checked-out?
>> >
>> > I know that
>> >         cons-hasRepetition A x xs hasRep-xs =  inj₂ hasRep-xs
>> >
>> > is sufficient.
>> > But the question about the pattern  (inj₁ y∈xs)  still remains.
>> >
>> >
>> > -----------------------------------------------------------------
>> > module Report4 where
>> > open import Level using (Level; _⊔_; Lift)
>> > open import Relation.Binary using (Setoid; module Setoid)
>> > open import Data.Empty    using (⊥)
>> > open import Data.Sum      using (_⊎_; inj₁; inj₂)
>> > open import Data.List     using (List; []; _∷_)
>> > open import Data.List.Any using (module Membership)
>> >
>> > 
>> --------------------------------------------------------------------
>> > hasRepetition : ∀ {c l} (A : Setoid c l) → List (Setoid.Carrier A) 
>> →
>> >                                                          Set (c ⊔ 
>> l)
>> > hasRepetition _ []       =  Lift ⊥
>> > hasRepetition A (x ∷ xs) =  x ∈ xs  ⊎ (hasRepetition A xs)
>> >                          where
>> >                          open module MembA = Membership A using 
>> (_∈_)
>> >
>> > cons-hasRepetition :
>> >          ∀ {c l} (A : Setoid c l) →
>> >          let C = Setoid.Carrier A
>> >          in
>> >          (x : C) → (xs : List C) → hasRepetition A xs →
>> >                                    hasRepetition A (x ∷ xs)
>> >
>> > cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) =  inj₂ (inj₁ y∈xs)
>> > 
>> --------------------------------------------------------------------
>> >
>> > The report is
>> >
>> >    Cannot split on argument of non-datatype   hasRepetition A xs
>> >    when checking the definition of  cons-hasRepetition.
>>
>>

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

Theoretical Computer Science, University of Munich 
http://www.tcs.informatik.uni-muenchen.de/~abel/