------------------------------------------------------------------------
-- Some properties related to totality
------------------------------------------------------------------------

module Totality where

open import Syntax
open import Semantics.BigStep

open import Data.Nat
open import Data.Empty
open import Data.Product
open import Relation.Nullary

-- Some properties of loop.

loop-⇑ : ∀ {x i} → x ↡[ i ] → loop x ⇑[ i ]
loop-⇑ x↡ ~ Loop (Seqn₂ x↡ (loop-⇑ x↡))

loop-¬⇓ : ∀ {x} → ¬ x ↯[ B ] → ¬ loop x ⇓[ B ]
loop-¬⇓ ¬x↯ (v      , Loop (Seqn₁ _ ⇓)) = loop-¬⇓ ¬x↯ (v , ⇓)
loop-¬⇓ ¬x↯ (.throw , Loop (Seqn₂ x↯))  = ¬x↯ x↯

loop-¬↡ : ∀ {x i} → ¬ loop x ↡[ i ]
loop-¬↡ (n , Loop (Seqn₁ x↡ y⇓)) = loop-¬↡ (n , y⇓)

-- A utility function.

nat-¬↯ : ∀ {n t} → ¬ ⌜_⌝ {t = t} (nat n) ↯[ B ]
nat-¬↯ ()

-- Partial expressions can sometimes be completely undefined.

¬defined : ∃₂ λ (x : Expr partial) i → ¬ x ⇓[ i ]
¬defined = (loop ⌜ nat  ⌝ , B , loop-¬⇓ nat-¬↯)

-- The expressions denoted as total are always potentially
-- terminating...

defined : ∀ (x : Expr total) i → x ⇓[ i ]
defined ⌜ v ⌝   _ = (_ , Val)
defined (x ⊕ y) i with defined x i | defined y i
... | (nat _ , x⇓) | (nat _ , y⇓) = (_ , Add₁ x⇓ y⇓)
... | (nat _ , x⇓) | (throw , y↯) = (_ , Add₃ x⇓ y↯)
... | (throw , x↯) | _            = (_ , Add₂ x↯)
defined (x >> y) i with defined x i | defined y i
... | (nat _ , x⇓) | (nat _ , y⇓) = (_ , Seqn₁ x⇓ y⇓)
... | (nat _ , x⇓) | (throw , y↯) = (_ , Seqn₁ x⇓ y↯)
... | (throw , x↯) | _            = (_ , Seqn₂ x↯)
defined (x catch y) i with defined x i | defined y B
... | (nat _ , x⇓) | _            = (_ , Catch₁ x⇓)
... | (throw , x↯) | (nat _ , y⇓) = (_ , Catch₂ x↯ y⇓)
... | (throw , x↯) | (throw , y↯) = (_ , Catch₂ x↯ y↯)
defined (block   x) _ = map-Σ₂ Block   (defined x B)
defined (unblock x) _ = map-Σ₂ Unblock (defined x U)

-- ...and never non-terminating.

¬undefined : ∀ (x : Expr total) {i} → ¬ x ⇑[ i ]
¬undefined ⌜ v ⌝       ()
¬undefined (x ⊕     y) (Add₁ x⇑)      = ¬undefined x x⇑
¬undefined (x ⊕     y) (Add₂ x⇓ y⇑)   = ¬undefined y y⇑
¬undefined (x >>    y) (Seqn₁ x⇑)     = ¬undefined x x⇑
¬undefined (x >>    y) (Seqn₂ x⇓ y⇑)  = ¬undefined y y⇑
¬undefined (x catch y) (Catch₁ x⇑)    = ¬undefined x x⇑
¬undefined (x catch y) (Catch₂ x↯ y⇑) = ¬undefined y y⇑
¬undefined (block   x) (Block   x⇑)   = ¬undefined x x⇑
¬undefined (unblock x) (Unblock x⇑)   = ¬undefined x x⇑

-- Some simple consequences.

cannot-throw⇒can-return :
  ∀ {x : Expr total} {i} → ¬ x ↯[ i ] → x ↡[ i ]
cannot-throw⇒can-return {x} {i} ¬x↯ with defined x i
... | (nat n , x↡) = (n , x↡)
... | (throw , x↯) = ⊥-elim (¬x↯ x↯)

cannot-return⇒can-throw :
  ∀ {x : Expr total} {i} → ¬ x ↡[ i ] → x ↯[ i ]
cannot-return⇒can-throw {x} {i} ¬x↡ with defined x i
... | (nat n , x↡) = ⊥-elim (¬x↡ (n , x↡))
... | (throw , x↯) = x↯

-- We can be more precise than in "defined" above.

can-throw? : ∀ (x : Expr total) i → Dec (x ↯[ i ])
can-throw? _         U = yes Int
can-throw? ⌜ nat m ⌝ B = no nat-¬↯
can-throw? ⌜ throw ⌝ B = yes Val
can-throw? (x ⊕ y) B with can-throw? x B | can-throw? y B
... | yes x↯ | _      = yes (Add₂ x↯)
... | no ¬x↯ | yes y↯ = yes (Add₃ (proj₂ (cannot-throw⇒can-return ¬x↯)) y↯)
... | no ¬x↯ | no ¬y↯ = no helper
  where
  helper : ¬ x ⊕ y ↯[ B ]
  helper (Add₂ x↯)   = ¬x↯ x↯
  helper (Add₃ _ y↯) = ¬y↯ y↯
can-throw? (x >> y) B with can-throw? x B | can-throw? y B
... | yes x↯ | _      = yes (Seqn₂ x↯)
... | no ¬x↯ | yes y↯ = yes (Seqn₁ (proj₂ (cannot-throw⇒can-return ¬x↯)) y↯)
... | no ¬x↯ | no ¬y↯ = no helper
  where
  helper : ¬ x >> y ↯[ B ]
  helper (Seqn₁ _ y↯) = ¬y↯ y↯
  helper (Seqn₂ x↯)   = ¬x↯ x↯
can-throw? (x catch y) B with can-throw? x B | can-throw? y B
... | yes x↯ | yes y↯ = yes (Catch₂ x↯ y↯)
... | yes x↯ | no ¬y↯ = no helper
  where
  helper : ¬ x catch y ↯[ B ]
  helper (Catch₂ _ y↯) = ¬y↯ y↯
... | no ¬x↯ | _      = no helper
  where
  helper : ¬ x catch y ↯[ B ]
  helper (Catch₂ x↯ _) = ¬x↯ x↯
can-throw? (block x) B with can-throw? x B
... | yes x↯ = yes (Block x↯)
... | no ¬x↯ = no helper
  where
  helper : ¬ block x ↯[ B ]
  helper (Block x↯) = ¬x↯ x↯
can-throw? (unblock x) B with can-throw? x U
... | yes x↯ = yes (Unblock x↯)
... | no ¬x↯ = no helper
  where
  helper : ¬ unblock x ↯[ B ]
  helper (Unblock x↯) = ¬x↯ x↯

can-return? : ∀ (x : Expr total) i → Dec (x ↡[ i ])
can-return? ⌜ nat m ⌝ i = yes (m , Val)
can-return? ⌜ throw ⌝ i = no helper
  where
  helper : ¬ ⌜_⌝ {t = total} throw ↡[ i ]
  helper (_ , ())
can-return? (x ⊕ y) i with can-return? x i | can-return? y i
... | yes x⇓ | yes y⇓ = yes (zip-Σ _+_ Add₁ x⇓ y⇓)
... | no ¬x⇓ | _      = no helper
  where
  helper : ¬ x ⊕ y ↡[ i ]
  helper (._ , Add₁ x⇓ _) = ¬x⇓ (_ , x⇓)
... | _      | no ¬y⇓ = no helper
  where
  helper : ¬ x ⊕ y ↡[ i ]
  helper (._ , Add₁ _ y⇓) = ¬y⇓ (_ , y⇓)
can-return? (x >> y) i with can-return? x i | can-return? y i
... | yes x⇓ | yes y⇓ = yes (zip-Σ (λ m n → n) Seqn₁ x⇓ y⇓)
... | no ¬x⇓ | _      = no helper
  where
  helper : ¬ x >> y ↡[ i ]
  helper (_ , Seqn₁ x⇓ _) = ¬x⇓ (_ , x⇓)
... | _      | no ¬y⇓ = no helper
  where
  helper : ¬ x >> y ↡[ i ]
  helper (_ , Seqn₁ _ y⇓) = ¬y⇓ (_ , y⇓)
can-return? (x catch y) i with can-return? x i | can-return? y B
... | yes x⇓ | _      = yes (map-Σ₂ Catch₁ x⇓)
... | no ¬x⇓ | yes y⇓ = yes (map-Σ₂ (Catch₂ (cannot-return⇒can-throw ¬x⇓)) y⇓)
... | no ¬x⇓ | no ¬y⇓ = no helper
  where
  helper : ¬ x catch y ↡[ i ]
  helper (_ , Catch₁ x⇓)   = ¬x⇓ (_ , x⇓)
  helper (_ , Catch₂ _ y⇓) = ¬y⇓ (_ , y⇓)
can-return? (block x) i with can-return? x B
... | yes x⇓ = yes (map-Σ₂ Block x⇓)
... | no ¬x⇓ = no helper
  where
  helper : ¬ block x ↡[ i ]
  helper (_ , Block x⇓) = ¬x⇓ (_ , x⇓)
can-return? (unblock x) i with can-return? x U
... | yes x⇓ = yes (map-Σ₂ Unblock x⇓)
... | no ¬x⇓ = no helper
  where
  helper : ¬ unblock x ↡[ i ]
  helper (_ , Unblock x⇓) = ¬x⇓ (_ , x⇓)

-- Wraps up the results of some of the functions above.

data _Or_ (P Q : Set) : Set where
  both   : ( p :   P) ( q :   Q) → P Or Q
  first  : ( p :   P) (¬q : ¬ Q) → P Or Q
  second : (¬p : ¬ P) ( q :   Q) → P Or Q

decidable : ∀ (x : Expr total) i → (x ↡[ i ]) Or (x ↯[ i ])
decidable x i with can-return? x i | can-throw? x i
decidable x i | yes x↡ | yes x↯ = both    x↡  x↯
decidable x i | yes x↡ | no ¬x↯ = first   x↡ ¬x↯
decidable x i | no ¬x↡ | yes x↯ = second ¬x↡  x↯
decidable x i | no ¬x↡ | no ¬x↯ with defined x i
decidable x i | no ¬x↡ | no ¬x↯ | (nat n , x↡) = ⊥-elim (¬x↡ (n , x↡))
decidable x i | no ¬x↡ | no ¬x↯ | (throw , x↯) = ⊥-elim (¬x↯ x↯)

-- One could also decide whether or not an expression can yield a
-- _specific_ natural number. However, I think I have already taken
-- this exercise a bit too far.