------------------------------------------------------------------------
-- Evaluation contexts
------------------------------------------------------------------------

-- The evaluation contexts are not part of the definition of the
-- semantics, they are just available as a convenience.

module Semantics.SmallStep.EvalCtxt where

open import Syntax
open import Infinite
open import Semantics.SmallStep

open import Data.Nat
open import Data.Star
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Evaluation contexts

infix  7 nat_⊕•_
infixl 7 _•⊕_
infixl 6 _•catch_
infixl 5 _•>>_

-- The evaluation contexts are indexed on the status at the hole and
-- the outermost status (see lift⟶ below).

data EvalCtxt t : Status -> Status -> Set where
  •        : forall {i} -> EvalCtxt t i i
  _•⊕_     : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j
  _•>>_    : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j
  _•catch_ : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j
  nat_⊕•_  : forall {i j} (m : ℕ) (E : EvalCtxt t i j) -> EvalCtxt t i j
  handler• : forall {i j} (E : EvalCtxt t i B) -> EvalCtxt t i j
  block•   : forall {i j} (E : EvalCtxt t i B) -> EvalCtxt t i j
  unblock• : forall {i j} (E : EvalCtxt t i U) -> EvalCtxt t i j

-- Filling holes.

infix 9 _[_]

_[_] : forall {t i j} -> EvalCtxt t i j -> Exprˢ t -> Exprˢ t
•            [ y ] = y
(E •⊕     x) [ y ] = run (E [ y ] ⊕     x)
(E •>>    x) [ y ] = run (E [ y ] >>    x)
(E •catch x) [ y ] = run (E [ y ] catch x)
(nat n ⊕• E) [ y ] = run (done (nat n) ⊕ E [ y ])
(handler• E) [ y ] = run (done throw catch E [ y ])
(block•   E) [ y ] = run (block   (E [ y ]))
(unblock• E) [ y ] = run (unblock (E [ y ]))

------------------------------------------------------------------------
-- Lifting of reductions/reduction sequences

lift⟶ : forall {t i j x y} (E : EvalCtxt t i j) ->
        x ⟶[ i ] y -> E [ x ] ⟶[ j ] E [ y ]
lift⟶ •            ⟶ = ⟶
lift⟶ (E •⊕     y) ⟶ = Addˡ     (lift⟶ E ⟶)
lift⟶ (E •>>    y) ⟶ = Seqnˡ    (lift⟶ E ⟶)
lift⟶ (E •catch y) ⟶ = Catchˡ   (lift⟶ E ⟶)
lift⟶ (nat m ⊕• E) ⟶ = Addʳ     (lift⟶ E ⟶)
lift⟶ (handler• E) ⟶ = Catchʳ   (lift⟶ E ⟶)
lift⟶ (block•   E) ⟶ = Blockˡ   (lift⟶ E ⟶)
lift⟶ (unblock• E) ⟶ = Unblockˡ (lift⟶ E ⟶)

lift⟶⋆ : forall {t i j x y} (E : EvalCtxt t i j) ->
         x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ]
lift⟶⋆ E = gmap (\x -> E [ x ]) (lift⟶ E)

lift⟶∞ : forall {t i j x} (E : EvalCtxt t i j) ->
         x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ]
lift⟶∞ E = map∞ (\x -> E [ x ]) (lift⟶ E)

------------------------------------------------------------------------
-- Composition of evaluation contexts

infixr 10 _⊚_

_⊚_ : forall {t i j k} ->
      EvalCtxt t j k -> EvalCtxt t i j -> EvalCtxt t i k
•             ⊚ E₂ = E₂
(E₁ •⊕     y) ⊚ E₂ = (E₁ ⊚ E₂) •⊕     y
(E₁ •>>    y) ⊚ E₂ = (E₁ ⊚ E₂) •>>    y
(E₁ •catch y) ⊚ E₂ = (E₁ ⊚ E₂) •catch y
(nat n ⊕• E₁) ⊚ E₂ = nat n ⊕• (E₁ ⊚ E₂)
handler• E₁   ⊚ E₂ = handler• (E₁ ⊚ E₂)
block•   E₁   ⊚ E₂ = block•   (E₁ ⊚ E₂)
unblock• E₁   ⊚ E₂ = unblock• (E₁ ⊚ E₂)

⊚-lemma : forall {t i j k}
          (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} ->
          E₁ ⊚ E₂ [ x ] ≡ E₁ [ E₂ [ x ] ]
⊚-lemma •             E₂ = ≡-refl
⊚-lemma (E₁ •⊕     y) E₂ = ≡-cong (\x -> run (x ⊕     y)  )        (⊚-lemma E₁ E₂)
⊚-lemma (E₁ •>>    y) E₂ = ≡-cong (\x -> run (x >>    y))          (⊚-lemma E₁ E₂)
⊚-lemma (E₁ •catch y) E₂ = ≡-cong (\x -> run (x catch y))          (⊚-lemma E₁ E₂)
⊚-lemma (nat n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (nat n) ⊕ x))   (⊚-lemma E₁ E₂)
⊚-lemma (handler• E₁) E₂ = ≡-cong (\x -> run (done throw catch x)) (⊚-lemma E₁ E₂)
⊚-lemma (block•   E₁) E₂ = ≡-cong (\x -> run (block   x))          (⊚-lemma E₁ E₂)
⊚-lemma (unblock• E₁) E₂ = ≡-cong (\x -> run (unblock x))          (⊚-lemma E₁ E₂)

------------------------------------------------------------------------
-- Another view of the small-step relation

-- Every step can be decomposed into a reduction and an evaluation
-- context.

infix 2 _⟶E[_]_

data _⟶E[_]_ {t} : Exprˢ t -> Status -> Exprˢ t -> Set where
  Red : forall {x y i j} (E : EvalCtxt t i j)
        (x⟶ʳy : x ⟶ʳ[ i ] y) -> E [ x ] ⟶E[ j ] E [ y ]

-- The two views are equivalent:

lift⟶E : forall {t i j x y} (E : EvalCtxt t i j) ->
         x ⟶E[ i ] y -> E [ x ] ⟶E[ j ] E [ y ]
lift⟶E {j = j} E₁ (Red {x = x} {y = y} E₂ red) =
  ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶E[ j ] y') (⊚-lemma E₁ E₂)
    (≡-subst (\x' -> x' ⟶E[ j ] E₁ ⊚ E₂ [ y ]) (⊚-lemma E₁ E₂)
       (Red (E₁ ⊚ E₂) red))

⟶⇒⟶E : forall {t i} {x y : Exprˢ t} ->
       x ⟶[ i ] y -> x ⟶E[ i ] y
⟶⇒⟶E (Red      ⟶) = Red • ⟶
⟶⇒⟶E (Addˡ     ⟶) = lift⟶E (• •⊕ _)     (⟶⇒⟶E ⟶)
⟶⇒⟶E (Addʳ     ⟶) = lift⟶E (nat _ ⊕• •) (⟶⇒⟶E ⟶)
⟶⇒⟶E (Seqnˡ    ⟶) = lift⟶E (• •>> _)    (⟶⇒⟶E ⟶)
⟶⇒⟶E (Catchˡ   ⟶) = lift⟶E (• •catch _) (⟶⇒⟶E ⟶)
⟶⇒⟶E (Catchʳ   ⟶) = lift⟶E (handler• •) (⟶⇒⟶E ⟶)
⟶⇒⟶E (Blockˡ   ⟶) = lift⟶E (block• •)   (⟶⇒⟶E ⟶)
⟶⇒⟶E (Unblockˡ ⟶) = lift⟶E (unblock• •) (⟶⇒⟶E ⟶)

⟶E⇒⟶ : forall {t i} {x y : Exprˢ t} ->
       x ⟶E[ i ] y -> x ⟶[ i ] y
⟶E⇒⟶ (Red •            x⟶ʳy) = Red x⟶ʳy
⟶E⇒⟶ (Red (E •⊕     y) x⟶ʳy) = lift⟶ (• •⊕ y)     (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (E •>>    y) x⟶ʳy) = lift⟶ (• •>> y)    (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (E •catch y) x⟶ʳy) = lift⟶ (• •catch y) (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (nat m ⊕• E) x⟶ʳy) = lift⟶ (nat m ⊕• •) (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (handler• E) x⟶ʳy) = lift⟶ (handler• •) (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (block• E)   x⟶ʳy) = lift⟶ (block• •)   (⟶E⇒⟶ (Red E x⟶ʳy))
⟶E⇒⟶ (Red (unblock• E) x⟶ʳy) = lift⟶ (unblock• •) (⟶E⇒⟶ (Red E x⟶ʳy))