[Agda] Termination problems with "with" and recursion

[Andreas Abel]

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


-- 
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/
-------------- next part --------------
{-# OPTIONS --sized-types #-}

open import Size
open import Data.Bool

module _ (Rank Priority : Set) (_<_ : Priority → Priority → Bool) where

-- 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}

module _ (makeT : Priority → Heap → Heap → Heap) where

-- And I need to use sized types in merge function:

  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)

{- 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 -}