Pat.agda

module Pat (BaseType : Set) where

data Ty : Set where
  ι   : BaseType -> Ty
  _⟶_ : Ty -> Ty -> Ty

data Bwd (A : Set) : Set where
  •   : Bwd A
  _◄_ : Bwd A -> A -> Bwd A

infixl 30 _◄_

Ctx = Bwd Ty

data Take {A : Set} : Bwd A -> A -> Bwd A -> Set where
  hd : forall {x xs} -> Take (xs ◄ x) x xs
  tl : forall {x y xs ys} -> Take xs x ys -> Take (xs ◄ y) x (ys ◄ y)

data Pat : Ctx -> Ctx -> Ty -> Ctx -> Set

data Pats : Ctx -> Ty -> Ctx -> Ty -> Set where
  ε : forall {Θ τ} -> Pats Θ τ Θ τ
  _,_ : forall {Θ₁ Θ₂ Θ₃ ρ σ τ} ->
        Pat • Θ₁ ρ Θ₂ -> Pats Θ₂ σ Θ₃ τ ->
        Pats Θ₁ (ρ ⟶ σ) Θ₃ τ

data Pat where
  ƛ    : forall {Δ Θ Θ' σ τ} -> Pat (Δ ◄ σ) Θ τ Θ' ->
         Pat Δ Θ (σ ⟶ τ) Θ'
  _[_] : forall {Θ Θ' Δ σ τ} ->
         Take Θ σ Θ' -> Pats Δ σ • τ -> Pat Δ Θ τ Θ'