------------------------------------------------------------------------
-- Some results about the blocked status and block/unblock
------------------------------------------------------------------------

module StatusLemmas where

open import Syntax
open import Semantics.BigStep
open import Equivalence
open import Totality
open import Data.Nat
open import Data.Product
open import Relation.Nullary

-- If something is possible in the blocked setting, then it is also
-- possible in the unblocked one.

Bto·⇓ : forall {t} {x : Expr t} {v i} -> x ⇓[ B ] v -> x ⇓[ i ] v
Bto·⇓ Val            = Val
Bto·⇓ (Loop ⇓)       = Loop   (Bto·⇓  ⇓)
Bto·⇓ (Add₁ x⇓ y⇓)   = Add₁   (Bto·⇓ x⇓) (Bto·⇓ y⇓)
Bto·⇓ (Add₂ x↯)      = Add₂   (Bto·⇓ x↯)
Bto·⇓ (Add₃ x⇓ y↯)   = Add₃   (Bto·⇓ x⇓) (Bto·⇓ y↯)
Bto·⇓ (Seqn₁ x⇓ y⇒)  = Seqn₁  (Bto·⇓ x⇓) (Bto·⇓ y⇒)
Bto·⇓ (Seqn₂ x↯)     = Seqn₂  (Bto·⇓ x↯)
Bto·⇓ (Catch₁ x⇓)    = Catch₁ (Bto·⇓ x⇓)
Bto·⇓ (Catch₂ x↯ y⇒) = Catch₂ (Bto·⇓ x↯) (Bto·⇓ y⇒)
Bto·⇓ (Block x)      = Block x
Bto·⇓ (Unblock x)    = Unblock x

·toU⇓ : forall {t} {x : Expr t} {v i} -> x ⇓[ i ] v -> x ⇓[ U ] v
·toU⇓ {i = B} x = Bto·⇓ x
·toU⇓ {i = U} x = x

Bto·⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ B ] -> x ⇑[ i ]
Bto·⇑ (Loop loop⇑)        ~ Loop (Bto·⇑ loop⇑)
Bto·⇑ (Add₁ x⇑)           ~ Add₁ (Bto·⇑ x⇑)
Bto·⇑ (Add₂ (_ , x⇓) y⇑)  ~ Add₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
Bto·⇑ (Seqn₁ x⇑)          ~ Seqn₁ (Bto·⇑ x⇑)
Bto·⇑ (Seqn₂ (_ , x⇓) y⇑) ~ Seqn₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑)
Bto·⇑ (Catch₁ x⇑)         ~ Catch₁ (Bto·⇑ x⇑)
Bto·⇑ (Catch₂ x↯ y⇑)      ~ Catch₂ (Bto·⇓ x↯) (Bto·⇑ y⇑)
Bto·⇑ (Block x⇑)          ~ Block x⇑
Bto·⇑ (Unblock x⇑)        ~ Unblock x⇑

·toU⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ i ] -> x ⇑[ U ]
·toU⇑ {i = B} x = Bto·⇑ x
·toU⇑ {i = U} x = x

-- However, the other direction is not valid, not even in a total
-- setting with a non-exceptional end result.

¬UtoB : ¬ (forall (x : Expr total) {n} ->
             x ⇓[ U ] nat n -> x ⇓[ B ] nat n)
¬UtoB UtoB with UtoB (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝) (Catch₂ Int Val)
... | Catch₁ ()
... | Catch₂ () _

-- Furthermore, in a partial setting the following even more limited
-- variant is also invalid.

¬UtoB' : ¬ (forall (x : Expr partial) -> x ↡[ U ] -> x ↡[ B ])
¬UtoB' UtoB'
  with UtoB' (loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝) (0 , Catch₂ Int Val)
... | (n , Catch₁ ⇓)                    = loop-¬⇓ nat-¬↯ (nat n , ⇓)
... | (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯)
... | (n , Catch₂ (Loop (Seqn₂ ())) _)

-- In a total setting the more limited variant is provable, though.

Uto·' : forall {x : Expr total} {i} -> x ↡[ U ] -> x ↡[ i ]
Uto·' (_ , x) = helper x
  where
  helper : forall {x : Expr total} {i m} -> x ⇓[ U ] nat m -> x ↡[ i ]
  helper Val           = (_ , Val)
  helper (Add₁ x⇓ y⇓)  = zip-Σ _+_ Add₁ (helper x⇓) (helper y⇓)
  helper (Seqn₁ x⇓ y⇓) = zip-Σ (\x y -> y) Seqn₁ (helper x⇓) (helper y⇓)
  helper (Catch₁ x⇓)   = map-Σ₂ Catch₁ (helper x⇓)
  helper (Block x)     = (_ , Block x)
  helper (Unblock x)   = (_ , Unblock x)
  helper {x catch y} {i} (Catch₂ x↯ y⇓) with defined x i
  ... | (throw , x↯') = (_ , Catch₂ x↯' y⇓)
  ... | (nat n , x⇓)  = (n , Catch₁ x⇓)

-- The problems with converting from U to B also mean that uses of
-- block and unblock seldom can be simplified.

block-unblockˡ : forall {t} {x : Expr t} -> x ⊑ block (unblock x)
block-unblockˡ = record { ⇓ = \x -> Block (Unblock (·toU⇓ x))
                        ; ⇑ = \x -> Block (Unblock (·toU⇑ x))
                        }

block-unblockʳ : ¬ (forall t (x : Expr t) -> block (unblock x) ⊑ x)
block-unblockʳ bux⊑x
  with _⊑_.⇓ (bux⊑x total ⌜ nat 0 ⌝) {i = B} (Block (Unblock Int))
... | ()

unblock-blockˡ : ¬ (forall t (x : Expr t) -> x ⊑ unblock (block x))
unblock-blockˡ x⊑ubx
  with _⊑_.⇓ (x⊑ubx total (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝)) (Catch₂ Int Val)
... | Unblock (Block (Catch₁ ()))
... | Unblock (Block (Catch₂ () _))

unblock-blockʳ : ¬ (forall t (x : Expr t) -> unblock (block x) ⊑ x)
unblock-blockʳ ubx⊑x
  with _⊑_.⇓ (ubx⊑x total ⌜ nat 0 ⌝) {i = B} (Unblock Int)
... | ()