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
infix 7 nat_⊕•_
infixl 7 _•⊕_
infixl 6 _•catch_
infixl 5 _•>>_
data EvalCtxt t : Status → Status → Set where
• : ∀ {i} → EvalCtxt t i i
_•⊕_ : ∀ {i j} (E : EvalCtxt t i j) (y : Exprˢ t) → EvalCtxt t i j
_•>>_ : ∀ {i j} (E : EvalCtxt t i j) (y : Exprˢ t) → EvalCtxt t i j
_•catch_ : ∀ {i j} (E : EvalCtxt t i j) (y : Exprˢ t) → EvalCtxt t i j
nat_⊕•_ : ∀ {i j} (m : ℕ) (E : EvalCtxt t i j) → EvalCtxt t i j
handler• : ∀ {i j} (E : EvalCtxt t i B) → EvalCtxt t i j
block• : ∀ {i j} (E : EvalCtxt t i B) → EvalCtxt t i j
unblock• : ∀ {i j} (E : EvalCtxt t i U) → EvalCtxt t i j
infix 9 _[_]
_[_] : ∀ {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 ]))
lift⟶ : ∀ {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⟶⋆ : ∀ {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⟶∞ : ∀ {t i j x} (E : EvalCtxt t i j) →
x ⟶∞[ i ] → E [ x ] ⟶∞[ j ]
lift⟶∞ E = map∞ (λ x → E [ x ]) (lift⟶ E)
infixr 10 _⊚_
_⊚_ : ∀ {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 : ∀ {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₂)
infix 2 _⟶E[_]_
data _⟶E[_]_ {t} : Exprˢ t → Status → Exprˢ t → Set where
Red : ∀ {x y i j} (E : EvalCtxt t i j) (x⟶ʳy : x ⟶ʳ[ i ] y) →
E [ x ] ⟶E[ j ] E [ y ]
lift⟶E : ∀ {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 : ∀ {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⇒⟶ : ∀ {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))