[Agda] Termination checker on commutative functions

[Jacek Karwowski]

Hi,

I'm trying to write a commutative function over some type, and not repeat
the code in the process.

The toy example is as follows:
```
module _ where

open import Data.Nat

data Int : {i : Size} -> Set where
  Pos : (x : ℕ) -> Int
  Neg : (x : ℕ) -> Int

_⊕_ : Int -> Int -> Int
Pos x ⊕ Pos y = Pos (x + y)
Neg x ⊕ Neg y = Neg (x + y)
Pos x ⊕ Neg zero = Pos x
Pos zero ⊕ Neg y = Neg y
Pos (suc x) ⊕ Neg (suc y) = (Pos x) ⊕ (Neg y)
--- problematic call
Neg x ⊕ Pos y = (Pos y) ⊕ (Neg x)
```
In the example above, termination checker complains about the last call,
since it is not a structural recursion.

(Of course, real types can (and do) have more than two constructors, the
constructors are recursive, etc.)

The naive, manual way I see would be to introduce an explicit order on the
constructors by some external function, and then call ⊕ passing this
parameter over:

```
ord : Int -> ℕ
ord (Pos _) = 0
ord (Neg _) = 1

_⊕_ : {s : ℕ} -> (x : Int) -> {s ≡ ord x} -> Int -> Int
Pos x ⊕ Pos y = Pos (x + y)
Neg x ⊕ Neg y = Neg (x + y)
Pos x ⊕ Neg zero = Pos x
Pos zero ⊕ Neg y = Neg y
Pos (suc x) ⊕ Neg (suc y) = _⊕_ {zero} (Pos x) {refl} (Neg y)
--- problematic call
_⊕_ {suc zero} (Neg x) (Pos y) = _⊕_ {zero} (Pos y) {refl} (Neg x)
```
but this ends up being very ugly and hard to read.

What is the idiomatic way of handling these types of situations,
introducing as little code overhead as possible?

Thanks,
Jacek
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191030/50fe01c8/attachment.html>