------------------------------------------------------------------------
-- Some algebraic properties
------------------------------------------------------------------------

module AlgebraicProperties where

open import Syntax
open import Semantics.BigStep
open import Equivalence
open import StatusLemmas
open import Totality

open import Relation.Nullary
open import Data.Product
open import Algebra
import Algebra.FunctionProperties as AlgProp
private
  open module AP (t : Totality) = AlgProp (≈-setoid t)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties as ℕ
open import Data.Empty

------------------------------------------------------------------------
-- A lemma

cast : ∀ {n₁ n₂ i t} {x : Expr t} →
       n₁ ≡ n₂ → x ⇓[ i ] nat n₁ → x ⇓[ i ] nat n₂
cast ≡-refl x = x

------------------------------------------------------------------------
-- Associativity

-- These properties show that the fixity declarations make sense.

-- _⊕_ is associative.

⊕-assoc : ∀ {t} → Associative t _⊕_
⊕-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑
  where
  assoc = CommutativeSemiring.+-assoc ℕ.commutativeSemiring

  ⟶⇓ : (x ⊕ y) ⊕ z ⊑⇓ x ⊕ (y ⊕ z)
  ⟶⇓ Int                 = Int
  ⟶⇓ (Add₃ (Add₁ x y) z) = Add₃ x (Add₃ y z)
  ⟶⇓ (Add₂ Int)          = Int
  ⟶⇓ (Add₂ (Add₃ x y))   = Add₃ x (Add₂ y)
  ⟶⇓ (Add₂ (Add₂ x))     = Add₂ x
  ⟶⇓ {i = i} (Add₁ {n = n₃} (Add₁ {m = n₁} {n = n₂} x⇓ y⇓) z⇓) =
     cast (≡-sym (assoc n₁ n₂ n₃)) (Add₁ x⇓ (Add₁ y⇓ z⇓))

  ⟵⇓ : x ⊕ (y ⊕ z) ⊑⇓ (x ⊕ y) ⊕ z
  ⟵⇓ Int                 = Int
  ⟵⇓ (Add₃ x Int)        = Int
  ⟵⇓ (Add₃ x (Add₂ y))   = Add₂ (Add₃ x y)
  ⟵⇓ (Add₃ x (Add₃ y z)) = Add₃ (Add₁ x y) z
  ⟵⇓ (Add₂ x)            = Add₂ (Add₂ x)
  ⟵⇓ {i = i} (Add₁ {m = n₁} x⇓ (Add₁ {m = n₂} {n = n₃} y⇓ z⇓)) =
     cast (assoc n₁ n₂ n₃) (Add₁ (Add₁ x⇓ y⇓) z⇓)

  ⟶⇑ : (x ⊕ y) ⊕ z ⊑⇑ x ⊕ (y ⊕ z)
  ⟶⇑ (Add₁ (Add₁ x⇑))            = Add₁ x⇑
  ⟶⇑ (Add₁ (Add₂ x↡ y⇑))         = Add₂ x↡ (Add₁ y⇑)
  ⟶⇑ (Add₂ (._ , Add₁ x↡ y↡) z⇑) = Add₂ (_ , x↡) (Add₂ (_ , y↡) z⇑)

  ⟵⇑ : x ⊕ (y ⊕ z) ⊑⇑ (x ⊕ y) ⊕ z
  ⟵⇑ (Add₁ x⇑)              = Add₁ (Add₁ x⇑)
  ⟵⇑ (Add₂ x↡ (Add₁ y⇑))    = Add₁ (Add₂ x↡ y⇑)
  ⟵⇑ (Add₂ x↡ (Add₂ y↡ z⇑)) = Add₂ (zip-Σ _+_ Add₁ x↡ y↡) z⇑

-- _catch_ is "left associative".

catch-assocˡ : ∀ {t} (x y z : Expr t) →
               x catch (y catch z) ⊑ (x catch y) catch z
catch-assocˡ x y z = record { ⇓ = ⇓; ⇑ = ⇑ }
  where
  ⇓ : x catch (y catch z) ⊑⇓ (x catch y) catch z
  ⇓ (Catch₁ x⇓)               = Catch₁ (Catch₁ x⇓)
  ⇓ (Catch₂ x↯ (Catch₁ y⇓))   = Catch₁ (Catch₂ x↯ y⇓)
  ⇓ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z
  ⇓ Int                       = Int

  ⇑ : x catch (y catch z) ⊑⇑ (x catch y) catch z
  ⇑ (Catch₁ x⇑)                = Catch₁ (Catch₁ x⇑)
  ⇑ (Catch₂ x↯ (Catch₁ y⇑))    = Catch₁ (Catch₂ x↯ y⇑)
  ⇑ (Catch₂ x↯ (Catch₂ y↯ z⇑)) = Catch₂ (Catch₂ x↯ y↯) z⇑

-- _catch_ is not associative.

¬catch-assoc : ∀ {t} → ¬ Associative t _catch_
¬catch-assoc assoc
  with _⊑_.⇓ (_≈_.⊑ (assoc ⌜ throw ⌝ ⌜ nat  ⌝ ⌜ nat  ⌝))
             {i = U} (Catch₂ Int Val)
¬catch-assoc assoc | Catch₁ ()
¬catch-assoc assoc | Catch₂ x↯ (Catch₁ ())
¬catch-assoc assoc | Catch₂ x↯ (Catch₂ () y⇓)

-- _>>_ is associative.

>>-assoc : ∀ {t} → Associative t _>>_
>>-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑
  where
  ⟶⇓ : (x >> y) >> z ⊑⇓ x >> (y >> z)
  ⟶⇓ (Seqn₁ (Seqn₁ x⇓ y⇓) z) = Seqn₁ x⇓ (Seqn₁ y⇓ z)
  ⟶⇓ (Seqn₂ (Seqn₁ x⇓ y↯))   = Seqn₁ x⇓ (Seqn₂ y↯)
  ⟶⇓ (Seqn₂ (Seqn₂ x↯))      = Seqn₂ x↯
  ⟶⇓ (Seqn₂ Int)             = Int
  ⟶⇓ Int                     = Int

  ⟵⇓ : x >> (y >> z) ⊑⇓ (x >> y) >> z
  ⟵⇓ (Seqn₁ x⇓ (Seqn₁ y⇓ z)) = Seqn₁ (Seqn₁ x⇓ y⇓) z
  ⟵⇓ (Seqn₁ x⇓ (Seqn₂ y↯))   = Seqn₂ (Seqn₁ x⇓ y↯)
  ⟵⇓ (Seqn₁ x↯ Int)          = Int
  ⟵⇓ (Seqn₂ x↯)              = Seqn₂ (Seqn₂ x↯)
  ⟵⇓ Int                     = Int

  ⟶⇑ : (x >> y) >> z ⊑⇑ x >> (y >> z)
  ⟶⇑ (Seqn₁ (Seqn₁ x⇑))           = Seqn₁ x⇑
  ⟶⇑ (Seqn₁ (Seqn₂ x↡ y⇑))        = Seqn₂ x↡ (Seqn₁ y⇑)
  ⟶⇑ (Seqn₂ (_ , Seqn₁ x↡ y↡) z⇑) = Seqn₂ (_ , x↡) (Seqn₂ (_ , y↡) z⇑)

  ⟵⇑ : x >> (y >> z) ⊑⇑ (x >> y) >> z
  ⟵⇑ (Seqn₁ x⇑)               = Seqn₁ (Seqn₁ x⇑)
  ⟵⇑ (Seqn₂ x↡ (Seqn₁ y⇑))    = Seqn₁ (Seqn₂ x↡ y⇑)
  ⟵⇑ (Seqn₂ x↡ (Seqn₂ y↡ z⇑)) = Seqn₂ (zip-Σ (λ u v → v) Seqn₁ x↡ y↡) z⇑

-- _finally_ is "right associative".

finally-assocʳ : ∀ {t} (x y z : Expr t) →
                 (x finally y) finally z ⊑ x finally (y finally z)
finally-assocʳ x y z = record { ⇓ = ⇓; ⇑ = ⇑ }
  where
  ⇓ : (x finally y) finally z ⊑⇓ x finally (y finally z)
  ⇓ Int = Int
  ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇒)) =
    Block (Seqn₁ (Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇓ y↡))) z⇒)))
  ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _))
  ⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))
  ⇓ (Block (Seqn₂ (Catch₂ _ z↯))) =
    Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ (Block (Seqn₂ (Catch₂ (Unblock Int) z↯))))))

  ⇑ : (x finally y) finally z ⊑⇑ x finally (y finally z)
  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x⇑))))))) =
    Block (Seqn₁ (Catch₁ x⇑))
  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ x↯ (Seqn₁ y⇑)))))))) =
    Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑))))))))
  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ()))))))))
  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₁ x↡) y⇑)))))) =
    Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑))))))
  ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _))))))
  ⇑ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑)))) =
    Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑)))))))
  ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ()))))
  ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↯))) (Seqn₁ z⇑)))) =
    Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑)))))
  ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))) _)))
  ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₁ y↡ _))))) (Seqn₁ z⇑)))) =
    Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑)))))
  ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₂ y↯))))) (Seqn₁ z⇑)))) =
    Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑)))))))
  ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇑)) =
    Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑)))
  ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _))
  ⇑ (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _))

-- In a partial setting _finally_ is not associative (c.f.
-- StatusLemmas.¬UtoB').

¬finally-assoc : ¬ Associative partial _finally_
¬finally-assoc assoc
  with _⊑_.⇓ (_≈_.⊒ (assoc ⌜ nat  ⌝ (loop ⌜ nat  ⌝ catch ⌜ nat  ⌝) ⌜ nat  ⌝))
         {i = U}
         (Block (Seqn₁ (Catch₁ (Unblock Val))
                       (Block (Seqn₁ (Catch₁ (Unblock (Catch₂ Int Val)))
                                     Val))))
... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ ↡)))))   Val) = loop-¬⇓ nat-¬↯ (, ↡)
... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ ↯ _))))) Val) = loop-¬⇓ nat-¬↯ (, ↯)
... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)
... | Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)

-- In a total setting _finally_ is associative.

finally-assoc : Associative total _finally_
finally-assoc x y z = record { ⊑ = finally-assocʳ x y z
                             ; ⊒ = record { ⇓ = ⟵⇓; ⇑ = ⟵⇑ } }
  where
  ⟵⇓ : x finally (y finally z) ⊑⇓ (x finally y) finally z
  ⟵⇓ Int = Int

  ⟵⇓ (Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock y)) z)))) =
    Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x) y')))) z)
    where y' = proj₂ (Uto·' (_ , y))
  ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))))
  ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₂ (Catch₂ _ z↯)))))         = Block (Seqn₂ (Catch₂ (Unblock Int) z↯))
  ⟵⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))

  ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _))))         = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Val)))
  ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₁ _ z))))))           = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ z)))
  ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₂ (Catch₂ _ z↯))))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯))

  ⟵⇑ : x finally (y finally z) ⊑⇑ (x finally y) finally z
  ⟵⇑ ⇑ = ⊥-elim (¬undefined _ ⇑)

------------------------------------------------------------------------
-- Commutativity

-- _⊕_ is commutative if the language is total.

⊕-comm : Commutative total _⊕_
⊕-comm x y = is-≈ (⟶⇓ _) (⟶⇓ _) ⟶⇑ ⟶⇑
  where
  comm = CommutativeSemiring.+-comm ℕ.commutativeSemiring

  ⟶⇓ : ∀ {x} y → x ⊕ y ⊑⇓ y ⊕ x
  ⟶⇓ _         Int                          = Int
  ⟶⇓ _         (Add₃ x⇓ y↯)                 = Add₂ y↯
  ⟶⇓ y {i = i} (Add₂ x↯)                    with defined y i
  ⟶⇓ _         (Add₂ x↯)                    | (nat _ , y⇓) = Add₃ y⇓ x↯
  ⟶⇓ _         (Add₂ x↯)                    | (throw , y↯) = Add₂ y↯
  ⟶⇓ _         (Add₁ {m = m} {n = n} x⇓ y⇓) =
    cast (≡-sym (comm m n)) (Add₁ y⇓ x⇓)

  ⟶⇑ : {x y : Expr total} → x ⊕ y ⊑⇑ y ⊕ x
  ⟶⇑ ⇑ = ⊥-elim (¬undefined _ ⇑)

-- _⊕_ is not commutative if the language is partial.

¬⊕-comm : ¬ Commutative partial _⊕_
¬⊕-comm ⊕-comm
  with _⊑_.⇓ (_≈_.⊑ (⊕-comm ⌜ throw ⌝ (loop ⌜ nat  ⌝)))
             {i = B} (Add₂ Val)
... | Add₂ ↡   = loop-¬⇓ nat-¬↯ (, ↡)
... | Add₃ ↯ _ = loop-¬⇓ nat-¬↯ (, ↯)