{- Algorithmic typing rules of the surface language -}
module Surface.SurfaceTyping where

open import Data.Maybe
open import Data.List
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Syntax
open import Common.Utils
open import Common.Types
open import Surface.SurfaceSyntax

infix 4 _;_⊢ᴳ_⦂_

data _;_⊢ᴳ_⦂_ : Context  Label  Term  Type  Set where

  ⊢const :  {Γ gc ι} {k : rep ι} {}
      ------------------------------------ Const
     Γ ; gc ⊢ᴳ $ k of   ` ι of l 

  ⊢var :  {Γ gc A x}
     Γ  x  A
      --------------------- Var
     Γ ; gc ⊢ᴳ ` x  A

  ⊢lam :  {Γ gc pc A B N }
     (A  Γ) ; l pc ⊢ᴳ N  B
      --------------------------------------------------------- Lam
     Γ ; gc ⊢ᴳ ƛ⟦ pc  A ˙ N of    l pc  A  B of l 

  ⊢app :  {Γ gc gc′ A A′ B L M g p}
     Γ ; gc ⊢ᴳ L   gc′  A  B of g
     Γ ; gc ⊢ᴳ M  A′
     A′  A
     g  gc′
     gc  gc′
      ------------------------------------- App
     Γ ; gc ⊢ᴳ L · M at p  stamp B g

  ⊢if :  {Γ gc A B C L M N g p}
     Γ ; gc     ⊢ᴳ L  ` Bool of g
     Γ ; gc ⋎̃ g ⊢ᴳ M  A
     Γ ; gc ⋎̃ g ⊢ᴳ N  B
     A ∨̃ B  just C
      ------------------------------------------------- If
     Γ ; gc ⊢ᴳ if L then M else N at p  stamp C g

  ⊢ann :  {Γ gc M A A′ p}
     Γ ; gc ⊢ᴳ M  A′
     A′  A
      ---------------------------- Ann
     Γ ; gc ⊢ᴳ M  A at p  A

  ⊢let :  {Γ gc A B M N}
     Γ     ; gc ⊢ᴳ M  A
     A  Γ ; gc ⊢ᴳ N  B
      ------------------------------- Let
     Γ ; gc ⊢ᴳ `let M `in N  B

  ⊢ref :  {Γ gc M T g  p}
     Γ ; gc ⊢ᴳ M  T of g
     T of g  T of l 
     gc  l 
      --------------------------------------------------------- Ref
     Γ ; gc ⊢ᴳ ref⟦   M at p  Ref (T of l ) of l low

  ⊢deref :  {Γ gc M A g}
     Γ ; gc ⊢ᴳ M  (Ref A) of g
      -------------------------------- Deref
     Γ ; gc ⊢ᴳ ! M  stamp A g

  ⊢assign :  {Γ gc L M A T g  p}
     Γ ; gc ⊢ᴳ L  Ref (T of ) of g
     Γ ; gc ⊢ᴳ M  A
     A  T of 
     g  
     gc  
      --------------------------------------------- Assign
     Γ ; gc ⊢ᴳ L := M at p  ` Unit of l low