[Agda] Termination checking with partiality monad

[Nils Anders Danielsson]

On 2011-08-18 21:32, Brandon Moore wrote:
> mutual
>    app : Trace → Trace → Trace
>    app (Call f) a = Call (♯ (app (♭ f) a))
>    app f (Call a) = Call (♯ (app f (♭ a)))
>    app Fail _ = Fail
>    app _ Fail = Fail
>    app (Ret (Closure env body)) (Ret val) = Call (♯ (eval (val ∷ env) body))
>
>    eval : {scope : ℕ} → Vec Val scope → Exp scope → Trace
>    eval env (var v) = Ret (lookup v env)
>    eval env (f $ a) = app (eval env f) (eval env a)
>    eval env (lam body) = Ret (Closure env body)

The productivity checker cannot handle nested calls to app (as in the
second clause of eval).

-- 
/NAD