[Agda] Termination Checking in Development Agda

[karim kanso]

Hello Agda Users,

Recently (about a week ago) I upgraded to the latest development version, I
have noticed
that a function that used to pass termination check now does not. To start
with, I am
exploring model checking from Agda as a platform. To this end, I require to
represent
infinite paths as codata.

Using these codata structures complicates matters (particularly with
dependant
pattern matching) so inductive data type of a lasso is defined, then a
translation
from the lasso to infinite paths. It is this translation that is causing
problems.

Below is a simplified version of the problem, instead of a lasso, loops are
used. I have
tested a simpler version that dont require the principle of transfer and
these pass the
termination check. To the best of my understanding the function loop2path
(below)
uses guarded recursion so should pass the check.

Could any one please explain why it applying the proof transfer principle
breaks
termination? Or is this some kind of bug?

Best,
Karim Kanso

module coterm where

open import Data.Nat using (ℕ;suc;zero)
open import Data.Fin using (Fin;suc;zero)
open import Relation.Binary.Core using (_≡_;refl)

transfer : {A : Set} →
           (F : A → Set) →
           (a b : A) →
           (r : a ≡ b) →
           (p : F a) →
           F b
transfer F .b b refl p = p

postulate state : ℕ
postulate action : Fin state → ℕ
postulate transition : (s : Fin state) →
                       (a : Fin (action s)) →
                       Fin state

data Path : Fin state → Fin state → Set where
  end : {s : Fin state} → Path s s
  next : {s' : Fin state} →
         (s : Fin state) →
         (a : Fin (action s)) →
         Path (transition s a) s' → Path s s'

codata Path' : Fin state → Set where
  next : (s : Fin state) →
         (a : Fin (action s)) →
         Path' (transition s a) →
         Path' s

data Loop (s : Fin state) : Set where
  loop : {s' : Fin state} →
         (l : Path s s') →
         (a : Fin (action s')) →
         (lp : s ≡ (transition s' a)) →
         Loop s

loop2path : {s : Fin state} → Loop s → Path' s
loop2path {s} (loop {s'} l a lp) = aux l a lp
  where
    aux : {t t' : Fin state} → (l : Path t t') → (a : Fin (action t')) → (lp
: s ≡ transition t' a) → Path' t
    aux {t} {.t} end a' lp' = next t a' (transfer Path' s (transition t a')
lp' (aux l a lp))
    aux {t} (next .t a' y) a lp = next t a' (aux y a lp)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091218/4b1ddc15/attachment.html