Agda - Counting Fixpoint In constructors

To practice Agda, I have been given an exercise. (Not graded)

Given the Fixpoint;

data Fix (r : Regular) : Set where
  In : (semantics r) (Fix r) -> Fix r

And the definition for regular pattern functors with semantics

data Regular : Set where
  I :  Regular
  U : Regular
  _<+>_ : Regular -> Regular -> Regular
  _<x>_ : Regular -> Regular -> Regular

semantics : Regular -> Set -> Set
semantics I X = X
semantics U X = ⊤ 
semantics (r1 <+> r2) X = Either(semantics r1 X) (semantics r2 X)
semantics (r1 <x> r2) X = Pair (semantics r1 X) (semantics r2 X)

I must define a function gsize : (r : Regular) -> Fix r -> Nat such that a call gsize r t counts the total number of In constructors that occur in t.

As tip, one can define an auxiliary function size: semantics r (Fix r') -> Nat for all regular types r and r'.

I have been stuck on this for hours. Could someone please help me.

Solution

You need to use mutual recursion:

size : {r r' : Regular} → semantics r (Fix r') → ℕ
gsize : {r : Regular} → Fix r → ℕ

size {I} t = gsize t
size {U} tt = 0
size {A <+> B} (left a) = size a
size {A <+> B} (right b) = size b
size {A <x> B} (pair a b) = size a + size b
gsize (In x) = suc (size x)

List⊤ = Fix (U <+> (U <x> I))
mkList⊤ : ℕ → List⊤
mkList⊤ 0 = In (left tt)
mkList⊤ (suc n) = In (right (pair tt (mkList⊤ n)))

_ : gsize (mkList⊤ 3) ≡ 4
_ = refl