module stlc.term where
open import Data.Nat using (ℕ)
open import stlc.type public
open import stlc.monad
open import context (Type) public
ctxToType : Context → Type
ctxToType ∅ = unit
ctxToType (Γ , A) = ctxToType Γ × A
infix 3 _⊢_
infix 5 ƛ_
infixl 7 _·_
infix 9 `_
infix 9 `nat_
infix 9 snd_
infix 9 fst_
infixr 6 _⦂_
data _⊢_ : Context → Type → Set where
⟨⟩ : ∀ {Γ} → Γ ⊢ unit
`_ : ∀ {Γ A} → Γ ∋ A → Γ ⊢ A
_,_ : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A × B
fst_ : ∀ {Γ A B} → Γ ⊢ A × B → Γ ⊢ A
snd_ : ∀ {Γ A B} → Γ ⊢ A × B → Γ ⊢ B
ƛ_ : ∀ {Γ A B} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
_·_ : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
`nat_ : ∀ {Γ} → ℕ → Γ ⊢ nat
inl_ : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ A + B
inr_ : ∀ {Γ A B} → Γ ⊢ B → Γ ⊢ A + B
case_inl_inr_ : ∀ {Γ A B C} → Γ ⊢ A + B → Γ , A ⊢ C → Γ , B ⊢ C → Γ ⊢ C
[] : ∀ {Γ A} → Γ ⊢ list A
_⦂_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ list A → Γ ⊢ list A
it : ∀ {Γ A X} → Γ ⊢ X → Γ , (A × X) ⊢ X → Γ ⊢ list A → Γ ⊢ X
`let_`in_ : ∀ {Γ A B TA TB} → {ma : Monad {A} TA} → {mb : Monad {B} TB} → {s : SameMonad ma mb} → Γ ⊢ TA → Γ , A ⊢ TB → Γ ⊢ TB
return : ∀ {Γ A TA} → {m : Monad {A} TA} → Γ ⊢ A → Γ ⊢ TA
module Utils where
open import Data.Nat using (zero; suc; _<_; _≤?_; z≤n; s≤s)
open import Relation.Nullary.Decidable using (True; toWitness)
infix 10 #_
ctxLen : Context → ℕ
ctxLen ∅ = zero
ctxLen (Γ , _) = suc (ctxLen Γ)
ctxLookup : {Γ : Context} → {n : ℕ} → (p : n < ctxLen Γ) → Type
ctxLookup {(_ , A)} {zero} (s≤s z≤n) = A
ctxLookup {(Γ , _)} {(suc _)} (s≤s p) = ctxLookup p
count : ∀ {Γ} → {n : ℕ} → (p : n < ctxLen Γ) → Γ ∋ ctxLookup p
count {_ , _} {zero} (s≤s z≤n) = Z
count {Γ , _} {(suc _)} (s≤s p) = S (count p)
#_ : ∀ {Γ}
→ (n : ℕ)
→ {n∈Γ : True (suc n ≤? ctxLen Γ)}
→ Γ ⊢ ctxLookup (toWitness n∈Γ)
#_ x {n∈Γ} = ` count (toWitness n∈Γ)