module GenSyntax where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.List
open import Data.Product
open import Data.Unit
open import Data.Bool
open import Relation.Binary.PropositionalEquality
Arity : Set
Arity = List Bool

module Dummy (L : Set) (B : Set) (ar : B -> Arity) where
 mutual
  data Tm (n : ℕ) : Set where
    _◂_ : (l : L) -> (i : Fin n) -> Tm n
    _∙_ : (b : B) -> (as : Args n (ar b)) -> Tm n

  Args : ℕ -> List Bool -> Set
  Args n [] = ⊤
  Args n (x ∷ xs) = Tm (if x then (suc n) else n) × Args n xs

  Sub : ℕ -> ℕ -> Set
  Sub m n = (∀ (l : L) d -> Fin (d + m) -> Tm (d + n)) 

 mutual
  graft : ∀ {m n} -> (∀ (l : L) d -> Fin (d + m) -> Tm (d + n)) -> ∀ d -> Tm (d + m) -> Tm (d + n)
  graft f d (l ◂ i) = f l d i
  graft f d (b ∙ as) = b ∙ grafts f (ar b) d as
 
  grafts : ∀ {m n} -> (∀ (l : L) d -> Fin (d + m) -> Tm (d + n)) -> ∀ xs -> ∀ d -> Args (d + m) xs -> Args (d + n) xs
  grafts f [] d t = tt
  grafts f (true ∷ xs) d (t , ts) = graft f (suc d) t , grafts f xs d ts
  grafts f (false ∷ xs) d (t , ts) = graft f d t , grafts f xs d ts

 mutual
  graft-id : ∀ {m} d t -> graft {m} {m} (\ l d i -> l ◂ i) d t ≡ t
  graft-id d (l ◂ i) = refl
  graft-id d (b ∙ as) = cong (_∙_ b) (grafts-id (ar b) d as)

  grafts-id : ∀ {m} xs d ts -> grafts {m} {m} (\ l d i -> l ◂ i) xs d ts ≡ ts
  grafts-id [] d ts = refl
  grafts-id (true ∷ xs) d ts = cong₂ _,_ (graft-id (suc d) _) (grafts-id xs d _)
  grafts-id (false ∷ xs) d ts = cong₂ _,_ (graft-id d _) (grafts-id xs d _)
 
 mutual
  graft-ext : ∀ {m n} -> (f g : Sub m n) -> (∀ l d i -> f l d i ≡ g l d i) -> ∀ d t -> graft {m} {n} f d t ≡ graft {m} {n} g d t
  graft-ext f g eq d (l ◂ i) = eq l d i
  graft-ext f g eq d (b ∙ as) = cong (_∙_ b) (grafts-ext f g eq (ar b) d as)

  grafts-ext : ∀ {m n} -> (f g : Sub m n) -> (∀ l d i -> f l d i ≡ g l d i) -> ∀ xs d t -> grafts {m} {n} f xs d t ≡ grafts {m} {n} g xs d t
  grafts-ext f g eq [] d t = refl
  grafts-ext f g eq (true ∷ xs) d (t , ts) = cong₂ _,_ (graft-ext f g eq (suc d) t) (grafts-ext f g eq xs d _)
  grafts-ext f g eq (false ∷ xs) d (t , ts) = cong₂ _,_ (graft-ext f g eq d t) (grafts-ext f g eq xs d _)

 mutual
  graft-∘ : ∀ {m n o} -> ∀ f g -> ∀ d t -> graft {n} {o} f d (graft {m} {n} g d t) ≡ graft {m} {o} (λ l d₁ x → graft f d₁ (g l d₁ x)) d t
  graft-∘ f g d (l ◂ i) = refl
  graft-∘ f g d (b ∙ as) = cong (_∙_ b) (grafts-∘ f g (ar b) d as)

  grafts-∘ : ∀ {m n o} -> ∀ f g -> ∀ xs d ts -> 
           grafts {n} {o} f xs d (grafts {m} {n} g xs d ts) ≡ grafts {m} {o} (λ l d₁ x → graft f d₁ (g l d₁ x)) xs d ts
  grafts-∘ f g [] d ts = refl
  grafts-∘ f g (true ∷ xs) d (t , ts) = cong₂ _,_ (graft-∘ f g (suc d) t) (grafts-∘ f g xs d ts)
  grafts-∘ f g (false ∷ xs) d (t , ts) = cong₂ _,_ (graft-∘ f g d t) (grafts-∘ f g xs d ts)