{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Abstract.Constructor(Constr,isEmpty,isSingleton,widening) where

import           Control.DeepSeq

import           Data.Order
import           Data.Hashable
import           Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import           Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import           Data.Text (Text)
import           Data.Identifiable
import           Data.Abstract.Widening
import           Data.Abstract.Stable

import           GHC.Exts

newtype Constr n = Constr (HashMap Text (IntMap [n])) deriving (Eq,Hashable,NFData)

instance (Identifiable n, Complete n, Show n) => Show (Constr n) where
  show cs = show (toList cs)

instance PreOrd n => PreOrd (Constr n) where
  Constr m1 ⊑ Constr m2 =
   (m1 `subsetKeys` m2) && forAll (M.intersectionWith (,) m1 m2) (\(a1,a2) ->
     (a1 `subsetKeys'` a2) && forAll (IM.intersectionWith (,) a1 a2) (\(ts1,ts2) ->
        ts1 ⊑ ts2))

instance Complete n => Complete (Constr n) where
  Constr m1 ⊔ Constr m2 = Constr (M.unionWith (IM.unionWith (zipWith (⊔))) m1 m2)

widening :: (Complete n) => Widening n -> Widening (Constr n)
widening w c1@(Constr m1) c2@(Constr m2) =
  let c3 = Constr (M.unionWith (IM.unionWith (zipWith (\x y -> snd (w x y)))) m1 m2)
  in (if c3 ⊑ c1 && c3 ⊑ c2 then Stable else Unstable, c3)

instance PreOrd n => LowerBounded (Constr n) where
  bottom = Constr M.empty

instance CoComplete n => CoComplete (Constr n) where
  Constr m1 ⊓ Constr m2 = removeEmpty $ Constr (M.intersectionWith (IM.intersectionWith (zipWith (⊓))) m1 m2)

instance (Identifiable n, Complete n) => IsList (Constr n) where
  type Item (Constr n) = (Text,[n])
  fromList l = Constr $ M.fromListWith (IM.unionWith (zipWith (⊔))) [ (c, IM.singleton (length ts) ts) | (c,ts) <- l]
  toList (Constr n) = [ (c,ts) | (c,tss) <- M.toList n, ts <- IM.elems tss ]

isEmpty :: Constr n -> Bool
isEmpty (Constr n) = M.null n

isSingleton :: (n -> Bool) -> Constr n -> Bool
isSingleton isSing (Constr n) = M.size n == 1 && forAll n (\a -> IM.size a == 1 && forAll a (all isSing))

-- size :: (Identifiable n, Complete n) => Constr n -> Int
-- size c = length (toList c)

removeEmpty :: Constr n -> Constr n
removeEmpty (Constr m) = Constr (M.mapMaybe (\a -> if IM.null a then Nothing else Just a) m)

forAll :: Foldable t => t a -> (a -> Bool) -> Bool
forAll l p = all p l

subsetKeys :: Identifiable a => HashMap a b -> HashMap a b' -> Bool
subsetKeys m1 m2 = all (`M.member` m2) (M.keys m1)

subsetKeys' :: IntMap a -> IntMap a' -> Bool
subsetKeys' m1 m2 = all (`IM.member` m2) (IM.keys m1)
