module CC.Reduction where

open import Data.Nat
open import Data.Unit using (⊀; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List hiding ([_])
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)

open import Common.Utils
open import Common.Types
open import CC.CCStatics
open import Memory.Heap Term Value

open import CC.ApplyCast        public
open import CC.ProxyElimination public
open import CC.Frame            public


infix 2 _∣_∣_β€”β†’_∣_

data _∣_∣_β€”β†’_∣_ : Term β†’ Heap β†’ StaticLabel β†’ Term β†’ Heap β†’ Set where

  ΞΎ : βˆ€ {M Mβ€² F ΞΌ ΞΌβ€² pc}
    β†’ M        ∣ ΞΌ ∣ pc β€”β†’ Mβ€²        ∣ ΞΌβ€²
      ---------------------------------------------- ΞΎ
    β†’ plug M F ∣ ΞΌ ∣ pc β€”β†’ plug Mβ€² F ∣ ΞΌβ€²

  ΞΎ-err : βˆ€ {F ΞΌ pc e}
      ---------------------------------------------- ΞΎ-error
    β†’ plug (error e) F ∣ ΞΌ ∣ pc β€”β†’ error e ∣ ΞΌ

  prot-val : βˆ€ {V ΞΌ pc β„“}
    β†’ (v : Value V)
      --------------------------------------------------- ProtectVal
    β†’ prot β„“ V ∣ ΞΌ ∣ pc β€”β†’ stamp-val V v β„“ ∣ ΞΌ

  prot-ctx : βˆ€ {M Mβ€² ΞΌ ΞΌβ€² pc β„“}
    β†’ M        ∣ ΞΌ ∣ pc β‹Ž β„“ β€”β†’ Mβ€²        ∣ ΞΌβ€²
      --------------------------------------------------- ProtectContext
    β†’ prot β„“ M ∣ ΞΌ ∣ pc     β€”β†’ prot β„“ Mβ€² ∣ ΞΌβ€²

  prot-err : βˆ€ {ΞΌ pc β„“ e}
      --------------------------------------------------- ProtectContext
    β†’ prot β„“ (error e) ∣ ΞΌ ∣ pc β€”β†’ error e ∣ ΞΌ

  Ξ² : βˆ€ {V N ΞΌ pc pcβ€² A β„“}
    β†’ Value V
      ------------------------------------------------------------------- Ξ²
    β†’ (Ζ›βŸ¦ pcβ€² ⟧ A Λ™ N of β„“) Β· V ∣ ΞΌ ∣ pc β€”β†’ prot β„“ (N [ V ]) ∣ ΞΌ

  Ξ²-if-true : βˆ€ {M N ΞΌ pc A β„“}
      ----------------------------------------------------------------------- IfTrue
    β†’ if ($ true of β„“) A M N ∣ ΞΌ ∣ pc β€”β†’ prot β„“ M ∣ ΞΌ

  Ξ²-if-false : βˆ€ {M N ΞΌ pc A β„“}
      ----------------------------------------------------------------------- IfFalse
    β†’ if ($ false of β„“) A M N ∣ ΞΌ ∣ pc β€”β†’ prot β„“ N ∣ ΞΌ

  Ξ²-let : βˆ€ {V N ΞΌ pc}
    β†’ Value V
      -------------------------------------- Let
    β†’ `let V N ∣ ΞΌ ∣ pc β€”β†’ N [ V ] ∣ ΞΌ

  ref-static : βˆ€ {M ΞΌ pc β„“}
      ------------------------------------------------- RefStatic
    β†’ ref⟦ β„“ ⟧ M ∣ ΞΌ ∣ pc β€”β†’ refβœ“βŸ¦ β„“ ⟧ M ∣ ΞΌ

  ref?-ok : βˆ€ {M ΞΌ pc β„“}
    β†’ pc β‰Ό β„“
      ------------------------------------------------- RefNSUSuccess
    β†’ ref?⟦ β„“ ⟧ M ∣ ΞΌ ∣ pc β€”β†’ refβœ“βŸ¦ β„“ ⟧ M ∣ ΞΌ

  ref?-fail : βˆ€ {M ΞΌ pc β„“}
    β†’ Β¬ pc β‰Ό β„“
      ------------------------------------------------- RefNSUFail
    β†’ ref?⟦ β„“ ⟧ M ∣ ΞΌ ∣ pc β€”β†’ error nsu-error ∣ ΞΌ

  ref : βˆ€ {V ΞΌ pc n β„“}
    β†’ (v : Value V)
    β†’ a⟦ β„“ ⟧ n FreshIn ΞΌ  {- address is fresh -}
      -------------------------------------------------------------------------------- Ref
    β†’ refβœ“βŸ¦ β„“ ⟧ V ∣ ΞΌ ∣ pc β€”β†’ addr (a⟦ β„“ ⟧ n) of low ∣ cons-ΞΌ (a⟦ β„“ ⟧ n) V v ΞΌ

  deref : βˆ€ {V ΞΌ pc v n β„“ β„“Μ‚}
    β†’ lookup-ΞΌ ΞΌ (a⟦ β„“Μ‚ ⟧ n) ≑ just (V & v)
      --------------------------------------------------------------------- Deref
    β†’ ! (addr (a⟦ β„“Μ‚ ⟧ n) of β„“) ∣ ΞΌ ∣ pc β€”β†’ prot (β„“Μ‚ β‹Ž β„“) V ∣ ΞΌ

  assign-static : βˆ€ {L M ΞΌ pc}
      ------------------------------------------------------- AssignStatic
    β†’ L := M ∣ ΞΌ ∣ pc β€”β†’ L :=βœ“ M ∣ ΞΌ

  assign?-ok : βˆ€ {M ΞΌ pc n β„“ β„“Μ‚}
    β†’ pc β‰Ό β„“Μ‚
      ----------------------------------------------------------------------------- AssignNSUSuccess
    β†’ (addr (a⟦ β„“Μ‚ ⟧ n) of β„“) :=? M ∣ ΞΌ ∣ pc β€”β†’ (addr (a⟦ β„“Μ‚ ⟧ n) of β„“) :=βœ“ M ∣ ΞΌ

  assign?-fail : βˆ€ {M ΞΌ pc n β„“ β„“Μ‚}
    β†’ Β¬ pc β‰Ό β„“Μ‚
      ----------------------------------------------------------------------------- AssignNSUFail
    β†’ (addr (a⟦ β„“Μ‚ ⟧ n) of β„“) :=? M ∣ ΞΌ ∣ pc β€”β†’ error nsu-error ∣ ΞΌ

  assign : βˆ€ {V ΞΌ pc n β„“ β„“Μ‚}
    β†’ (v : Value V)
      ---------------------------------------------------------------------------------------------- Assign
    β†’ (addr (a⟦ β„“Μ‚ ⟧ n) of β„“) :=βœ“ V ∣ ΞΌ ∣ pc β€”β†’ $ tt of low ∣ cons-ΞΌ (a⟦ β„“Μ‚ ⟧ n) V v ΞΌ

  {- Reduction rules about casts, active and inert: -}
  cast : βˆ€ {A B V M ΞΌ pc} {c : Cast A β‡’ B}
    β†’ Value V β†’ Active c
    β†’ ApplyCast V , c ↝ M
      -------------------------------------------------- Cast
    β†’ V ⟨ c ⟩ ∣ ΞΌ ∣ pc β€”β†’ M ∣ ΞΌ

  if-cast-true : βˆ€ {M N ΞΌ pc A g β„“} {c : Cast (` Bool of g) β‡’ (` Bool of ⋆)}
    β†’ Inert c
      --------------------------------------------------------------------------------------------- IfCastTrue
    β†’ if ($ true of β„“ ⟨ c ⟩) A M N ∣ ΞΌ ∣ pc β€”β†’ prot β„“ (cast-pc ⋆ M) ⟨ branch/c A c ⟩ ∣ ΞΌ

  if-cast-false : βˆ€ {M N ΞΌ pc A g β„“} {c : Cast (` Bool of g) β‡’ (` Bool of ⋆)}
    β†’ Inert c
      --------------------------------------------------------------------------------------------- IfCastFalse
    β†’ if ($ false of β„“ ⟨ c ⟩) A M N ∣ ΞΌ ∣ pc β€”β†’ prot β„“ (cast-pc ⋆ N) ⟨ branch/c A c ⟩ ∣ ΞΌ

  fun-cast : βˆ€ {V W ΞΌ pc A B C D gc₁ gcβ‚‚ g₁ gβ‚‚} {c : Cast (⟦ gc₁ ⟧ A β‡’ B of g₁) β‡’ (⟦ gcβ‚‚ ⟧ C β‡’ D of gβ‚‚)}
    β†’ Value V β†’ Value W
    β†’ (i : Inert c)
      ---------------------------------------------------------------- FunCast
    β†’ (V ⟨ c ⟩) Β· W ∣ ΞΌ ∣ pc β€”β†’ elim-fun-proxy V W i pc ∣ ΞΌ

  deref-cast : βˆ€ {V ΞΌ pc A B g₁ gβ‚‚} {c : Cast (Ref A of g₁) β‡’ (Ref B of gβ‚‚)}
    β†’ Value V
    β†’ Inert c
      ------------------------------------------------------ DerefCast
    β†’ ! (V ⟨ c ⟩) ∣ ΞΌ ∣ pc β€”β†’ ! V ⟨ out/c c ⟩ ∣ ΞΌ

  assign?-cast : βˆ€ {V M ΞΌ pc A B g₁ gβ‚‚} {c : Cast (Ref A of g₁) β‡’ (Ref B of gβ‚‚)}
    β†’ Value V
    β†’ (i : Inert c)
      ----------------------------------------------------------------------------- AssignNSUCast
    β†’ (V ⟨ c ⟩) :=? M ∣ ΞΌ ∣ pc β€”β†’ elim-ref-proxy V M i _:=?_ ∣ ΞΌ

  assign-cast : βˆ€ {V W ΞΌ pc A B g₁ gβ‚‚} {c : Cast (Ref A of g₁) β‡’ (Ref B of gβ‚‚)}
    β†’ Value V β†’ Value W
    β†’ (i : Inert c)
      --------------------------------------------------------------------------------------------- AssignCast
    β†’ (V ⟨ c ⟩) :=βœ“ W ∣ ΞΌ ∣ pc β€”β†’ elim-ref-proxy V W i _:=βœ“_ {- V := (W ⟨ in/c c ⟩) -} ∣ ΞΌ

  Ξ²-cast-pc : βˆ€ {V ΞΌ pc g}
    β†’ Value V
      ------------------------------------- CastPC
    β†’ cast-pc g V ∣ ΞΌ ∣ pc β€”β†’ V ∣ ΞΌ