[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Thanks Andreas! Now I see that it didn't work because I used:

merge h1 h2 with h1 | h2

as a workaround for Agda's lack of @ patterns.

Janek

Dnia poniedziałek, 2 grudnia 2013, Andreas Abel napisał:
> Here you go:
> Note that unconstraint sizes default to \inf, so you need to give sizes
> in type signatures where sizes are important, e.g. in merge.
>
> {-# OPTIONS --sized-types #-}
>
> open import Size
> open import Data.Bool
>
> module _ (Rank Priority : Set) (_<_ : Priority → Priority → Bool) where
>
> data Heap : {i : Size} → Set where
>    empty : {i : Size} → Heap {↑ i}
>    node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑ i}
>
> module _ (makeT : Priority → Heap → Heap → Heap) where
>
>    merge : {i : Size} → Heap {i} → Heap {i} → Heap
>    merge empty h2 = h2
>    merge h1 empty = h1
>    merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  with p1 < p2
>    merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | true  =
>      makeT p1 l1 (merge r1 (node p2 w2 l2 r2))
>    merge (node p1 w1 l1 r1) (node p2 w2 l2 r2)  | false =
>      makeT p2 l2 (merge (node p1 w1 l1 r1) r2)
>
> Depending on what makeT is, you might be able to give a more precise
> type to merge.
>
> On 02.12.2013 12:38, Jan Stolarek wrote:
> > Ok, I think I need some help with Sized types. I have a datatype
> > representing a Heap:
> >
> > data Heap : {i : Size} → Set where
> >    empty : {i : Size} → Heap {↑ i}
> >    node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑
> > i}
> >
> > And I need to use sized types in merge function:
> >
> > merge : {i : Size} → Heap → Heap → Heap
> > merge h1 h2 with h1 | h2
> > merge h1 h2 | empty | _ = h2
> > merge h1 h2 | _ | empty = h1
> > merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  with p1 < p2
> > merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2 r2)  | true  = makeT
> > p1 l1 (merge r1 h2) merge h1 h2  | (node p1 w1 l1 r1)  | (node p2 w2 l2
> > r2)  | false = makeT p2 l2 (merge h1 r2)
> >
> > Can I please have a hint how to do that? I tried adding annotation
> > according to this presentation:
> >
> > www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf‎
> >
> > but with no success :-/ I keep getting errors like i != inf.
> >
> > Janek