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
--- PRODUCT ---
  _,_ :  {Γ A B}  Γ  A  Γ  B  Γ  A × B
  fst_ :  {Γ A B}  Γ  A × B  Γ  A
  snd_ :  {Γ A B}  Γ  A × B  Γ  B
--- EXPONENTIAL ---
  ƛ_  :  {Γ A B}  Γ , A  B  Γ  A  B
  _·_ :  {Γ A B}  Γ  A  B  Γ  A  Γ  B
--- NATURAL NUMBERS ---
  `nat_ :  {Γ}    Γ  nat
--- COPRODUCT ---
  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
--- LIST OBJECT ---
  [] :  {Γ A}  Γ  list A
  _⦂_ :  {Γ A}  Γ  A  Γ  list A  Γ  list A
  it :  {Γ A X}  Γ  X  Γ , (A × X)  X  Γ  list A  Γ  X
--- MONAD ---
  `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∈Γ)