[Agda] difficulties with patterns

[Sergei Meshveliani]

Andreas responded recently:


> Mmh, I would guess this is because Agda creates a local function for 
> the
> \ { ... } (which is called "extended-lambda" in Agda-speak).
>
> What you can try instead is to write
>
>   case toBDigits n of \ pr ->
>     let (bs , (_ , hasLast1-if-bs)) = pr
>         ... more let bindings ...
>
>     in cong-...
>
> Cheers,
> Andreas


This is not type-checked:

 hasLast1-toBDigs-suc : (n : ℕ) → HasLast1 $ toBDigs $ suc n
 hasLast1-toBDigs-suc n =
                                
   case  toBDigits n
   of \ pr →
         let (bs , (_ , hasLast1-if-bs)) = pr
             digs-n'          = toBDigs $ suc n
             digs-n'=addC1-bs = toBDigs-suc-eq {n}

             hasLast1-addC1-bs : HasLast1 $ addC1 bs
             hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
         in
         cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs

The report  
 
--------------------
(proj₁ pr) != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl))) of
type (List Bit)
when checking that the expression hasLast1-addC1-bs has type
HasLast1 (addC1 (toBDigs n))
-------------------

looks similar as the previous one (see the citation below).

I tried to compose a stand-alone example of 5 - 15 lines, but my first
simple attempt has failed.

If you do not see such an example, I could consider reducing the
existing one.

Regards,

------
Sergei



On Wed, 2013-11-27 at 18:27 +0400, Sergei Meshveliani wrote:
> Please,
> how can one avoid difficulties in using patterns?
> (what is a common way out?).
> 
> For example, this program works:
> 
>  hasLast1-toBDigs-suc-n : (n : ℕ) → HasLast1 $ toBDigs $ suc n
>  hasLast1-toBDigs-suc-n n =
>              cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs 
>     where
>     pr             = toBDigits n 
>     bs             = proj₁ pr          
>     hasLast1-if-bs = proj₂ $ proj₂ pr         
> 
>     digs-n'          = toBDigs $ suc n
>     digs-n'=addC1-bs = toBDigs-suc-eq {n}
> 
>     hasLast1-addC1-bs : HasLast1 $ addC1 bs
>     hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
> 
> 
> Then I try to improve the style and replace the three assignments and
> projections with pattern matching:
> 
>     case toBDigits n
>     of \
>     { (bs , (_ ,  hasLast1-if-bs)) →
>             let
>                digs-n'          = toBDigs $ suc n
>                digs-n'=addC1-bs = toBDigs-suc-eq {n}
> 
>                hasLast1-addC1-bs : HasLast1 $ addC1 bs
>                hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>             in
>            cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>     }
> 
> And obtain the report 
> 
>   bs != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl)))  
>   of type  (List Bit)
>   when checking that the expression  hasLast1-addC1-bs  has type
>   HasLast1 (addC1 (toBDigs n)).
> 
> The checker somehow does not allow to improve style.
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>