content: {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE DeriveTraversable #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE OverloadedStrings #-}
  module Data.Abstract.Terminating where
  
  import Control.Arrow hiding (ArrowMonad)
  import Control.Arrow.Monad
  import Control.Monad
  import Control.Applicative
  import Control.DeepSeq
  
  import Data.Profunctor
  import Data.Order
  import Data.Hashable
  import Data.Abstract.Stable
  import Data.Abstract.Widening
  import Prettyprinter
  
  import GHC.Generics
  
  -- Free cocompletion of a type
  data Terminating a = NonTerminating | Terminating a deriving (Eq,Functor,Traversable,Foldable,Generic)
  instance NFData a => NFData (Terminating a)
  
  instance Pretty a => Show (Terminating a) where
    show = show . pretty
  
  instance Pretty a => Pretty (Terminating a) where
    pretty NonTerminating = "NonTerminating"
    pretty (Terminating a) = pretty a
  
  instance Hashable a => Hashable (Terminating a)
  
  instance Applicative Terminating where
    pure = Terminating
    (<*>) = ap
    {-# INLINE pure #-}
    {-# INLINE (<*>) #-}
  
  instance Monad Terminating where
    return = pure
    Terminating x >>= k = k x
    NonTerminating >>= _ = NonTerminating
    {-# INLINE return #-}
    {-# INLINE (>>=) #-}
  
  instance (ArrowChoice c, Profunctor c) => ArrowFunctor Terminating c where
    mapA f = lmap toEither (arr (\() -> NonTerminating) ||| rmap Terminating f)
    -- mapA f = proc t -> case t of
    --   Terminating x -> rmap Terminating f -< x
    --   NonTerminating -> returnA -< NonTerminating
    {-# INLINE mapA #-}
  
  instance (ArrowChoice c, Profunctor c) => ArrowMonad Terminating c where
    mapJoinA f = lmap toEither (arr (\() -> NonTerminating) ||| f)
    -- mapJoinA f = proc t -> case t of
    --   Terminating x -> f -< x
    --   NonTerminating -> returnA -< NonTerminating
    {-# INLINE mapJoinA #-}
  
  toEither :: Terminating a -> Either () a
  toEither (Terminating a) = Right a
  toEither NonTerminating = Left ()
  {-# INLINE toEither #-}
  
  instance PreOrd a => PreOrd (Terminating a) where
    NonTerminating ⊑ _ = True
    Terminating a ⊑ Terminating b = a ⊑ b
    _ ⊑ _ = False
  
    NonTerminating ≈ NonTerminating = True
    Terminating a ≈ Terminating b = a ≈ b
    _ ≈ _ = False
  
  instance Complete a => Complete (Terminating a) where
    Terminating a ⊔ Terminating b = Terminating (a ⊔ b) 
    x ⊔ NonTerminating = x
    NonTerminating ⊔ y = y
  
  -- instance CoComplete a => CoComplete (Terminating a) where
  --   Terminating a ⊓ Terminating b = Terminating (a ⊓ b) 
  --   NonTerminating ⊓ _ = NonTerminating
  --   _ ⊓ NonTerminating = NonTerminating
  
  instance UpperBounded a => UpperBounded (Terminating a) where
    top = Terminating top
  
  instance PreOrd a => LowerBounded (Terminating a) where
    bottom = NonTerminating
  
  widening :: Widening a -> Widening (Terminating a)
  widening _ NonTerminating NonTerminating = (Stable,NonTerminating)
  widening _ NonTerminating (Terminating b) = (Unstable,Terminating b)
  widening _ (Terminating a) NonTerminating = (Unstable,Terminating a)
  widening w (Terminating a) (Terminating b) = second Terminating (w a b)
  
  instance Num a => Num (Terminating a) where
    (+) = liftA2 (+)
    (*) = liftA2 (*)
    negate = fmap negate
    abs = fmap abs
    signum = fmap signum
    fromInteger = pure . fromInteger
  
  instance Fractional a => Fractional (Terminating a) where
    (/) = liftA2 (/)
    fromRational = pure . fromRational
  
  fromTerminating :: a -> Terminating a -> a
  fromTerminating _ (Terminating a) = a
  fromTerminating a NonTerminating = a
  {-# INLINE fromTerminating #-}
  
  toMaybe :: Terminating a -> Maybe a
  toMaybe (Terminating a) = Just a
  toMaybe NonTerminating = Nothing
  {-# INLINE toMaybe #-}
  