import Parametric.Syntax.Type as Type
module Parametric.Syntax.Term
(Base : Type.Structure)
where
open Type.Structure Base
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import Data.Unit
open import Data.Sum
Structure : Set₁
Structure = Context → Type → Set
module Structure (Const : Structure) where
import Base.Data.DependentList as DependentList
open DependentList public using (∅ ; _•_)
open DependentList
data Term
(Γ : Context) :
(τ : Type) → Set
Terms : Context → Context → Set
Terms Γ = DependentList (Term Γ)
data Term Γ where
const : ∀ {Σ τ} →
(c : Const Σ τ) →
(args : Terms Γ Σ) →
Term Γ τ
var : ∀ {τ} →
(x : Var Γ τ) →
Term Γ τ
app : ∀ {σ τ}
(s : Term Γ (σ ⇒ τ)) →
(t : Term Γ σ) →
Term Γ τ
abs : ∀ {σ τ}
(t : Term (σ • Γ) τ) →
Term Γ (σ ⇒ τ)
FV : ∀ {τ Γ} → Term Γ τ → Vars Γ
FV-terms : ∀ {Σ Γ} → Terms Γ Σ → Vars Γ
FV (const ι ts) = FV-terms ts
FV (var x) = singleton x
FV (abs t) = tail (FV t)
FV (app s t) = FV s ∪ FV t
FV-terms ∅ = none
FV-terms (t • ts) = FV t ∪ FV-terms ts
closed? : ∀ {τ Γ} → (t : Term Γ τ) → (FV t ≡ none) ⊎ ⊤
closed? t = empty? (FV t)
weaken : ∀ {Γ₁ Γ₂ τ} →
(Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
Term Γ₁ τ →
Term Γ₂ τ
weaken-terms : ∀ {Γ₁ Γ₂ Σ} →
(Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
Terms Γ₁ Σ →
Terms Γ₂ Σ
weaken Γ₁≼Γ₂ (const c ts) = const c (weaken-terms Γ₁≼Γ₂ ts)
weaken Γ₁≼Γ₂ (var x) = var (weaken-var Γ₁≼Γ₂ x)
weaken Γ₁≼Γ₂ (app s t) = app (weaken Γ₁≼Γ₂ s) (weaken Γ₁≼Γ₂ t)
weaken Γ₁≼Γ₂ (abs {σ} t) = abs (weaken (keep σ • Γ₁≼Γ₂) t)
weaken-terms Γ₁≼Γ₂ ∅ = ∅
weaken-terms Γ₁≼Γ₂ (t • ts) = weaken Γ₁≼Γ₂ t • weaken-terms Γ₁≼Γ₂ ts
weaken₁ : ∀ {Γ σ τ} →
Term Γ τ → Term (σ • Γ) τ
weaken₁ t = weaken (drop _ • ≼-refl) t
weaken₂ : ∀ {Γ α β τ} →
Term Γ τ → Term (α • β • Γ) τ
weaken₂ t = weaken (drop _ • drop _ • ≼-refl) t
weaken₃ : ∀ {Γ α β γ τ} →
Term Γ τ → Term (α • β • γ • Γ) τ
weaken₃ t = weaken (drop _ • drop _ • drop _ • ≼-refl) t
app₂ : ∀ {Γ α β γ} →
Term Γ (α ⇒ β ⇒ γ) →
Term Γ α → Term Γ β → Term Γ γ
app₂ f x = app (app f x)
app₃ : ∀ {Γ α β γ δ} →
Term Γ (α ⇒ β ⇒ γ ⇒ δ) →
Term Γ α → Term Γ β → Term Γ γ → Term Γ δ
app₃ f x = app₂ (app f x)
app₄ : ∀ {Γ α β γ δ ε} →
Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε) →
Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
Term Γ ε
app₄ f x = app₃ (app f x)
app₅ : ∀ {Γ α β γ δ ε ζ} →
Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ) →
Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
Term Γ ε → Term Γ ζ
app₅ f x = app₄ (app f x)
app₆ : ∀ {Γ α β γ δ ε ζ η} →
Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ ⇒ η) →
Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
Term Γ ε → Term Γ ζ → Term Γ η
app₆ f x = app₅ (app f x)
UncurriedTermConstructor : (Γ Σ : Context) (τ : Type) → Set
UncurriedTermConstructor Γ Σ τ = Terms Γ Σ → Term Γ τ
uncurriedConst : ∀ {Σ τ} → Const Σ τ → ∀ {Γ} → UncurriedTermConstructor Γ Σ τ
uncurriedConst constant = const constant
CurriedTermConstructor : (Γ Σ : Context) (τ : Type) → Set
CurriedTermConstructor Γ ∅ τ′ = Term Γ τ′
CurriedTermConstructor Γ (τ • Σ) τ′ = Term Γ τ → CurriedTermConstructor Γ Σ τ′
curryTermConstructor : ∀ {Σ Γ τ} → UncurriedTermConstructor Γ Σ τ → CurriedTermConstructor Γ Σ τ
curryTermConstructor {∅} k = k ∅
curryTermConstructor {τ • Σ} k = λ t → curryTermConstructor (λ ts → k (t • ts))
curriedConst : ∀ {Σ τ} → Const Σ τ → ∀ {Γ} → CurriedTermConstructor Γ Σ τ
curriedConst constant = curryTermConstructor (uncurriedConst constant)
abs₁ :
∀ {Γ τ₁ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → (x : Term Γ′ τ₁) → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ))
abs₁ {Γ} {τ₁} = λ f → abs (f {Γ≼Γ′ = drop τ₁ • ≼-refl} (var this))
abs₂ :
∀ {Γ τ₁ τ₂ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ₂ ⇒ τ))
abs₂ f =
abs₁ (λ {_} {Γ≼Γ′} x₁ →
abs₁ (λ {_} {Γ′≼Γ′₁} →
f {Γ≼Γ′ = ≼-trans Γ≼Γ′ Γ′≼Γ′₁} (weaken Γ′≼Γ′₁ x₁)))
abs₃ :
∀ {Γ τ₁ τ₂ τ₃ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τ₃ → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ₂ ⇒ τ₃ ⇒ τ))
abs₃ f =
abs₁ (λ {_} {Γ≼Γ′} x₁ →
abs₂ (λ {_} {Γ′≼Γ′₁} →
f {Γ≼Γ′ = ≼-trans Γ≼Γ′ Γ′≼Γ′₁} (weaken Γ′≼Γ′₁ x₁)))
abs₄ :
∀ {Γ τ₁ τ₂ τ₃ τ₄ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τ₃ → Term Γ′ τ₄ → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ₂ ⇒ τ₃ ⇒ τ₄ ⇒ τ))
abs₄ f =
abs₁ (λ {_} {Γ≼Γ′} x₁ →
abs₃ (λ {_} {Γ′≼Γ′₁} →
f {Γ≼Γ′ = ≼-trans Γ≼Γ′ Γ′≼Γ′₁} (weaken Γ′≼Γ′₁ x₁)))
abs₅ :
∀ {Γ τ₁ τ₂ τ₃ τ₄ τ₅ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τ₃ → Term Γ′ τ₄ → Term Γ′ τ₅ → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ₂ ⇒ τ₃ ⇒ τ₄ ⇒ τ₅ ⇒ τ))
abs₅ f =
abs₁ (λ {_} {Γ≼Γ′} x₁ →
abs₄ (λ {_} {Γ′≼Γ′₁} →
f {Γ≼Γ′ = ≼-trans Γ≼Γ′ Γ′≼Γ′₁} (weaken Γ′≼Γ′₁ x₁)))
abs₆ :
∀ {Γ τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ τ} →
(∀ {Γ′} → {Γ≼Γ′ : Γ ≼ Γ′} → Term Γ′ τ₁ → Term Γ′ τ₂ → Term Γ′ τ₃ → Term Γ′ τ₄ → Term Γ′ τ₅ → Term Γ′ τ₆ → Term Γ′ τ) →
(Term Γ (τ₁ ⇒ τ₂ ⇒ τ₃ ⇒ τ₄ ⇒ τ₅ ⇒ τ₆ ⇒ τ))
abs₆ f =
abs₁ (λ {_} {Γ≼Γ′} x₁ →
abs₅ (λ {_} {Γ′≼Γ′₁} →
f {Γ≼Γ′ = ≼-trans Γ≼Γ′ Γ′≼Γ′₁} (weaken Γ′≼Γ′₁ x₁)))