Skip to content

Instantly share code, notes, and snippets.

@L-TChen
Created February 26, 2019 14:43
Show Gist options
  • Save L-TChen/ccb7f86f43930b0140913334ec1965b9 to your computer and use it in GitHub Desktop.
Save L-TChen/ccb7f86f43930b0140913334ec1965b9 to your computer and use it in GitHub Desktop.
Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment