open import Common.Types

module CC2.Syntax where

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

open import Syntax
open import Common.BlameLabels
open import Common.Coercions public
open import LabelExpr.LabelExpr
  renaming (blame to bl; Irreducible to Ir;
            Progress to Progressβ‚‘; progress to progressβ‚‘; ⊒_βŠ‘_⇐_βŠ‘_ to _βŠ‘_⇐_βŠ‘_)
  hiding (_∎; _β€”β†’βŸ¨_⟩_) public
open import Memory.Addr


data Op : Set where
  op-addr         : (n : RawAddr) β†’ Op
  op-lam          : Op
  op-app          : (A B : Type) β†’ (β„“ : StaticLabel) β†’ Op
  op-app⋆         : (A : Type) β†’ (T : RawType) β†’ Op
  op-const        : βˆ€ {ΞΉ} (k : rep ΞΉ) β†’ Op
  op-if           : (A : Type) β†’ (β„“ : StaticLabel) β†’ Op
  op-if⋆          : (T : RawType) β†’ Op
  op-let          : (A : Type) β†’ Op
  op-ref          : (β„“ : StaticLabel) β†’ Op
  op-ref?         : (β„“ : StaticLabel) β†’ (p : BlameLabel) β†’ Op
  op-deref        : (A : Type) β†’ (β„“ : StaticLabel) β†’ Op
  op-deref⋆       : (T : RawType) β†’ Op
  op-assign       : (T : RawType) β†’ (β„“Μ‚ β„“ : StaticLabel) β†’ Op
  op-assign?      : (T : RawType) β†’ (gΜ‚ : Label) β†’ BlameLabel β†’ Op
  op-cast         : βˆ€ {A B} β†’ Cast A β‡’ B β†’ Op
  op-prot         : βˆ€ (A : Type) β†’ (PC : LExpr) β†’ LVal PC
                                 β†’ (β„“ : StaticLabel) β†’ Op
  op-blame        : BlameLabel β†’ Op
  {- Terms that only appear in erasure -}
  op-opaque       : Op

sig : Op β†’ List Sig
sig (op-addr n)        = []
sig op-lam             = (Ξ½ β– ) ∷ []
sig (op-app  A B β„“)    = β–  ∷ β–  ∷ []
sig (op-app⋆ A B)      = β–  ∷ β–  ∷ []
sig (op-const k)       = []
sig (op-if  A β„“)       = β–  ∷ β–  ∷ β–  ∷ []
sig (op-if⋆ A)         = β–  ∷ β–  ∷ β–  ∷ []
sig (op-let A)         = β–  ∷ (Ξ½ β– ) ∷ []
sig (op-ref β„“)         = β–  ∷ []
sig (op-ref? β„“ p)      = β–  ∷ []
sig (op-deref A β„“)     = β–  ∷ []
sig (op-deref⋆ A)      = β–  ∷ []
sig (op-assign  T β„“Μ‚ β„“) = β–  ∷ β–  ∷ []
sig (op-assign? T gΜ‚ p) = β–  ∷ β–  ∷ []
sig (op-cast c)        = β–  ∷ []
sig (op-prot A PC v β„“)   = β–  ∷ []
sig (op-blame p)       = []
sig op-opaque          = []

open Syntax.OpSig Op sig renaming (ABT to Term; plug to plug-abt; βŸͺ_⟫ to β¦…_⦆) public

infix 8 _⟨_⟩

pattern addr n             = (op-addr n) β¦… nil ⦆
pattern Ζ› N                = (op-lam) β¦… cons (bind (ast N)) nil ⦆
pattern app L M A B β„“      = (op-app A B β„“) β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern app⋆ L M A T       = (op-app⋆ A T) β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern $_ 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 if⋆ L T M N        = (op-if⋆ T) β¦… cons (ast L) (cons (ast M) (cons (ast N) nil)) ⦆
pattern `let M A N         = (op-let A) β¦… cons (ast M) (cons (bind (ast N)) nil) ⦆
pattern ref⟦_⟧ β„“ M         = (op-ref β„“) β¦… cons (ast M) nil ⦆
pattern ref?⟦_⟧ β„“ M p      = (op-ref? β„“ p) β¦… cons (ast M) nil ⦆
pattern ! M A g            = (op-deref A g) β¦… cons (ast M) nil ⦆
pattern !⋆ M T             = (op-deref⋆ T) β¦… cons (ast M) nil ⦆
pattern assign  L M T β„“Μ‚ β„“  = (op-assign  T β„“Μ‚ β„“) β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern assign? L M T gΜ‚ p  = (op-assign? T gΜ‚ p) β¦… cons (ast L) (cons (ast M) nil) ⦆
pattern _⟨_⟩ M c           = (op-cast c) β¦… cons (ast M) nil ⦆
pattern prot PC v β„“ M A    = (op-prot A PC v β„“) β¦… cons (ast M) nil ⦆
pattern blame p            = (op-blame p) β¦… nil ⦆
pattern ●                 = op-opaque β¦… nil ⦆                     {- opaque value -}