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.
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