ir in agda

ir.agda

module ind-rec where
open import Data.Empty
open import Data.Product
open import Function
open import Level

record ⊤ {ℓ : Level} : Set ℓ where
  constructor tt

mutual
  data Code : Set → Set₁ where
    ι : {A : Set} → A → Code A
    σ : {B : Set}(A : Set) → (A → Code B) → Code B
    δ : {B : Set}(A : Set) → ((A → B) → Code B) → Code B

  -- Unfold one level of a type
  decode₁ : (U D : Set)(T : U → D) → Code D → Set
  decode₁ U D T (ι x) = ⊤
  decode₁ U D T (σ A c) = Σ A λ a → decode₁ U D T (c a)
  decode₁ U D T (δ A c) = Σ (A → U) λ a → decode₁ U D T (c (T ∘ a))

  -- Unfold one level of the recursive component of an IR defn
  decode₂ : {U D : Set}(T : U → D)(δ : Code D) → decode₁ U D T δ → D
  decode₂ T (ι x) arg = x
  decode₂ T (σ A x) (a , rest) = decode₂ T (x a) rest
  decode₂ T (δ A x) (f , rest) = decode₂ T (x (T ∘ f)) rest

mutual
  data U {D : Set}(γ : Code D) : Set where
    intro : decode₁ (U γ) D (T γ) γ → U γ
  {-# NO_TERMINATION_CHECK #-} -- Can we do without this?
  T : {D : Set}(γ : Code D) → U γ → D
  T γ (intro x) = decode₂ (T γ) γ x

ih : {ℓ : Level}(U D : Set)(T : U → D)(γ : Code D)
   → decode₁ U D T γ
   → (U → Set ℓ)
   → Set ℓ
ih U D T (ι x) arg E = ⊤
ih U D T (σ A x) (a , rest) E = ih U D T (x a) rest E
ih U D T (δ A x) (f , rest) E =
  ((x : A) → E (f x)) × ih U D T (x (T ∘ f)) rest E

call : {ℓ : Level}{U : Set}{D : Set}{T : U → D}(γ : Code D){E : U → Set ℓ}
     → ((a : U) → E a)
     → (a : decode₁ U D T γ) → ih _ _ _ γ a E
call (ι x) f a = tt
call (σ A x) f (a , rest) = call (x a) f rest
call {T = T} (δ A x) f (a , rest) = (f ∘ a) , call (x (T ∘ a)) f rest

{-# NO_TERMINATION_CHECK #-}
rec : {ℓ : Level}{D : Set}(γ : Code D){E : U γ → Set ℓ}
    → ((a : decode₁ (U γ) D (T γ) γ) → ih _ _ _ γ a E → E (intro a))
    → (a : U γ) → E a
rec (ι x) f (intro a) = f a tt
rec (σ A x) f (intro (a , rest)) =
  f (a , rest) (call (x a) (rec (σ A x) f) rest)
rec (δ A x) f (intro (a , rest)) =
  f (a , rest) (rec _ f ∘ a , call (x (T _ ∘ a)) (rec _ f) rest)

data Two : Set where
  one : Two
  two : Two

ℕ : Code ⊤
ℕ = σ Two λ { one → ι tt; two → δ ⊤ λ _ → ι tt }

z : U ℕ
z = intro (one , tt)

s : U ℕ → U ℕ
s n = intro (two , (λ _ → n) , tt)

recℕ : {A : U ℕ → Set} → A z → ((n : U ℕ) → A n → A (s n))
      → (n : U ℕ) → A n
recℕ {A = A} zc sc a = rec ℕ go a
  where go : (a : decode₁ (U ℕ) ⊤ (T ℕ) ℕ) → ih _ _ _ ℕ a A → A (intro a)
        go (one , tt) ih = zc
        go (two , n , tt) (ih , tt) = sc (n tt) (ih tt)

plus : U ℕ → U ℕ → U ℕ
plus n m = recℕ m (λ _ → s) n