Derive.agda

module Derive where
  open import Data.Product using (_×_; _,_)
  open import Data.Sum using (_⊎_; inj₁; inj₂)
  open import Data.Unit using (⊤)
  open import Data.Empty using (⊥)
  open import Data.Nat using (ℕ ; suc ; zero ; _+_)
  open import Data.Fin using (Fin ; inject₁ ; suc ; zero)
  open import Data.Fin.Properties using (_≟_)
  open import Relation.Nullary using (yes ; no)
  open import Agda.Builtin.Equality using (refl)

  -- Regular universe, multivariate.
  -- |n| defines the number of variables
  data Reg : ℕ → Set₁ where
    0′    : {n : ℕ} → Reg n
    1′    : {n : ℕ} → Reg n
    I     : {n : ℕ} → Fin n → Reg n
    _⨁_  : {n : ℕ} → (l r : Reg n) → Reg n
    _⨂_  : {n : ℕ} → (l r : Reg n) → Reg n
    μ′    : {n : ℕ} → Reg (suc n)   → Reg n

  infixl 30 _⨁_
  infixl 40 _⨂_

  data Env : ℕ → Set₁ where
    []  : Env 0
    _,_ : {n : ℕ} → Reg n → Env n → Env (suc n)

  mutual
    ⟦_⟧ : {n : ℕ} → Reg n → Env n → Set
    ⟦ 0′ ⟧  _ = ⊥
    ⟦ 1′ ⟧  _ = ⊤
    ⟦ I zero  ⟧   (X , Xs) = ⟦ X ⟧  Xs
    ⟦ I (suc n) ⟧ (X , Xs) = ⟦ I n ⟧ Xs
    ⟦ L ⨁ R ⟧ Xs = ⟦ L ⟧ Xs ⊎ ⟦ R ⟧ Xs
    ⟦ L ⨂ R ⟧ Xs = ⟦ L ⟧ Xs × ⟦ R ⟧ Xs
    ⟦  μ′ F  ⟧ Xs =  μ F Xs

    data μ {n : ℕ} (F : Reg (suc n)) (Xs : Env n) : Set where
      ⟨_⟩ : ⟦ F ⟧ (μ′ F , Xs) → μ F Xs

  inject₁ᵣ : {n : ℕ} → Reg n → Reg (suc n)
  inject₁ᵣ 0′       = 0′
  inject₁ᵣ 1′       = 1′
  inject₁ᵣ (I x)    =  I (inject₁ x)
  inject₁ᵣ (L ⨁ R) = (inject₁ᵣ L) ⨁ (inject₁ᵣ R)
  inject₁ᵣ (L ⨂ R) = (inject₁ᵣ L) ⨂ (inject₁ᵣ R)
  inject₁ᵣ (μ′ F)   = μ′ (inject₁ᵣ F)

  infixl 50 _[_]
  infixl 50 ^_

  _[_]  : {n : ℕ} → Reg (suc n) → Reg n → Reg n
  0′ [ G ]        = 0′
  1′ [ G ]        = 1′
  I zero [ G ]    = G
  I (suc x) [ G ] = I x
  (L ⨁ R) [ G ]  = L [ G ] ⨁ R [ G ]
  (L ⨂ R) [ G ]  = L [ G ] ⨂ R [ G ]
  μ′ F [ G ]      = μ′ (F [ inject₁ᵣ G ])


  ^_ : {n : ℕ} → Reg n → Reg (suc n)
  ^ 0′       = 0′
  ^ 1′       = 1′
  ^ I x      = I (suc x)
  ^ (L ⨁ R) = ^ L ⨁ ^ R
  ^ (L ⨂ R) = ^ L ⨂ ^ R
  ^ μ′ F     = μ′ (inject₁ᵣ F)

  derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
  derive = {!!}


  {-
  derive {zero} ()
  derive {suc _} i 0′ = 0′
  derive {suc _} i 1′ = 0′
  derive {suc _} i (I j) with i ≟ j
  derive {suc _} i (I j) | yes refl = 1′
  ...                    | no _     = 0′
  derive {suc _} i (L ⨁ R) = derive i L ⨁ derive i R
  derive {suc _} i (L ⨂ R) = (derive i L ⨂ R) ⨁ (L ⨂ derive i R)
  derive {suc n} i (μ′ F) = μ′ ( 1′ ⨁ ((derive zero (^ (F [ μ′  F ])) ⨂ I zero))) ⨂ (derive (suc i)  F [ μ′ F ])
  -}