Example of Small IR

Sums.agda

module Sums where

open import Data.Nat
open import Data.Fin using (Fin; module Fin)
open import Function

sum : (k : ℕ) (f : Fin k → ℕ) → ℕ
sum zero    f = 0
sum (suc k) f = f Fin.zero + sum k (f ∘ Fin.suc)

mutual

  data Tm : Set where
    `val : ℕ → Tm
    `sum : (k : Tm) (f : Fin ⟦ k ⟧ → Tm) → Tm

  ⟦_⟧ : Tm → ℕ
  ⟦ `val n   ⟧ = n
  ⟦ `sum t f ⟧ = sum ⟦ t ⟧ (λ x → ⟦ f x ⟧)


mutual

  data Tm' : Set where
    `val : ℕ → Tm'
    `sum : (k : Tm') {k' : ℕ} (⟦k⟧ : ⟦ k ⟧'≡ k') (f : Fin k' → Tm') → Tm'

  data ⟦_⟧'≡_ : Tm' → ℕ → Set where
    `⟦val⟧ : {n : ℕ} → ⟦ `val n ⟧'≡ n
    `⟦sum⟧ : {t : Tm'} {t' : ℕ} (⟦t⟧ : ⟦ t ⟧'≡ t') {f : Fin t' → Tm'} {f' : Fin t' → ℕ}
             (⟦f⟧ : ∀ k → ⟦ f k ⟧'≡ f' k) → ⟦ `sum t ⟦t⟧ f ⟧'≡ sum t' f'