{-# OPTIONS --safe #-}
 
module Class.Computational where
 
open import Agda.Primitive using () renaming (Set to Type)
open import Level
 
open import Prelude.Init hiding (map)
 
open import Class.Applicative
open import Class.Bifunctor
open import Class.DecEq
open import Class.Functor renaming (fmap to map)
open import Class.Monad
open import Function
open import Relation.Binary.PropositionalEquality
 
private variable
  a : Level
  I O : Type
  i : I
  o o' : O
  Err Err₁ Err₂ : Type
 
data ComputationResult {a : Level} (Err : Type) (R : Type a) : Type a where
  success : R → ComputationResult Err R
  failure : Err → ComputationResult Err R
 
isFailure : ∀ {A : Type a} → ComputationResult Err A → Type a
isFailure x = ∃[ e ] x ≡ failure e
 
module _ {a b} {E : Type} {A : Type a} {B : Type b} where
  caseCR_∣_∣_ : (ma : ComputationResult E A) → (∀ {a} → ma ≡ success a → B) → (isFailure ma → B) → B
  caseCR ma ∣ f ∣ g with ma
  ... | success _ = f refl
  ... | failure e = g (e , refl)
 
  caseCR-success : ∀ {a} {ma : ComputationResult E A} {f : ∀ {a} → ma ≡ success a → B} {g : isFailure ma → B}
    → (eq : ma ≡ success a)
    → caseCR ma ∣ f ∣ g ≡ f eq
  caseCR-success refl = refl
 
  caseCR-failure : {ma : ComputationResult E A} {f : ∀ {a} → ma ≡ success a → B} {g : isFailure ma → B}
    → (eq : isFailure ma)
    → caseCR ma ∣ f ∣ g ≡ g eq
  caseCR-failure (_ , refl) = refl
 
instance
  Bifunctor-ComputationResult : ∀ {a : Level} → Bifunctor {_} {a} ComputationResult
  Bifunctor-ComputationResult .bimap _ f (success x) = success $ f x
  Bifunctor-ComputationResult .bimap f _ (failure x) = failure $ f x
 
  Functor-ComputationResult : ∀ {E : Type} → Functor (ComputationResult E)
  Functor-ComputationResult ._<$>_ f (success x) = success $ f x
  Functor-ComputationResult ._<$>_ _ (failure x) = failure x
 
  Applicative-ComputationResult : ∀ {E : Type} → Applicative (ComputationResult E)
  Applicative-ComputationResult .pure = success
  Applicative-ComputationResult ._<*>_ (success f) x = f <$> x
  Applicative-ComputationResult ._<*>_ (failure e) _ = failure e
 
  Monad-ComputationResult : ∀ {E : Type} → Monad (ComputationResult E)
  Monad-ComputationResult .return = success
  Monad-ComputationResult ._>>=_ (success a) m = m a
  Monad-ComputationResult ._>>=_ (failure e) _ = failure e
 
map-failure : ∀ {A B C : Type} {f : A → B} {x : C} {ma} → ma ≡ failure x → map f ma ≡ failure x
map-failure refl = refl
 
success-maybe : ∀ {R : Type} → ComputationResult Err R → Maybe R
success-maybe (success x) = just x
success-maybe (failure _) = nothing
 
failure-maybe : ∀ {R : Type} → ComputationResult Err R → Maybe Err
failure-maybe (success _) = nothing
failure-maybe (failure x) = just x
 
_≈ᶜʳ_ : ∀ {A} → ComputationResult Err A → ComputationResult Err A → Type
x ≈ᶜʳ y = success-maybe x ≡ success-maybe y
 
module _ (STS : I → O → Type) where
 
  ExtendedRel : I → ComputationResult Err O → Type
  ExtendedRel i (success o) = STS i o
  ExtendedRel i (failure _) = ∀ o → ¬ STS i o
 
  record Computational Err : Type₁ where
    constructor MkComputational
    field
      computeProof : (i : I) → ComputationResult Err (∃[ o ] STS i o)
 
    compute : I → ComputationResult Err O
    compute i = map proj₁ $ computeProof i
 
    field
      completeness : (i : I) → (o : O) → STS i o → compute i ≡ success o
 
    open ≡-Reasoning
 
    computeFail : I → Type
    computeFail i = isFailure $ compute i
 
    ≡-success⇔STS : compute i ≡ success o ⇔ STS i o
    ≡-success⇔STS {i} {o} with computeProof i in eq
    ... | success (o' , h) = mk⇔ (λ where refl → h) λ h' →
      begin success o' ≡˘⟨ completeness _ _ h ⟩
            compute i  ≡⟨ completeness _ _ h' ⟩
            success o  ∎
    ... | failure y = mk⇔ (λ ()) λ h →
      begin failure _ ≡˘⟨ map-failure eq ⟩
            compute i ≡⟨ completeness _ _ h ⟩
            success o ∎
 
    failure⇒∀¬STS : computeFail i → ∀ o → ¬ STS i o
    failure⇒∀¬STS comp≡nothing o h rewrite ≡-success⇔STS .Equivalence.from h =
      case comp≡nothing of λ ()
 
    ∀¬STS⇒failure : (∀ o → ¬ STS i o) → computeFail i
    ∀¬STS⇒failure {i = i} ¬sts with computeProof i
    ... | success (x , y) = ⊥-elim (¬sts x y)
    ... | failure y = (y , refl)
 
    failure⇔∀¬STS : computeFail i ⇔ ∀ o → ¬ STS i o
    failure⇔∀¬STS = mk⇔ failure⇒∀¬STS ∀¬STS⇒failure
 
    recomputeProof : STS i o → ComputationResult Err (∃[ o' ] STS i o')
    recomputeProof _ = computeProof _
 
module _ (STS : I → O → Type) ⦃ comp : Computational STS Err ⦄ where
 
  open Computational comp
 
  ExtendedRelSTS = ExtendedRel STS
 
  ExtendedRel-compute : ExtendedRelSTS i (compute i)
  ExtendedRel-compute {i} with compute i in eq
  ... | success o = Equivalence.to ≡-success⇔STS eq
  ... | failure _ = λ o h → case trans (sym $ Equivalence.from ≡-success⇔STS h) eq of λ ()
 
  open ≡-Reasoning
 
  ExtendedRel-rightUnique : ExtendedRelSTS i o → ExtendedRelSTS i o' → _≈ᶜʳ_ {Err = Err} o o'
  ExtendedRel-rightUnique {o = success x} {success x'} h h'
    with trans (sym $ Equivalence.from ≡-success⇔STS h) (Equivalence.from ≡-success⇔STS h')
  ... | refl = refl
 
  ExtendedRel-rightUnique {o = success x} {failure _}  h h' = ⊥-elim $ h' x h
  ExtendedRel-rightUnique {o = failure _} {success x'} h h' = ⊥-elim $ h x' h'
  ExtendedRel-rightUnique {o = failure a} {failure b}  h h' = refl
 
  computational⇒rightUnique : STS i o → STS i o' → o ≡ o'
  computational⇒rightUnique h h' with ExtendedRel-rightUnique h h'
  ... | refl = refl
 
  Computational⇒Dec : ⦃ _ : DecEq O ⦄ → Dec (STS i o)
  Computational⇒Dec {i} {o}
    with compute i | ExtendedRel-compute {i}
  ... | failure _ | ExSTS = no (ExSTS o)
  ... | success x | ExSTS with x ≟ o
  ... | no ¬p     = no  λ h → ¬p $ sym $ computational⇒rightUnique h ExSTS
  ... | yes refl  = yes ExSTS
 
module _ {STS : I → O → Type} (comp comp' : Computational STS Err) where
 
  open Computational comp  renaming (compute to compute₁)
  open Computational comp' renaming (compute to compute₂)
 
  compute-ext≡ : compute₁ i ≈ᶜʳ compute₂ i
  compute-ext≡ = ExtendedRel-rightUnique _ ⦃ comp ⦄
    (ExtendedRel-compute _ ⦃ comp ⦄) (ExtendedRel-compute _ ⦃ comp' ⦄)
 
open Computational ⦃...⦄
 
Computational⇒Dec' :
  {STS : I → O → Type} ⦃ comp : Computational STS Err ⦄ → Dec (∃[ o ] STS i o)
Computational⇒Dec' with computeProof _ in eq
... | success x = yes x
... | failure x = no λ (_ , h) → failure⇒∀¬STS (-, cong (map proj₁) eq) _ h
 
record InjectError Err₁ Err₂ : Type where
  field injectError : Err₁ → Err₂
 
open InjectError
 
instance
  InjectError-⊥ : InjectError ⊥ Err
  InjectError-⊥ = λ where
    .injectError ()
 
  InjectError-Id : InjectError Err Err
  InjectError-Id = λ where
    .injectError → id