content: {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  module Data.Abstract.Error where
  
  import Control.Arrow hiding (ArrowMonad,(<+>))
  import Control.Arrow.Monad
  import Control.Monad
  import Control.Monad.Except
  import Control.DeepSeq
  
  import Data.String
  import Data.Profunctor
  import Data.Bifunctor hiding (second)
  import Data.Hashable
  import Data.Order
  import Data.GaloisConnection
  import Data.Concrete.Powerset as C
  import Data.Identifiable
  import qualified Data.Concrete.Error as C
  import Prettyprinter
  
  import Data.Abstract.FreeCompletion (FreeCompletion(..))
  import Data.Abstract.Widening
  import Data.Abstract.Stable
  
  import GHC.Generics (Generic, Generic1)
  
  -- | Error is an Either-like type with the ordering Success ⊑ Failure.
  data Error e a = Fail e | Success a
    deriving (Eq, Functor, Generic, Generic1, NFData, NFData1)
  
  instance (Show e,Show a) => Show (Error e a) where
    show (Fail e) = "Error " ++ show e
    show (Success a) = show a
  
  instance (Pretty e, Pretty a) => Pretty (Error e a) where
    pretty (Fail e) = "Error" <+> pretty e
    pretty (Success a) = pretty a
  
  instance (Hashable e, Hashable a) => Hashable (Error e a) where
    hashWithSalt s (Fail e)  = s `hashWithSalt` (0::Int) `hashWithSalt` e
    hashWithSalt s (Success a) = s `hashWithSalt` (1::Int) `hashWithSalt`  a
  
  instance Bifunctor Error where
    bimap f g x = case x of
      Fail e -> Fail (f e)
      Success a -> Success (g a)
  
  instance MonadError e (Error e) where
    throwError = Fail
    catchError (Fail e) f = f e
    catchError (Success a) _ = Success a
  
  instance IsString e => MonadFail (Error e) where
    fail e = Fail (fromString e)
  
  instance Applicative (Error e) where
    pure = Success
    (<*>) = ap
    {-# INLINE pure #-}
    {-# INLINE (<*>) #-}
  
  instance Monad (Error e) where
    return = pure
    Fail e >>= _ = Fail e
    Success a >>= k = k a
    {-# INLINE return #-}
    {-# INLINE (>>=) #-}
  
  instance (ArrowChoice c, Profunctor c) => ArrowFunctor (Error e) c where
    mapA f = lmap toEither (arr Fail ||| rmap Success f)
    {-# INLINE mapA #-}
  
  instance (ArrowChoice c, Profunctor c) => ArrowMonad (Error e) c where
    mapJoinA f = lmap toEither (arr Fail ||| f)
    {-# INLINE mapJoinA #-}
  
  instance (PreOrd e, PreOrd a) => PreOrd (Error e a) where
    Success x ⊑ Success y = x ⊑ y
    Success _ ⊑ Fail _  = True
    Fail x ⊑ Fail y = x ⊑ y
    _ ⊑ _ = False
  
    Fail x ≈ Fail y = x ≈ y
    Success x ≈ Success y = x ≈ y
    _ ≈ _ = False
  
  instance (Complete e,Complete a) => Complete (Error e a) where
    (⊔) = toJoin2 widening (⊔) (⊔)
  
  widening :: Widening e -> Widening a -> Widening (Error e a)
  widening we _ (Fail a) (Fail b) = second Fail (a `we` b)
  widening _ wa (Success a) (Success b) = second Success (a `wa` b)
  widening _ _ (Fail a) (Success _) = (Unstable ,Fail a)
  widening _ _ (Success _) (Fail b) = (Unstable ,Fail b)
  
  instance (CoComplete e,CoComplete a) => CoComplete (Error e a) where
    Fail x ⊓ Fail y = Fail (x ⊓ y)
    Fail _ ⊓ Success y = Success y
    Success x ⊓ Fail _ = Success x
    Success x ⊓ Success y = Success (x ⊓ y)
  
  instance (PreOrd a, UpperBounded e) => UpperBounded (Error e a) where
    top = Fail top
  
  instance (PreOrd e, LowerBounded a) => LowerBounded (Error e a) where
    bottom = Success bottom
  
  instance (PreOrd e, PreOrd a, Complete (FreeCompletion e), Complete (FreeCompletion a)) => Complete (FreeCompletion (Error e a)) where
    Lower m1 ⊔ Lower m2 = case (bimap Lower Lower m1 ⊔ bimap Lower Lower m2) of
      Fail (Lower e) -> Lower (Fail e)
      Success (Lower a) -> Lower (Success a)
      _ -> Top
    _ ⊔ _ = Top
  
  instance (Identifiable a, Identifiable e, Complete e', Complete a', Galois (C.Pow e) e', Galois (C.Pow a) a')
      => Galois (C.Pow (C.Error e a)) (Error e' a') where
    alpha = lifted $ \er -> case er of
      C.Fail e -> Fail (alphaSing e)
      C.Success y -> Success (alphaSing y)
    gamma (Fail e) = C.Fail <$> gamma e
    gamma (Success x) = C.Success <$> gamma x
  
  fromError :: a -> Error e a -> a
  fromError _ (Success a) = a
  fromError a (Fail _) = a
  
  fromEither :: Either e a -> Error e a
  fromEither (Left e) = Fail e
  fromEither (Right a) = Success a
  
  toEither :: Error e a -> Either e a
  toEither (Fail e) = Left e
  toEither (Success a) = Right a
  {-# INLINE toEither #-}
  
  fromMaybe :: Maybe a -> Error () a
  fromMaybe Nothing = Fail ()
  fromMaybe (Just a) = Success a
  
  toMaybe :: Error e a -> Maybe a
  toMaybe (Fail _) = Nothing
  toMaybe (Success a) = Just a
  