content: {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  module Data.Abstract.Exception where
  
  import Data.GaloisConnection
  import Data.Hashable
  import Data.Order
  import Data.Set
  import Data.String
  
  import qualified Data.Concrete.Exception as Con
  import qualified Data.Concrete.Powerset as Con
  
  data Exception v = StaticException (Set String) | DynamicException v deriving (Eq)
  
  instance Show v => Show (Exception v) where
    show (StaticException s) = "Static: " ++ show s
    show (DynamicException v) = "Dynamic: " ++ show v
  
  instance PreOrd v => PreOrd (Exception v) where
    StaticException s1 ⊑ StaticException s2 = s1 ⊑ s2
    DynamicException _ ⊑ StaticException _ = True
    DynamicException v1 ⊑ DynamicException v2 = v1 ⊑ v2
    _ ⊑ _ = False
  
  instance LowerBounded v => LowerBounded (Exception v) where
    bottom = DynamicException bottom
  
  instance Complete v => Complete (Exception v) where
    StaticException s1 ⊔ StaticException s2 = StaticException $ s1 `union` s2
    StaticException s ⊔ _ = StaticException s
    _ ⊔ StaticException s = StaticException s
    DynamicException v1 ⊔ DynamicException v2 = DynamicException $ v1 ⊔ v2
  
  instance IsString (Exception v) where
    fromString = StaticException . singleton
  
  instance (Eq v, Hashable v, Complete v', Galois (Con.Pow v) v')
      => Galois (Con.Pow (Con.Exception v)) (Exception v') where
    alpha = lifted $ \e -> case e of
      Con.StaticException s -> fromString s
      Con.DynamicException v -> DynamicException $ alphaSing v
    gamma = error "noncomputable"
  