20070530-4

The following program that does structural recursion on termination predicates (in this case the graphs of the original functions) is not accepted:

Attach:comb.agda

It would also be a nice candidate for doing Brady style optimisation during compilation to erase the termination predicate. This should then yield the original recursive functions as the compiled version.

Here is a simplified version of the program:

 module Comb where

 infixr 50 _→_

 data Ty : Set where
   ι : Ty
   _→_ : Ty -> Ty -> Ty

 data Tm : Ty -> Set where
   _$_ : {σ τ : Ty} -> Tm (σ → τ) -> Tm σ -> Tm τ

 data Nf : Ty -> Set where

 data _⇓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where
   r$ : {σ τ : Ty} -> {t : Tm (σ → τ)} -> {f : Nf (σ → τ)} -> t ⇓ f ->
     {u : Tm σ} -> {a : Nf σ} -> u ⇓ a -> {v : Nf τ} ->
     t $ u ⇓ v

 nf⁼ : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ⇓ n -> Set
 nf⁼ .{τ} (_$_ {σ} {τ} t u) {v} (r$ {f = f} p q) with nf⁼ {σ → τ} t {f} p
 nf⁼ (t $ u) (r$ p q)  |   _ = Ty

The call graph computed for nf⁼ in Termination.TermCheck is the following one:

 [ [Unknown, Unknown, Unknown, Unknown]
 , [Unknown, Unknown, Unknown, Unknown]
 , [Unknown, Lt,      Unknown, Unknown]
 , [Unknown, Unknown, Le,      Unknown]
 ]

However, it should be this one:

 [ [Unknown, Unknown, Unknown, Unknown]
 , [Unknown, Lt,      Unknown, Unknown]
 , [Unknown, Unknown, Lt,      Unknown]
 , [Unknown, Unknown, Unknown, Lt     ]
 ]

Update: Fixed. There was a bug when generating with function calls.