[Agda] Hindas 2002 flashback

[Conor McBride]

Hi all

Reminded by various goings on, I thought I'd try to hack up
an Agda version of the example from the "Views for Recursion"
talk which James McKinna gave at the 2002 workshop on termination
in type theory. I had a few scares with "Panic: blocked by dot
pattern" along the way, but somehow (actually, when I opened a
mail window to file a query) it eventually decided the program
was ok.

So for your amusement, but a little noisier than James wanted,
here's Euclid's algorithm, built with a view for comparison and
a view for recursion. Or have you done it already?

Happy Thursday

Conor

--------

module Gcd where

data Nat : Set where
   zero : Nat
   suc : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN ZERO    zero #-}

_+_ : Nat -> Nat -> Nat
zero + y = y
suc x + y = suc (x + y)

data _==_ {S : Set}(s : S) : {T : Set}(t : T) -> Set where
   refl : s == s

data NPV (x : Nat) : Set where
   guard : ((y z : Nat) -> x == suc (y + z) -> NPV z) -> NPV x

npv : (x : Nat) -> NPV x
npv zero = guard aha where
   aha : (y z : Nat) -> zero == suc (y + z) -> NPV z
   aha y z ()
npv (suc n) = guard (oho n (npv n)) where
   oho : (n : Nat) -> NPV n -> (y z : Nat) -> (suc n) == suc (y + z) - 
 > NPV z
   oho .z r zero z refl = r
   oho .(suc (y + z)) (guard l) (suc y) z refl = l y z refl

data Cmp : (x y : Nat) -> Set where
   cLt : {x : Nat}(y : Nat) -> Cmp x (x + suc y)
   cEq : {x : Nat}          -> Cmp x x
   cGt : {y : Nat}(x : Nat) -> Cmp (y + suc x) y

cmp : (x y : Nat) -> Cmp x y
cmp zero                 zero                            = cEq
cmp zero                 (suc y)                         = cLt y
cmp (suc x)              zero                            = cGt x
cmp (suc x)              (suc y)           with cmp x y
cmp (suc x)              (suc .(x + suc y))   | cLt y    = cLt y
cmp (suc x)              (suc .x)             | cEq      = cEq
cmp (suc .(y + (suc x))) (suc y)              | cGt x    = cGt x

gcd : Nat -> Nat -> Nat
gcd x y = gcdr x y (npv x) (npv y) where
   gcdr : (x y : Nat) -> NPV x -> NPV y -> Nat
   gcdr x       y                  _     _  with cmp x y
   gcdr zero    (suc .y)           _     _     | cLt y    = suc y
   gcdr (suc x) (suc .(x + suc y)) l (guard r) | cLt y
                 = gcdr (suc x) (suc y) l (r x (suc y) refl)
   gcdr x .x _ _ | cEq = x
   gcdr (suc .x) zero              _     _     | cGt x    = suc x
   gcdr (suc .(y + suc x)) (suc y) (guard l) r | cGt x
                 = gcdr (suc x) (suc y) (l y (suc x) refl) r