Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid

larrytheliquid/SafeGenerallyIndexedIR.agda

Last active February 5, 2017 22:24
Show Gist options
  • Save larrytheliquid/14bf1ce208c13e543a6d20f60e903ae9 to your computer and use it in GitHub Desktop.
Save larrytheliquid/14bf1ce208c13e543a6d20f60e903ae9 to your computer and use it in GitHub Desktop.
Download ZIP
Inductive-recursive and infinitary version of https://gist.github.com/larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c
Raw
SafeGenerallyIndexedIR.agda
open import Data.Unit
open import Data.Product
module _ where
----------------------------------------------------------------------
data Desc (I : Set) (O : I → Set) : Set₁ where
`ι : (i : I) (o : O i) → Desc I O
`δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
`σ : (A : Set) (D : A → Desc I O) → Desc I O
mutual
data μ {I O} (R : I → Desc I O) (i : I) : I → Set where
init : (xs : ⟦ R i ⟧ R) → μ R i (proj₁ (io (R i) R xs))
ode : ∀ {I O} (R : I → Desc I O) (i j : I) → μ R i j → O j
ode R i ._ (init xs) = proj₂ (io (R i) R xs)
⟦_⟧ : ∀{I O} (D : Desc I O) (R : I → Desc I O) → Set
⟦ `ι i o ⟧ R = ⊤
⟦ `δ A i D ⟧ R = Σ ((a : A) → μ R (i a) (i a)) λ f → ⟦ D (λ a → ode R (i a) (i a) (f a)) ⟧ R
⟦ `σ A D ⟧ R = Σ A λ a → ⟦ D a ⟧ R
io : ∀{I O} (D : Desc I O) (R : I → Desc I O) (xs : ⟦ D ⟧ R) → Σ I O
io (`ι i o) R tt = i , o
io (`δ A i D) R (f , xs) = io (D (λ a → ode R (i a) (i a) (f a))) R xs
io (`σ A D) R (a , xs) = io (D a) R xs
----------------------------------------------------------------------
Hyps : ∀{I O} (R : I → Desc I O) (P : (i j : I) → μ R i j → Set) (D : Desc I O) (xs : ⟦ D ⟧ R) → Set
Hyps R P (`ι i o) tt = ⊤
Hyps R P (`σ A D) (a , xs) = Hyps R P (D a) xs
Hyps R P (`δ A i D) (f , xs) = ((a : A) → P (i a) (i a) (f a))
× Hyps R P (D (λ a → ode R (i a) (i a) (f a))) xs
----------------------------------------------------------------------
ind :
∀{I O}
(R : I → Desc I O)
(P : (i j : I) → μ R i j → Set)
(pcon : (i : I) (xs : ⟦ R i ⟧ R) → Hyps R P (R i) xs → P i (proj₁ (io (R i) R xs)) (init xs))
(i j : I)
(x : μ R i j)
→ P i j x
hyps :
∀{I O}
(R : I → Desc I O)
(P : (i j : I) → μ R i j → Set)
(pcon : (i : I) (xs : ⟦ R i ⟧ R) → Hyps R P (R i) xs → P i (proj₁ (io (R i) R xs)) (init xs))
(D : Desc I O)
(xs : ⟦ D ⟧ R)
→ Hyps R P D xs
ind R P pcon i j (init xs) = pcon i xs (hyps R P pcon (R i) xs)
hyps R P pcon (`ι i o) tt = tt
hyps R P pcon (`σ A D) (a , xs) = hyps R P pcon (D a) xs
hyps R P pcon (`δ A i D) (f , xs) = (λ a → ind R P pcon (i a) (i a) (f a))
, hyps R P pcon (D (λ a → ode R (i a) (i a) (f a))) xs
----------------------------------------------------------------------
Raw
UnsafeGenerallyIndexedIR.agda
open import Data.Unit
open import Data.Product
module _ where
----------------------------------------------------------------------
data Desc (I : Set) (O : I → Set) : Set₁ where
`ι : (i : I) (o : O i) → Desc I O
`δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
`σ : (A : Set) (D : A → Desc I O) → Desc I O
⟦_⟧ : ∀{I O} (D : Desc I O) (X : I → I → Set) (Y : (i j : I) → X i j → O j) → Set
⟦ `ι i o ⟧ X Y = ⊤
⟦ `δ A i D ⟧ X Y = Σ ((a : A) → X (i a) (i a)) λ f → ⟦ D (λ a → Y (i a) (i a) (f a)) ⟧ X Y
⟦ `σ A D ⟧ X Y = Σ A λ a → ⟦ D a ⟧ X Y
io : ∀{I O} (D : Desc I O) (X : I → I → Set) (Y : (i j : I) → X i j → O j) (xs : ⟦ D ⟧ X Y) → Σ I O
io (`ι i o) X Y tt = i , o
io (`δ A i D) X Y (f , xs) = io (D (λ a → Y (i a) (i a) (f a))) X Y xs
io (`σ A D) X Y (a , xs) = io (D a) X Y xs
{-# TERMINATING #-}
mutual
data μ {I O} (R : I → Desc I O) (i : I) : I → Set where
init : (xs : ⟦ R i ⟧ (μ R) (ode R)) → μ R i (proj₁ (io (R i) (μ R) (ode R) xs))
ode : ∀ {I O} (R : I → Desc I O) (i j : I) → μ R i j → O j
ode R i ._ (init xs) = proj₂ (io (R i) (μ R) (ode R) xs)
----------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment