open import Common.Types

module CC.CCSyntax (Cast_β‡’_ : Type β†’ Type β†’ Set) where

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

open import Syntax
open import Common.BlameLabels
open import Memory.Addr
open import CC.Errors public


data Op : Set where
  op-addr         : (a : Addr) β†’ (β„“ : StaticLabel) β†’ Op
  op-lam          : (pc : StaticLabel) β†’ Type β†’ (β„“ : StaticLabel) β†’ Op
  op-app          : Op
  op-const        : βˆ€ {ΞΉ} β†’ rep ΞΉ β†’ StaticLabel β†’ Op
  op-if           : Type β†’ Op
  op-let          : Op
  op-ref          : StaticLabel β†’ Op
  op-ref?         : StaticLabel β†’ Op
  op-refβœ“         : StaticLabel β†’ Op
  op-deref        : Op
  op-assign       : Op
  op-assign?      : Op
  op-assignβœ“      : Op
  op-cast         : βˆ€ {A B} β†’ Cast A β‡’ B β†’ Op
  op-prot         : StaticLabel β†’ Op
  op-cast-pc      : Label β†’ Op
  op-error        : Error β†’ Op
  {- Terms that only appear in erasure -}
  op-opaque       : Op

sig : Op β†’ List Sig
sig (op-addr a β„“)      = []
sig (op-lam pc A β„“)    = (Ξ½ β– ) ∷ []
sig op-app             = β–  ∷ β–  ∷ []
sig (op-const k β„“)     = []
sig (op-if A)          = β–  ∷ β–  ∷ β–  ∷ []
sig op-let             = β–  ∷ (Ξ½ β– ) ∷ []
sig (op-ref  β„“)        = β–  ∷ []
sig (op-ref? β„“)        = β–  ∷ []
sig (op-refβœ“ β„“)        = β–  ∷ []
sig op-deref           = β–  ∷ []
sig op-assign          = β–  ∷ β–  ∷ []
sig op-assign?         = β–  ∷ β–  ∷ []
sig op-assignβœ“         = β–  ∷ β–  ∷ []
sig (op-cast c)        = β–  ∷ []
sig (op-prot β„“)        = β–  ∷ []
sig (op-cast-pc g)     = β–  ∷ []
sig (op-error e)       = []
sig op-opaque          = []

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

infixl 7  _Β·_
infix 8 _⟨_⟩

pattern addr_of_ a β„“             = (op-addr a β„“) β¦… nil ⦆
pattern Ζ›βŸ¦_⟧_Λ™_of_ pc A N β„“      = (op-lam pc A β„“) β¦… cons (bind (ast N)) nil ⦆
pattern _Β·_ L M                  = op-app β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern $_of_ k β„“                = (op-const k β„“) β¦… nil ⦆
pattern if L A M N               = (op-if A) β¦… cons (ast L) (cons (ast M) (cons (ast N) nil)) ⦆
pattern `let M N                 = op-let β¦… cons (ast M) (cons (bind (ast N)) nil) ⦆
pattern ref⟦_⟧_ β„“ M              = (op-ref β„“) β¦… cons (ast M) nil ⦆
pattern ref?⟦_⟧_ β„“ M             = (op-ref? β„“) β¦… cons (ast M) nil ⦆
pattern refβœ“βŸ¦_⟧_ β„“ M             = (op-refβœ“ β„“) β¦… cons (ast M) nil ⦆
pattern !_ M                     = op-deref β¦… cons (ast M) nil ⦆
pattern _:=_  L M                = op-assign β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern _:=?_ L M                = op-assign? β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern _:=βœ“_ L M                = op-assignβœ“ β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern _⟨_⟩ M c                 = (op-cast c) β¦… cons (ast M) nil ⦆
pattern prot β„“ M                 = (op-prot β„“) β¦… cons (ast M) nil ⦆      {- protection term -}
pattern cast-pc g M              = (op-cast-pc g) β¦… cons (ast M) nil ⦆
pattern error e                  = (op-error e) β¦… nil ⦆                  {- blame / nsu error -}
pattern ●                        = op-opaque β¦… nil ⦆                    {- opaque value -}


{- There are 3 forms of reference creation: static, not-yet-checked, and checked -}
data RefCreation : (StaticLabel β†’ Term β†’ Term) β†’ Set where
  static    : RefCreation ref⟦_⟧_
  unchecked : RefCreation ref?⟦_⟧_
  checked   : RefCreation refβœ“βŸ¦_⟧_

{- There are 3 forms of reference assignment: static, not-yet-checked, and checked -}
data RefAssign : (Term β†’ Term β†’ Term) β†’ Set where
  static    : RefAssign _:=_
  unchecked : RefAssign _:=?_
  checked   : RefAssign _:=βœ“_