{-# OPTIONS --safe #-}
module Pat.Term where
open import Relation.Nullary using (¬_)
open import Function.Base using (id; _∘_)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) renaming (subst to transport)
open import Pat.Context
data Term : (n : ℕ) → Context n → Type n → Set
infix 4 Term
syntax Term n Γ A = Γ ⊢ A ^ n
infix 4 _⊩_
infix 4 _⊩[_⊢_^_]
infix 4 _∣_⊩_↝_
infix 4 _∣_⊩[_⊢_^_]↝_
infixl 5 _,_
infixl 5 _++ˢ_
data _⊩[_⊢_^_] Γ′ {m} (Δ : Context m) (A : Type m) (m≥n : m ≥‴ n) : Set where
term
: (e : Γ′ ↾≥ m≥n ++ Δ ⊢ A ^ m)
→ Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
var
: (x : Γ′ ∋[ Δ ⊢ A ^ m≥n ])
→ Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
data _⊩_ (Γ′ : Context n) : Context n → Set where
∅ : Γ′ ⊩ ∅
_,_ : (σ : Γ′ ⊩ Γ) → (item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ ,[ Δ ⊢ A ^ m≥n ]
lookup : Γ′ ⊩ Γ → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
lookup (σ , e) Z = e
lookup (σ , e) (S x) = lookup σ x
_++ˢ_ : Γ′ ⊩ Γ → Γ′ ⊩ Δ → Γ′ ⊩ Γ ++ Δ
σ ++ˢ ∅ = σ
σ ++ˢ (σ′ , item) = σ ++ˢ σ′ , item
Subst : Context n → Context n → Set
Subst Γ Γ′ = Γ′ ⊩ Γ
variable
Π Π′ Π₁ Π₂ Π₃ : Context n
infix 4 Pattern
syntax Pattern n Γ Δ A Π = Γ ∣ Δ ⊢ A ^ n ↝ Π
data Pattern : (n : ℕ) → Context n → Context n → Type n → Context n → Set
data _∣_⊩[_⊢_^_]↝_ (Γ′ Δ : Context n) {m} (Δ′ : Context m) (A : Type m) (m≥n : m ≥‴ n) : (Π : Context m) → Set where
term
: (p : Γ′ ↾≥ m≥n ∣ Δ ↾≥ m≥n ++ Δ′ ⊢ A ^ m ↝ Π)
→ Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π
var
: (x : Γ′ ++ Δ ∋[ Δ′ ⊢ A ^ m≥n ])
→ Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ ∅
data _∣_⊩_↝_ (Γ′ : Context n) (Δ : Context n) : Context n → (Π : Context n) → Set where
∅ : Γ′ ∣ Δ ⊩ ∅ ↝ ∅
_,_
: (π : Γ′ ∣ Δ ⊩ Γ ↝ Π₁)
→ (item : Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π₂)
→ Γ′ ∣ Δ ⊩ Γ ,[ Δ′ ⊢ A ^ m≥n ] ↝ Π₁ ++ inject≥ m≥n Π₂
data Pattern where
`pat
: Γ ∣ Δ ⊢ A ^ n ↝ ∅ ,[ Δ ⊢ A ^ ≤‴-refl ]
`_`with₁_
: (x : Γ ∋[ Δ′ ⊢ A ^ ≤‴-refl ])
→ (σ : Γ ++ Δ ⊩ Δ′)
→ Γ ∣ Δ ⊢ A ^ n ↝ ∅
`_`with₂_
: (x : Δ ∋[ Δ′ ⊢ A ^ ≤‴-refl ])
→ (π : Γ ∣ Δ ⊩ Δ′ ↝ Π)
→ Γ ∣ Δ ⊢ A ^ n ↝ Π
`true
: Γ ∣ Δ ⊢ `Bool ^ n ↝ ∅
`false
: Γ ∣ Δ ⊢ `Bool ^ n ↝ ∅
`if_`then_`else_
: (p₁ : Γ ∣ Δ ⊢ `Bool ^ n ↝ Π₁)
→ (p₂ : Γ ∣ Δ ⊢ A ^ n ↝ Π₂)
→ (p₃ : Γ ∣ Δ ⊢ A ^ n ↝ Π₃)
→ Γ ∣ Δ ⊢ A ^ n ↝ Π₁ ++ Π₂ ++ Π₃
`λ⟨_⟩_
: ∀ Δ′
→ (p : Γ ∣ Δ ,[ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n ↝ Π)
→ Γ ∣ Δ ⊢ [ Δ′ ⊢ A ]⇒ B ^ n ↝ Π
_·_
: (p₁ : Γ ∣ Δ ⊢ [ Δ′ ⊢ A ]⇒ B ^ n ↝ Π₁)
→ (p₂ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ A ^ n ↝ Π₂)
→ Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++ Π₂
⟨_⟩
: (p : Γ ↾ ∣ Δ ↾ ⊢ A ^ suc n ↝ Π)
→ Γ ∣ Δ ⊢ ◯ A ^ n ↝ inject₁ Π
`let⟨_⟩
: ∀ Δ′
→ (p₁ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ ◯ A ^ n ↝ Π₁)
→ (p₂ : Γ ∣ Δ ,[ Δ′ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n ↝ Π₂)
→ Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++ Π₂
`wrap : ∀ Δ′
→ (e : Γ ∣ Δ ++ inject₁ Δ′ ⊢ A ^ n ↝ Π)
→ Γ ∣ Δ ⊢ Δ′ ▷ A ^ n ↝ Π
`letwrap : ∀ Δ′
→ (e₁ : Γ ∣ Δ ⊢ Δ′ ▷ A ^ n ↝ Π₁)
→ (e₂ : Γ ∣ Δ ,[ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n ↝ Π₂)
→ Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++ Π₂
`iflet⟨_⟩
: ∀ Δ′
→ (p : Γ ↾ ++ (Δ ↾) ∣ Δ′ ⊢ A ^ suc n ↝ Π)
→ (p₁ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ ◯ A ^ n ↝ Π₁)
→ (p₂ : Γ ∣ Δ ++ inject₁ Π ⊢ B ^ n ↝ Π₂)
→ (p₃ : Γ ∣ Δ ⊢ B ^ n ↝ Π₃)
→ Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++ Π₂ ++ Π₃
`rewritȩ
: (p : Γ ↾ ++ (Δ ↾) ∣ ∅ ⊢ A ^ suc n ↝ Π)
→ (p₁ : Γ ∣ Δ ++ inject₁ Π ⊢ ◯ A ^ n ↝ Π₁)
→ (p₂ : Γ ∣ Δ ⊢ ◯ B ^ n ↝ Π₂)
→ Γ ∣ Δ ⊢ ◯ B ^ n ↝ Π₁ ++ Π₂
infix 5 `λ⟨_⟩_
infixl 7 _·_
infixr 7 `if_`then_`else_
infix 9 `_`with_
data Term where
`_`with_
: (x : Γ ∋[ Δ ⊢ A ^ ≤‴-refl ])
→ (σ : Γ ⊩ Δ)
→ Γ ⊢ A ^ n
`true
: Γ ⊢ `Bool ^ n
`false
: Γ ⊢ `Bool ^ n
`if_`then_`else_
: (e₁ : Γ ⊢ `Bool ^ n)
→ (e₂ : Γ ⊢ A ^ n)
→ (e₃ : Γ ⊢ A ^ n)
→ Γ ⊢ A ^ n
`λ⟨_⟩_
: ∀ Δ
→ (e : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n
_·_
: (e₁ : Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n)
→ (e₂ : Γ ++ inject₁ Δ ⊢ A ^ n)
→ Γ ⊢ B ^ n
⟨_⟩
: (e : Γ ↾ ⊢ A ^ suc n)
→ Γ ⊢ ◯ A ^ n
`let⟨_⟩ : ∀ Δ
→ (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
→ (e₂ : Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ B ^ n
`wrap : ∀ Δ
→ (e : Γ ++ inject₁ Δ ⊢ A ^ n)
→ Γ ⊢ Δ ▷ A ^ n
`letwrap : ∀ Δ
→ (e₁ : Γ ⊢ Δ ▷ A ^ n)
→ (e₂ : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ B ^ n
`iflet⟨_⟩ : ∀ Δ
→ (p : Γ ↾ ∣ Δ ⊢ A ^ suc n ↝ Π)
→ (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
→ (e₂ : Γ ++ inject₁ Π ⊢ B ^ n)
→ (e₃ : Γ ⊢ B ^ n)
→ Γ ⊢ B ^ n
`rewritȩ
: (p : Γ ↾ ∣ ∅ ⊢ A ^ suc n ↝ Π)
→ (e1 : Γ ++ inject₁ Π ⊢ ◯ A ^ n)
→ (e2 : Γ ⊢ ◯ B ^ n)
→ Γ ⊢ ◯ B ^ n
transportContext : Γ ≡ Γ′ → Term n Γ A → Term n Γ′ A
transportContext refl e = e
transportContextₚ : Γ ≡ Γ′ → Γ ∣ Δ ⊢ A ^ n ↝ Π → Γ′ ∣ Δ ⊢ A ^ n ↝ Π
transportContextₚ refl p = p
rename : Rename Γ Γ′ → Term n Γ A → Term n Γ′ A
renameSubst : Rename Γ Γ′ → Subst Δ Γ → Subst Δ Γ′
renamePattern : Rename Γ Γ′ → Pattern n Γ Δ A Π → Pattern n Γ′ Δ A Π
renameSubstPattern : Rename Γ Γ′ → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π
rename ρ (` x `with σ) = ` ρ x `with renameSubst ρ σ
rename ρ `true = `true
rename ρ `false = `false
rename ρ (`if e `then e₁ `else e₂) = `if (rename ρ e) `then (rename ρ e₁) `else (rename ρ e₂)
rename ρ (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ (rename (ext ρ) e)
rename ρ (e₁ · e₂) = rename ρ e₁ · rename (ext++ _ ρ) e₂
rename ρ ⟨ e ⟩ = ⟨ rename (ext↾ ρ) e ⟩
rename ρ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext ρ) e₂)
rename ρ (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) = `iflet⟨ Δ ⟩ (renamePattern (ext↾ ρ) p) (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext++ (inject₁ _) ρ) e₂) (rename ρ e₃)
rename ρ (`wrap Δ e) = `wrap Δ (rename (ext++ (inject₁ Δ) ρ) e)
rename ρ (`letwrap Δ e₁ e₂) = `letwrap Δ (rename ρ e₁) (rename (ext ρ) e₂)
rename ρ (`rewritȩ p e₁ e₂) = `rewritȩ (renamePattern (ext↾ ρ) p) (rename (ext++ _ ρ) e₁) (rename ρ e₂)
renameSubst ρ ∅ = ∅
renameSubst ρ (_,_ {Δ = Δ} {m≥n = m≥n} σ (term e)) = renameSubst ρ σ , term (rename (ext++ Δ (ext↾≥ m≥n ρ)) e)
renameSubst ρ (σ , var x) = renameSubst ρ σ , var (ρ x)
renamePattern ρ `pat = `pat
renamePattern ρ (` x `with₁ σ) = ` ρ x `with₁ renameSubst (ext++ _ ρ) σ
renamePattern ρ (` x `with₂ π) = ` x `with₂ renameSubstPattern ρ π
renamePattern ρ `true = `true
renamePattern ρ `false = `false
renamePattern ρ (`if p₁ `then p₂ `else p₃)
= `if (renamePattern ρ p₁) `then (renamePattern ρ p₂) `else (renamePattern ρ p₃)
renamePattern ρ (`λ⟨ Δ′ ⟩ p) = `λ⟨ Δ′ ⟩ renamePattern ρ p
renamePattern ρ (p₁ · p₂) = renamePattern ρ p₁ · renamePattern (ext++ _ ρ) p₂
renamePattern ρ (⟨ p ⟩) = ⟨ renamePattern (ext↾ ρ) p ⟩
renamePattern ρ (`let⟨ Δ ⟩ p₁ p₂) = `let⟨ Δ ⟩ (renamePattern ρ p₁) (renamePattern ρ p₂)
renamePattern ρ (`iflet⟨ Δ′ ⟩ p e₁ e₂ e₃) = `iflet⟨ Δ′ ⟩ (renamePattern (ext++ _ (ext↾ ρ)) p) (renamePattern ρ e₁) (renamePattern ρ e₂) (renamePattern ρ e₃)
renamePattern ρ (`wrap Δ p) = `wrap Δ (renamePattern (ext++ _ ρ) p)
renamePattern ρ (`letwrap Δ p₁ p₂) = `letwrap Δ (renamePattern (ext++ _ ρ) p₁) (renamePattern ρ p₂)
renamePattern ρ (`rewritȩ p e₁ e₂) = `rewritȩ (renamePattern (ext++ _ (ext↾ ρ)) p) (renamePattern (ext++ _ ρ) e₁) (renamePattern ρ e₂)
renameSubstPattern ρ ∅ = ∅
renameSubstPattern ρ (_,_ {m≥n = m≥n} π (term p)) = renameSubstPattern ρ π , term (renamePattern (ext++ _ (ext↾≥ m≥n ρ)) p)
renameSubstPattern ρ (π , var x) = renameSubstPattern ρ π , var ((ext++ _ ρ) x)
lift : Rename Γ Γ′ → Subst Γ Γ′
lift {Γ = ∅} ρ = ∅
lift {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} ρ = lift (ρ ∘ S) , var (ρ Z)
exts : Subst Γ Γ′ → Subst (Γ ,[ Δ ⊢ A ^ m≥n ]) (Γ′ ,[ Δ ⊢ A ^ m≥n ])
exts {Δ = Δ} {m≥n = m≥n} σ = renameSubst S σ , var Z
exts++ : ∀ Δ → Subst Γ Γ′ → Subst (Γ ++ Δ) (Γ′ ++ Δ)
exts++ ∅ σ = σ
exts++ (Δ ,[ _ ⊢ _ ^ _ ]) σ = exts (exts++ Δ σ)
exts↾ : Subst Γ Γ′ → Subst (Γ ↾) (Γ′ ↾)
exts↾ ∅ = ∅
exts↾ (_,_ {m≥n = ≤‴-refl} σ (term e)) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = exts↾ σ , term e
exts↾ (_,_ {m≥n = ≤‴-refl} σ (var x)) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ (var x)) = exts↾ σ , var (∋-↾⁺ x)
exts↾≥ : (m≥n : m ≥‴ n) → Subst Γ Γ′ → Subst (Γ ↾≥ m≥n) (Γ′ ↾≥ m≥n)
exts↾≥ ≤‴-refl σ = σ
exts↾≥ (≤‴-step sm≥n) σ = exts↾≥ sm≥n (exts↾ σ)
⊩-↾⁻ : Γ ↾ ⊩ Π → Γ ⊩ inject₁ Π
⊩-↾⁻ ∅ = ∅
⊩-↾⁻ (σ , term e) = ⊩-↾⁻ σ , term e
⊩-↾⁻ (σ , var x) = (⊩-↾⁻ σ) , var (∋-↾⁻ x)
⊩-↾⁺ : Γ ⊩ inject₁ Π → Γ ↾ ⊩ Π
⊩-↾⁺ {Π = ∅} ∅ = ∅
⊩-↾⁺ {Π = Π ,[ _ ⊢ _ ^ _ ]} (σ , term e) = ⊩-↾⁺ σ , term e
⊩-↾⁺ {Π = Π ,[ _ ⊢ _ ^ _ ]} (σ , var x) = ⊩-↾⁺ σ , var (∋-↾⁺ x)
⊩-↾≥⁻ : ∀ m≥n → Γ ↾≥ m≥n ⊩ Π → Γ ⊩ inject≥ m≥n Π
⊩-↾≥⁻ ≤‴-refl σ = σ
⊩-↾≥⁻ (≤‴-step m≥n) σ = ⊩-↾⁻ (⊩-↾≥⁻ m≥n σ)
⊩-↾≥⁺ : ∀ (m≥n : m ≥‴ n) → Γ ⊩ inject≥ m≥n Π → Γ ↾≥ m≥n ⊩ Π
⊩-↾≥⁺ ≤‴-refl σ = σ
⊩-↾≥⁺ (≤‴-step m≥n) σ = ⊩-↾≥⁺ m≥n (⊩-↾⁺ σ)