module CC.BigStep 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


infix 2 _∣_⊒_⇓_∣_
data _∣_⊒_⇓_∣_ : Heap β†’ StaticLabel β†’ (M V : Term) β†’ Heap β†’ Set

⇓-value : βˆ€ {ΞΌ ΞΌβ€² pc M V} β†’ ΞΌ ∣ pc ⊒ M ⇓ V ∣ ΞΌβ€² β†’ Value V

{- only consider evaluation to values -}
data _∣_⊒_⇓_∣_ where

  ⇓-val : βˆ€ {ΞΌ pc V}
    β†’ Value V
      --------------------------- Value
    β†’ ΞΌ ∣ pc ⊒ V ⇓ V ∣ ΞΌ

  ⇓-app : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ μ₃ pc pcβ€² L M N V W A β„“}
    β†’ ΞΌ  ∣ pc     ⊒ L       ⇓ Ζ›βŸ¦ pcβ€² ⟧ A Λ™ N of β„“ ∣ μ₁
    β†’ μ₁ ∣ pc     ⊒ M       ⇓ V ∣ ΞΌβ‚‚
    β†’ (⇓W : ΞΌβ‚‚ ∣ pc β‹Ž β„“ ⊒ N [ V ] ⇓ W ∣ μ₃)
      ---------------------------------------------------------------------- Application
    β†’ ΞΌ  ∣ pc     ⊒ L Β· M   ⇓ stamp-val W (⇓-value ⇓W) β„“ ∣ μ₃

  ⇓-if-true : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M N V A β„“}
    β†’ ΞΌ  ∣ pc     ⊒ L ⇓ $ true of β„“ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc β‹Ž β„“ ⊒ M ⇓ V ∣ ΞΌβ‚‚)
      ---------------------------------------------------------------------- IfTrue
    β†’ ΞΌ  ∣ pc     ⊒ if L A M N ⇓ stamp-val V (⇓-value ⇓V) β„“ ∣ ΞΌβ‚‚

  ⇓-if-false : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M N V A β„“}
    β†’ ΞΌ  ∣ pc     ⊒ L ⇓ $ false of β„“ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc β‹Ž β„“ ⊒ N ⇓ V ∣ ΞΌβ‚‚)
      ---------------------------------------------------------------------- IfFalse
    β†’ ΞΌ  ∣ pc     ⊒ if L A M N ⇓ stamp-val V (⇓-value ⇓V) β„“ ∣ ΞΌβ‚‚

  ⇓-let : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc M N V W}
    β†’ ΞΌ  ∣ pc ⊒ M        ⇓ V ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ N [ V ]  ⇓ W ∣ ΞΌβ‚‚
      ----------------------------------------- Let
    β†’ ΞΌ  ∣ pc ⊒ `let M N ⇓ W ∣ ΞΌβ‚‚

  ⇓-ref? : βˆ€ {ΞΌ μ₁ pc M V n β„“}
    β†’ (⇓V : ΞΌ ∣ pc ⊒ M ⇓ V ∣ μ₁)
    β†’ a⟦ β„“ ⟧ n FreshIn μ₁
    β†’ pc β‰Ό β„“
      -------------------------------------------------------------------------------------- RefNSU
    β†’ ΞΌ ∣ pc ⊒ ref?⟦ β„“ ⟧ M ⇓ addr a⟦ β„“ ⟧ n of low ∣ cons-ΞΌ (a⟦ β„“ ⟧ n) V (⇓-value ⇓V) μ₁

  ⇓-ref : βˆ€ {ΞΌ μ₁ pc M V n β„“}
    β†’ (⇓V : ΞΌ ∣ pc ⊒ M ⇓ V ∣ μ₁)
    β†’ a⟦ β„“ ⟧ n FreshIn μ₁
      -------------------------------------------------------------------------------------- Ref
    β†’ ΞΌ ∣ pc ⊒ ref⟦ β„“ ⟧ M ⇓ addr a⟦ β„“ ⟧ n of low ∣ cons-ΞΌ (a⟦ β„“ ⟧ n) V (⇓-value ⇓V) μ₁

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

  ⇓-assign? : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V n β„“ β„“Μ‚}
    β†’ ΞΌ  ∣ pc ⊒ L ⇓ addr a⟦ β„“Μ‚ ⟧ n of β„“ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc ⊒ M ⇓ V ∣ ΞΌβ‚‚)
    β†’ pc β‰Ό β„“Μ‚
      -------------------------------------------------------------------------- AssignNSU
    β†’ ΞΌ ∣ pc ⊒ L :=? M ⇓ $ tt of low ∣ cons-ΞΌ (a⟦ β„“Μ‚ ⟧ n) V (⇓-value ⇓V) ΞΌβ‚‚

  ⇓-assign : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V n β„“ β„“Μ‚}
    β†’ ΞΌ  ∣ pc ⊒ L ⇓ addr a⟦ β„“Μ‚ ⟧ n of β„“ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc ⊒ M ⇓ V ∣ ΞΌβ‚‚)
      -------------------------------------------------------------------------- Assign
    β†’ ΞΌ  ∣ pc ⊒ L := M ⇓ $ tt of low ∣ cons-ΞΌ (a⟦ β„“Μ‚ ⟧ n) V (⇓-value ⇓V) ΞΌβ‚‚

  ⇓-cast : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc M N V W A B} {c : Cast A β‡’ B}
    β†’ Active c
    β†’ ΞΌ  ∣ pc ⊒ M ⇓ V ∣ μ₁
    β†’ ApplyCast V , c ↝ N
    β†’ μ₁ ∣ pc ⊒ N ⇓ W ∣ ΞΌβ‚‚
      --------------------------------------------------------- Cast
    β†’ ΞΌ  ∣ pc ⊒ M ⟨ c ⟩ ⇓ W ∣ ΞΌβ‚‚

  ⇓-if-cast-true : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ μ₃ pc L M N V W A g β„“}
                      {c : Cast (` Bool of g) β‡’ (` Bool of ⋆)}
    β†’ Inert c
    β†’ ΞΌ  ∣ pc     ⊒ L                    ⇓ $ true of β„“ ⟨ c ⟩ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc β‹Ž β„“ ⊒ M ⇓ V ∣ ΞΌβ‚‚)
      {- don't need casting PC to ⋆ in big step -}
    β†’ ΞΌβ‚‚ ∣ pc     ⊒ stamp-val V (⇓-value ⇓V) β„“ ⟨ branch/c A c ⟩ ⇓ W ∣ μ₃
      --------------------------------------------------------- IfCastTrue
    β†’ ΞΌ  ∣ pc     ⊒ if L A M N           ⇓ W ∣ μ₃

  ⇓-if-cast-false : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ μ₃ pc L M N V W A g β„“}
                       {c : Cast (` Bool of g) β‡’ (` Bool of ⋆)}
    β†’ Inert c
    β†’ ΞΌ  ∣ pc     ⊒ L                    ⇓ $ false of β„“ ⟨ c ⟩ ∣ μ₁
    β†’ (⇓V : μ₁ ∣ pc β‹Ž β„“ ⊒ N ⇓ V ∣ ΞΌβ‚‚)
    β†’ ΞΌβ‚‚ ∣ pc     ⊒ stamp-val V (⇓-value ⇓V) β„“ ⟨ branch/c A c ⟩ ⇓ W ∣ μ₃
      --------------------------------------------------------- IfCastFalse
    β†’ ΞΌ  ∣ pc     ⊒ if L A M N           ⇓ W ∣ μ₃

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

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

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

  ⇓-assign-cast : βˆ€ {ΞΌ μ₁ ΞΌβ‚‚ pc L M V W A B g₁ gβ‚‚}
                     {c : Cast (Ref A of g₁) β‡’ (Ref B of gβ‚‚)}
    β†’ (i : Inert c)
    β†’ ΞΌ  ∣ pc ⊒ L                         ⇓ V ⟨ c ⟩ ∣ μ₁
    β†’ μ₁ ∣ pc ⊒ elim-ref-proxy V M i _:=_ ⇓ W ∣ ΞΌβ‚‚
      ----------------------------------------------------------- AssignCast
    β†’ ΞΌ  ∣ pc ⊒ L := M                    ⇓ W ∣ ΞΌβ‚‚


{- If M ⇓ V then V is Value -}
⇓-value (⇓-val v) = v
⇓-value (⇓-app _ _ ⇓W) = stamp-val-value (⇓-value ⇓W)
⇓-value (⇓-if-true  _ ⇓V) = stamp-val-value (⇓-value ⇓V)
⇓-value (⇓-if-false _ ⇓V) = stamp-val-value (⇓-value ⇓V)
⇓-value (⇓-let _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-ref? _ _ _) = V-addr
⇓-value (⇓-ref _ _) = V-addr
⇓-value (⇓-deref {v = v} _ _) = stamp-val-value v
⇓-value (⇓-assign? _ _ _) = V-const
⇓-value (⇓-assign _ _) = V-const
⇓-value (⇓-cast          _ _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-if-cast-true  _ _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-if-cast-false _ _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-fun-cast      _ _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-deref-cast      _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-assign?-cast    _ _ ⇓V) = ⇓-value ⇓V
⇓-value (⇓-assign-cast     _ _ ⇓V) = ⇓-value ⇓V

{- If M ⇓ V then M is not Error -}
error-not-⇓ : βˆ€ {ΞΌ ΞΌβ€² pc M V} β†’ ΞΌ ∣ pc ⊒ M ⇓ V ∣ ΞΌβ€² β†’ Β¬ Err M
error-not-⇓ (⇓-val ()) E-error