{- 2.0 -}

module Surface2.Syntax where

open import Data.List
open import Data.Bool renaming (Bool to 𝔹)

open import Syntax
open import Common.BlameLabels
open import Common.Types


data Op : Set where
  op-lam    : (g : Label) β†’ Type β†’ (β„“ : StaticLabel) β†’ Op
  op-app    : BlameLabel β†’ Op
  op-const  : βˆ€ {ΞΉ} β†’ rep ΞΉ β†’ StaticLabel β†’ Op
  op-if     : BlameLabel β†’ Op
  op-ann    : Type β†’ BlameLabel β†’ Op
  op-let    : Op
  op-ref    : StaticLabel β†’ BlameLabel β†’ Op
  op-deref  : BlameLabel β†’ Op
  op-assign : BlameLabel β†’ Op

sig : Op β†’ List Sig
sig (op-lam g A β„“)     = (Ξ½ β– ) ∷ []
sig (op-app p)         = β–  ∷ β–  ∷ []
sig (op-const k β„“)     = []
sig (op-if p)          = β–  ∷ β–  ∷ β–  ∷ []
sig (op-ann A p)       = β–  ∷ []
sig op-let             = β–  ∷ (Ξ½ β– ) ∷ []
sig (op-ref β„“ p)       = β–  ∷ []
sig (op-deref p)       = β–  ∷ []
sig (op-assign p)      = β–  ∷ β–  ∷ []

open Syntax.OpSig Op sig renaming (ABT to Term) hiding (plug; rename) public

infixl 7  _Β·_at_

pattern Ζ›_,_Λ™_of_ g A N β„“        = (op-lam g A β„“) β¦… cons (bind (ast N)) nil ⦆
pattern _Β·_at_ L M p             = (op-app p) β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern $_of_ k β„“                = (op-const k β„“) β¦… nil ⦆
pattern if_then_else_at_ L M N p = (op-if p) β¦… cons (ast L) (cons (ast M) (cons (ast N) nil)) ⦆
pattern _∢_at_ M A p             = (op-ann A p) β¦… cons (ast M) nil ⦆
pattern `let_`in_ M N            = op-let β¦… cons (ast M) (cons (bind (ast N)) nil) ⦆
pattern ref⟦_⟧_at_ β„“ M p         = (op-ref β„“ p) β¦… cons (ast M) nil ⦆
pattern !_at_ M p                = (op-deref p) β¦… cons (ast M) nil ⦆
pattern _:=_at_ L M p            = (op-assign p) β¦… cons (ast L) (cons (ast M) nil) ⦆