------------------------------------------------------------------------
-- 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·⇓ : ∀ {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⇓ : ∀ {t} {x : Expr t} {v i} → x ⇓[ i ] v → x ⇓[ U ] v
·toU⇓ {i = B} x = Bto·⇓ x
·toU⇓ {i = U} x = x

Bto·⇑ : ∀ {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⇑ : ∀ {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.

¬UtoB : ∀ t v → ∃ λ (x : Expr t) → x ⇓[ U ] v × ¬ (x ⇓[ B ] v)
¬UtoB t v = (x , Catch₂ Int Val , helper)
  where
  v′ : Value
  v′ with v
  ... | nat  = nat 
  ... | _     = nat 

  x : Expr t
  x = ⌜ v′ ⌝ catch ⌜ v ⌝

  helper : ¬ (x ⇓[ B ] v)
  helper x⇓ with v
  helper (Catch₁ ())   | nat zero
  helper (Catch₁ ())   | nat (suc n)
  helper (Catch₂ () _) | nat zero
  helper (Catch₂ () _) | nat (suc n)
  helper (Catch₂ () _) | throw

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

Uto·' : ∀ {x : Expr total} {i} → x ↡[ U ] → x ↡[ i ]
Uto·' (_ , x) = helper x
  where
  helper : ∀ {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⇓)

-- ...but not in a partial setting.

¬UtoB′ : ∃ λ (x : Expr partial) → x ↡[ U ] × ¬ (x ↡[ B ])
¬UtoB′ = (x , ( , Catch₂ Int Val) , helper)
  where
  x = loop ⌜ nat  ⌝ catch ⌜ nat  ⌝

  helper : ¬ (x ↡[ B ])
  helper (n , Catch₁ ⇓)                    = loop-¬⇓ nat-¬↯ (nat n , ⇓)
  helper (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯)
  helper (n , Catch₂ (Loop (Seqn₂ ())) _)

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

block-unblockˡ : ∀ {t} {x : Expr t} → x ⊑ block (unblock x)
block-unblockˡ = record { ⇓ = λ x → Block (Unblock (·toU⇓ x))
                        ; ⇑ = λ x → Block (Unblock (·toU⇑ x))
                        }

block-unblockʳ : ∀ t → ∃ λ (x : Expr t) → block (unblock x) ⋢ x
block-unblockʳ _ =
  (⌜ nat  ⌝ , λ bu⊑ → nat-¬↯ (_⊑_.⇓ bu⊑ {i = B} (Block (Unblock Int))))

unblock-blockˡ : ∀ t → ∃ λ (x : Expr t) → x ⋢ unblock (block x)
unblock-blockˡ t =
  (⌜ nat  ⌝ catch ⌜ nat  ⌝ , λ ⊑ub →
     helper (_⊑_.⇓ ⊑ub (Catch₂ Int Val)))
  where
  helper : ¬ (unblock {t} (block (⌜ nat  ⌝ catch ⌜ nat  ⌝))
                ⇓[ U ] nat )
  helper (Unblock (Block (Catch₁ ())))
  helper (Unblock (Block (Catch₂ () _)))

unblock-blockʳ : ∀ t → ∃ λ (x : Expr t) → unblock (block x) ⋢ x
unblock-blockʳ _ =
  (⌜ nat  ⌝ , λ ub⊑ → nat-¬↯ (_⊑_.⇓ ub⊑ {i = B} (Unblock Int)))