Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables

Base.agda

open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])

module Term.Base (Atom : Set)(_≟A_ : Decidable {A = Atom} (_≡_)) where

open import Relation.Nullary public
open import Data.Nat renaming (_≟_ to _≟ℕ_) 
open import Data.Fin renaming (_≟_ to _≟F_) hiding (_+_; compare)
open import Data.Product hiding (map)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Function
--open import Size
open import Agda.Builtin.Size

open import Distinct
open Permutation Atom _≟A_

Atoms : Set
Atoms = List Atom

data RawTm (n : ℕ) (xs : Atoms) ⦃ _ : Dist xs ⦄ : ∀ {s : Size} → Set where
  bvar_ : ∀ {s} (i : Fin n)           → RawTm n xs {↑ s}
  fvar_ : ∀ {s} x ⦃ x∈xs : x ∈ xs ⦄   → RawTm n xs {↑ s}
  _·_   : ∀ {s₁} (t₁ : RawTm n xs {s₁}) {s₂} (t₂ : RawTm n xs {s₂}) → RawTm n xs {↑ (s₁ ⊔ˢ s₂)}
  ƛ_    : ∀ {s} (t : RawTm (suc n) xs {s}) → RawTm n xs {↑ s}

infix  8  fvar_
infix  8  bvar_
infixl 15 _·_
infixr 15 ƛ_

data _#[_]_ (x : Atom) {n xs} ⦃ _ : Dist xs ⦄ : ∀ s → RawTm n xs {s} → Set where
  instance
    fvar_ : ∀ {y s} ⦃ _ : y ∈ xs ⦄ → x ≢ y         → x #[ ↑ s ] (fvar y)
    bvar_ : ∀ {s}                    (i : Fin n)   → x #[ ↑ s ] (bvar i)
    _·_   : ∀ {s₁ t₁ s₂ t₂} → x #[ s₁ ] t₁ → x #[ s₂ ] t₂
                            → x #[ ↑ (s₁ ⊔ˢ s₂) ] _·_ {s₁ = s₁} t₁ {s₂} t₂
    ƛ_    : ∀ {s t}                → x #[ s ] t         → x #[ ↑ s ] ƛ t 
infix 5 _#[_]_

x∉xs⇒x#t : ∀ {s x xs n} ⦃ _ : Dist xs ⦄ → (t : RawTm n xs {s}) → x ∉ xs → x #[ s ] t 
x∉xs⇒x#t (fvar_ y ⦃ y∈xs ⦄) x∉xs    = fvar λ { refl → x∉xs y∈xs }
x∉xs⇒x#t {s} (bvar i) x∉xs          = bvar i
x∉xs⇒x#t (_·_ {s₁} t₁ {s₂} t₂) x∉xs =
  _·_ {s₁ = s₁} {s₂ = s₂} (x∉xs⇒x#t t₁ x∉xs) (x∉xs⇒x#t t₂ x∉xs)
x∉xs⇒x#t (ƛ t) x∉xs    = ƛ x∉xs⇒x#t t x∉xs

_⁺ : ∀ {s n xs} ⦃ _ : Dist xs ⦄ → RawTm n xs {s} → RawTm (suc n) xs {s}
(bvar i) ⁺ = bvar (inject₁ i)
(fvar x) ⁺ = fvar x
(_·_ t₁ {s₂} t₂) ⁺ = _·_ (t₁ ⁺) {s₂} (t₂ ⁺)
(ƛ t) ⁺ = ƛ (t ⁺)

Tm : ∀ (xs : Atoms) ⦃ _ : Dist xs ⦄ {s} → Set
Tm xs {s} = RawTm 0 xs {s}

⟦_↦_⟧_ : ∀ {s} n x {xs} {x∉xs : x ∉ xs} ⦃ p : Dist xs ⦄
       → RawTm (suc n) xs {s} → RawTm n (x ∷ xs) ⦃ x∉xs ∷ p ⦄ {s}
⟦ n ↦ x ⟧ (bvar i) with n ≟ℕ (toℕ i)
... | yes p = fvar_ x ⦃ here refl ⦄ 
... | no ¬p = bvar (lower₁ i ¬p)
⟦ n ↦ x ⟧ (fvar y) = fvar y
⟦ n ↦ x ⟧ (_·_ u₁ {s₂} u₂) = _·_ (⟦ n ↦ x ⟧ u₁) {s₂} (⟦ n ↦ x ⟧ u₂) 
⟦ n ↦ x ⟧ (ƛ u)   = ƛ ⟦ suc n ↦ x ⟧ u 

⟦_↤_⟧_ : ∀ {s} {xs ys : Atoms} n (x : Atom) ⦃ p : Dist (xs ++ x ∷ ys) ⦄
       → RawTm n (xs ++ x ∷ ys) {s} → RawTm (suc n) (xs ++ ys) ⦃ Dist-rm xs p ⦄ {s}
⟦ k ↤ x ⟧ (bvar i) = bvar (inject₁ i)
⟦ k ↤ x ⟧ (fvar y) with x ≟A y
⟦ k ↤ x ⟧ (fvar y) | yes _ = bvar (fromℕ k)
⟦ k ↤ x ⟧ (fvar_ y ⦃ y∈xs++x∷ys ⦄) | no x≢y =
  fvar_ y ⦃ ∈-++-somewhere {z = x} (λ y≡x → x≢y (sym y≡x)) y∈xs++x∷ys ⦄
⟦ k ↤ x ⟧ (_·_ t₁ {s₂} t₂) = _·_ (⟦ k ↤ x ⟧ t₁) {s₂} (⟦ k ↤ x ⟧ t₂)
⟦ k ↤ x ⟧ (ƛ t)   = ƛ ⟦ suc k ↤ x ⟧ t

Tm-weaken : ∀ {s x xs n} ⦃ p : Dist xs ⦄ → (x∉xs : x ∉ xs)
            → RawTm n xs {s} → RawTm n (x ∷ xs) ⦃ x∉xs ∷ p ⦄ {s}
Tm-weaken x∉xs (fvar_ y ⦃ x∈xs ⦄) = fvar_ y ⦃ there x∈xs ⦄ 
Tm-weaken x∉xs (bvar i) = bvar i
Tm-weaken x∉xs (_·_ t₁ {s₂} t₂) = _·_ (Tm-weaken x∉xs t₁) {s₂} (Tm-weaken x∉xs t₂)
Tm-weaken x∉xs (ƛ t)    = ƛ Tm-weaken x∉xs t

Tm-perm : ∀ {a b s n xs} ⦃ p : Dist xs ⦄ 
        → RawTm n xs {s}
        → RawTm n (map ⦅ a · b ⦆_ xs) ⦃ perm-dist p ⦄ {s}
Tm-perm {a} {b} (fvar_ x ⦃ x∈xs ⦄) = fvar_ (⦅ a · b ⦆  x)   ⦃ map-perm-∈′ x∈xs ⦄ 
Tm-perm (bvar i)         = bvar i
Tm-perm (_·_ t₁ {s₂} t₂) = _·_ (Tm-perm t₁) {s₂} (Tm-perm t₂)
Tm-perm (ƛ t)            = ƛ Tm-perm t

module _ (fresh-atom-gen : ∀ xs → Σ[ x ∈ Atom ] x ∉ xs) where
  fvars : ∀ {xs} ⦃ _ : Dist xs ⦄ → {s : Size} → Tm xs {s} → Atoms
  fvars (bvar ())
  fvars (fvar x) = x ∷ []
  fvars {xs} .{↑ (s₁ ⊔ˢ s₂)} (_·_ {s₁} t₁ {s₂} t₂) =
    fvars {xs} {s₁} t₁ ++ fvars {xs} {s₂} t₂
  fvars {xs} ⦃ p ⦄ (ƛ_ {s} t) with fresh-atom-gen xs
  ... | (z , z∉xs) =
    fvars ⦃ Dist-ins [] z p z∉xs  ⦄ {s} (⟦ 0 ↦ z ⟧ t)

  [_/_] : ∀ {xs ys} ⦃ p : Dist xs ⦄ ⦃ _ : Dist ys ⦄ 
        → Tm ys → (x : Atom) {x∉xs : x ∉ xs}
        → {s : Size} → Tm (x ∷ xs) ⦃ Dist-ins [] x p x∉xs ⦄ {s}
        → Tm ys
  [ u / x ] (bvar ())
  [ u / x ] (fvar y) with x ≟A y
  ... | yes p = {!!}
  ... | no ¬p = {!!}
  [ u / x ] (t₁ · t₂) = {!!} -- [ u / x ] t₁ · [ u / x ] t₂
  [_/_] {xs} u x (ƛ t) with fresh-atom-gen xs
  ... | (y , y∉xs) = {!⟦ 0 ↦ y ⟧ t!} -- ƛ [ u ⁺ / x ] t