{-# OPTIONS --safe  #-}
open import Level
open import Data.Sum
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Maybe using (just; Is-just; Maybe; nothing)
import Data.Maybe as Maybe
import Data.Maybe.Relation.Binary.Connected as Maybe
import Data.Maybe.Relation.Unary.Any as Maybe-Any
import Data.Maybe.Properties as Maybe
import Data.List as List
import Data.List.Relation.Binary.Pointwise as List
open import Data.List.Properties as List
open import Data.List hiding (length)
open import Data.List.NonEmpty using (List⁺)
import Data.List.NonEmpty as List⁺
open import Data.List.Relation.Binary.Prefix.Heterogeneous using (Prefix)
import Data.List.Relation.Binary.Prefix.Heterogeneous as Pref
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Pref

open import Function.Base

open import Relation.Binary.PropositionalEquality
open import Relation.Binary using (DecidableEquality; Symmetric)
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary as Binary

open import Partial-Map
open import Auxiliary-Definitions

module Apartness {i o : Level}
                 (I : Set i)
                 (O : Set o)
                 (_≟_ : DecidableEquality I)
                 (_≟o_ : DecidableEquality O) where


module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
  prefix-view? : Decidable R → Decidable (Pref.PrefixView R)
  prefix-view? dec-R short long = map′ Pref.toView Pref.fromView (Pref.prefix? dec-R short long)


module _ {a} {A : Set a} where
  ProperPrefix : List A → List A → Set a
  ProperPrefix v w = ∃[ z ](v ++ List⁺.toList z ≡ w)

  Proper⇒View : {l₁ l₂ : List A} → ProperPrefix l₁ l₂ → Pref.PrefixView _≡_ l₁ l₂
  Proper⇒View (z , eq) rewrite (sym eq) = Pref._++_ (List.refl refl) (List⁺.toList z)

  pointwise-≡ : {l₁ l₂ : List A} → List.Pointwise _≡_ l₁ l₂ → l₁ ≡ l₂
  pointwise-≡ List.[] = refl
  pointwise-≡ (x∼y List.∷ eq) rewrite x∼y rewrite (pointwise-≡ eq) = refl

  proper-prefix? : Decidable _≡_ → Binary.Decidable ProperPrefix
  proper-prefix? dec-≡ v w with (prefix-view? dec-≡ v w)
  ... | yes (eq Pref.++ x ∷ z) rewrite pointwise-≡ eq = yes ((x List⁺.∷ z) , refl)
  ... | yes (eq Pref.++ [])  rewrite pointwise-≡ eq = no (λ { (z , eq') →
                case (++-cancelˡ _ (List⁺.toList z) [] eq') of λ ()
                })
  ... | no bc = no λ { z → bc (Proper⇒View z) }

module Observation-Cache (f : List I ⇀ O) where
  -- apartness relation in the observation tree. It is crucial
  -- that the witness is non-empty. We only add the ε⊢ notation
  -- for readability.
  _ε⊢_#_ : List I → List I → List I → Set _
  z ε⊢ v # w =
      ∃[ o₁ ] ∃[ o₂ ]
      (f (v ++ z) ≡ just o₁)
      × (f (w ++ z) ≡ just o₂)
      × (o₁ ≢ o₂)
  -- I would have prefered to define _ε⊢_#_ as a record with
  -- a constructor named 'conflict', but then the pattern matching
  -- later does not automatically infer some of the equalities
  pattern conflict o₁ o₂ fo₁ fo₂ o₁≢o₂ = o₁ , o₂ , fo₁ , fo₂ , o₁≢o₂

  _⊢_#_ : List⁺ I → List I → List I → Set _
  z ⊢ v # w = (List⁺.toList z) ε⊢ v # w

  _#_ : List I → List I → Set _
  v # w = ∃[ z ](z ⊢ v # w)

  -- Compatibility for maybe-outputs:
  _∼ₒ_ : Maybe O → Maybe O → Set _
  o₁ ∼ₒ o₂ = Maybe.Connected _≡_ o₁ o₂
  -- ¬∼ₒ⇒≢ : ∀ o₁ o₂ → ¬ (o₁ ∼ₒ o₂) → (Is-just o₁ × Is-just o₂ × o₁ ≢ o₂)

  -- Two maybe-outputs are either compatible or they are both 'just' and different:
  ∼ₒ-dec² : ∀ o₁ o₂ → (o₁ ∼ₒ o₂) ⊎ (Is-just o₁ × Is-just o₂ × o₁ ≢ o₂)
  ∼ₒ-dec² o₁ o₂ with (Maybe.connected? _≟o_ o₁ o₂)
  ∼ₒ-dec² o₁ o₂ | yes witness = inj₁ witness
  ∼ₒ-dec² nothing (just _)    | no bc = ⊥-elim (bc Maybe.nothing-just)
  ∼ₒ-dec² nothing nothing     | no bc = ⊥-elim (bc Maybe.nothing)
  ∼ₒ-dec² (just _) nothing    | no bc = ⊥-elim (bc Maybe.just-nothing)
  ∼ₒ-dec² (just o₁) (just o₂) | no bc =
    inj₂ ((Maybe-Any.just tt) , ((Maybe-Any.just tt) , λ { refl → bc (Maybe.just refl)}))

  -- The complement of apartness: uncertain bisimulation ∼.
  -- Again, it is important that the witness 'z' must be non-empty
  _∼_ : List I → List I → Set _
  v ∼ w = ∀ z → f (v ++ List⁺.toList z) ∼ₒ f (w ++ List⁺.toList z)

  #-sym : Symmetric _#_
  #-sym {v} {w} (z , conflict o₁ o₂ fo₁ fo₂ neq) = z , conflict o₂ o₁ fo₂ fo₁ (≢-sym neq)

  #-irreflexive : ∀ {v} → ¬ (v # v)
  #-irreflexive {v} (z , conflict o₁ o₂ fo₁ fo₂ neq) =
    neq (Maybe.just-injective (trans (sym fo₁) fo₂))

  -- # is weakly co-transitive
  #-weakly-cotrans : ∀ {u v w z : List I}
              → (z ε⊢ v # w)
              → Is-just (f (u ++ z))
              → (z ε⊢ u # v) ⊎ (z ε⊢ u # w)
  #-weakly-cotrans {u} {v} {w} {z} (conflict fv fw eq-fvz eq-fwz o-v≢o-w) is-j with (f (u ++ z)) | is-j
  ... | nothing | ()
  ... | (just fu) | _ with (fu ≟o fv) | (fu ≟o fw)
  ...                 | no fu≢fv | _ = inj₁ (conflict fu fv refl eq-fvz fu≢fv)
  ...                 | _ | no fu≢fw = inj₂ (conflict fu fw refl eq-fwz fu≢fw)
  ...                 | yes fu≡fv | yes fu≡fw = ⊥-elim (o-v≢o-w (trans (sym fu≡fv) fu≡fw))

  -- not being apart implies compatiblity
  ¬#-to-∼ : ∀ {v} {w} → ¬ (v # w) → (v ∼ w)
  ¬#-to-∼ {v} {w} ¬# z with (∼ₒ-dec² _ _)
  ... | inj₁ witness = witness
  ... | inj₂ (j-fvz , j-fwz , ineq) =
        let
          o₁ , eq-o₁ = is-just-⇒-ret-just j-fvz -- TODO: turn 'is-just-⇒-ret-just' into a pattern
          o₂ , eq-o₂ = is-just-⇒-ret-just j-fwz
          open ≡-Reasoning
        in
        ⊥-elim (¬# (z , conflict o₁ o₂ eq-o₁ eq-o₂ λ o₁≡o₂ → ineq
          (begin
            f (v ++ _) ≡⟨ eq-o₁ ⟩
            _ ≡⟨ cong just o₁≡o₂ ⟩
            _ ≡⟨  sym eq-o₂ ⟩
            f (w ++ _)
          ∎)))

  ∼-refl : ∀ {v} → (v ∼ v)
  ∼-refl = ¬#-to-∼ #-irreflexive

  -- The converse direction holds, too:
  ∼-to-¬# : ∀ {v} {w} → (v ∼ w) → ¬ (v # w)
  ∼-to-¬# {v} {w} v∼w (z , conflict o₁ o₂ fv fw o₁≢o₂) with (v∼w z)
  ... | o₁∼ₒo₂ rewrite fv rewrite fw with (Maybe.just o₁≡o₂) ← o₁∼ₒo₂ =
    o₁≢o₂ o₁≡o₂


  -- a 'guarded' version:
  _#g_ : List I → List I → Set _
  v #g w = ∃[ u ] (Is-just (f u)) × ∃[ z ] (v ++ List⁺.toList z ≡ u) × (z ⊢ v # w)

  #g⇒# : ∀ {v} {w} → v #g w → v # w
  #g⇒# {v} {w} (u , _ , z , _ , z⊢v#w) = z , z⊢v#w

  #⇒#g : ∀ {v} {w} → v # w → v #g w
  #⇒#g {v} {w} (z , conflict o₁ o₂ fo₁ fo₂ o₁≢o₂) = (v ++ List⁺.toList z) , ret-just-⇒-is-just fo₁ , z , (refl , (conflict o₁ o₂ fo₁ fo₂ o₁≢o₂))

  ⊢#-dec : ∀ z v w → Dec (z ⊢ v # w)
  ⊢#-dec z v w with f (v ++ List⁺.toList z) in fv | f (w ++ List⁺.toList z) in fw
  ... | nothing | _ = no λ { () }
  ... | _ | nothing = no λ { () }
  ... | just o₁ | just o₂ with (o₁ ≟o o₂)
  ...               | yes eq = no λ { (conflict o1' o2' refl refl neq) → neq eq }
  ...               | no neq = yes (conflict o₁ o₂ refl refl neq)

  decide-guarded-part : ∀ v w u → Dec (∃[ z ] (v ++ List⁺.toList z ≡ u) × (z ⊢ v # w))
  decide-guarded-part v w u with (proper-prefix? _≟_ v u)
  ... | no v-not-pref-u = no (λ { (z , pref , _) → v-not-pref-u (z , pref) })
  ... | yes (z , z-prop) with (⊢#-dec z v w)
  ...         | (yes z⊢v#w) = yes (z , (z-prop , z⊢v#w))
  ...         | (no no-⊢#) = no (λ { (z' , refl , z'⊢v#w) →
              let
                z≡z' : List⁺.toList z ≡ List⁺.toList z'
                z≡z' = ++-cancelˡ v _ _ z-prop
                witness : z ⊢ v # w
                witness = subst (λ - → - ε⊢ v # w) (sym z≡z') z'⊢v#w
              in
              no-⊢# witness })

  module Decide-# {l : List (List I)} (dom : HasFiniteDomain f l) where
    #-dec : Binary.Decidable _#_
    #-dec v w = map′ #g⇒# #⇒#g (finite-domain-∃-dec f (decide-guarded-part v w) dom)

    ∼-dec : Binary.Decidable _∼_
    ∼-dec v w = map′ ¬#-to-∼ ∼-to-¬# (¬? (#-dec v w))

    #-dec² : ∀ v w → (v # w) ⊎ (v ∼ w)
    #-dec² v w with (#-dec v w)
    ... | (yes witness) = inj₁ witness
    ... | (no bc) = inj₂ (¬#-to-∼ bc)

module Observation-Cache-With-Explicit-f (f : List I ⇀ O) where
  open Observation-Cache renaming (_ε⊢_#_  to _⊧_ε⊢_#_; _⊢_#_ to _⊧_⊢_#_; _#_ to _⊧_#_) public

module Monotonicity {f g : List I ⇀ O} where
  open Observation-Cache-With-Explicit-f
  open Order⇀

  ε⊢#-monotone : f ⊑ g → ∀ z → _⊧_ε⊢_#_ f z ⇒ _⊧_ε⊢_#_ g z
  ε⊢#-monotone f⊑g z {x} {y} (conflict o-x o-y f-xz f-yz neq) =
    (conflict o-x o-y (⊑-elim f⊑g f-xz) (⊑-elim f⊑g f-yz) neq)

  ⊢#-monotone : f ⊑ g → ∀ z → _⊧_⊢_#_ f z ⇒ _⊧_⊢_#_ g z
  ⊢#-monotone f⊑g z {x} {y} x#y =
    ε⊢#-monotone f⊑g (List⁺.toList z) {x} {y} x#y

  #-monotone : f ⊑ g → _⊧_#_ f ⇒ _⊧_#_ g
  #-monotone f⊑g {x} {y} (z , x#y) =
    (z , ⊢#-monotone f⊑g z {x} {y} x#y)