{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Map'.
module Language.Symantic.Lib.Map where

import Data.Bool
import Data.Eq (Eq)
import Data.Foldable (Foldable)
import Data.Function (($))
import Data.Functor (Functor)
import Data.Map.Strict (Map)
import Data.Maybe (Maybe(..))
import Data.MonoTraversable (MonoFunctor)
import Data.Monoid (Monoid)
import Data.Ord (Ord)
import Data.Traversable (Traversable)
import Text.Show (Show)
import qualified Data.Map.Strict as Map

import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.List (tyList)
import Language.Symantic.Lib.Maybe (tyMaybe)
import Language.Symantic.Lib.MonoFunctor (Element)
import Language.Symantic.Lib.Ord (tyOrd)
import Language.Symantic.Lib.Tuple2 (tyTuple2)

-- * Class 'Sym_Map'
type instance Sym Map = Sym_Map
class Sym_Map term where
        map_fromList     :: Ord k => term [(k, a)] -> term (Map k a)
        map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
        map_lookup       :: Ord k => term k -> term (Map k a) -> term (Maybe a)
        map_keys         :: term (Map k a) -> term [k]
        map_member       :: Ord k => term k -> term (Map k a) -> term Bool
        map_insert       :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
        map_delete       :: Ord k => term k -> term (Map k a) -> term (Map k a)
        map_difference   :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
        map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b

        default map_fromList     :: Sym_Map (UnT term) => Trans term => Ord k => term [(k, a)] -> term (Map k a)
        default map_mapWithKey   :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b) -> term (Map k a) -> term (Map k b)
        default map_lookup       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Maybe a)
        default map_keys         :: Sym_Map (UnT term) => Trans term          => term (Map k a) -> term [k]
        default map_member       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term Bool
        default map_insert       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
        default map_delete       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Map k a)
        default map_difference   :: Sym_Map (UnT term) => Trans term => Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
        default map_foldrWithKey :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b

        map_fromList     = trans1 map_fromList
        map_mapWithKey   = trans2 map_mapWithKey
        map_lookup       = trans2 map_lookup
        map_keys         = trans1 map_keys
        map_member       = trans2 map_member
        map_insert       = trans3 map_insert
        map_delete       = trans2 map_delete
        map_difference   = trans2 map_difference
        map_foldrWithKey = trans3 map_foldrWithKey

-- Interpreting
instance Sym_Map Eval where
        map_fromList     = eval1 Map.fromList
        map_mapWithKey   = eval2 Map.mapWithKey
        map_lookup       = eval2 Map.lookup
        map_keys         = eval1 Map.keys
        map_member       = eval2 Map.member
        map_insert       = eval3 Map.insert
        map_delete       = eval2 Map.delete
        map_difference   = eval2 Map.difference
        map_foldrWithKey = eval3 Map.foldrWithKey
instance Sym_Map View where
        map_fromList     = view1 "Map.fromList"
        map_mapWithKey   = view2 "Map.mapWithKey"
        map_lookup       = view2 "Map.lookup"
        map_keys         = view1 "Map.keys"
        map_member       = view2 "Map.member"
        map_insert       = view3 "Map.insert"
        map_delete       = view2 "Map.delete"
        map_difference   = view2 "Map.difference"
        map_foldrWithKey = view3 "Map.foldrWithKey"
instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where
        map_fromList     = dup1 @Sym_Map map_fromList
        map_mapWithKey   = dup2 @Sym_Map map_mapWithKey
        map_lookup       = dup2 @Sym_Map map_lookup
        map_keys         = dup1 @Sym_Map map_keys
        map_member       = dup2 @Sym_Map map_member
        map_insert       = dup3 @Sym_Map map_insert
        map_delete       = dup2 @Sym_Map map_delete
        map_difference   = dup2 @Sym_Map map_difference
        map_foldrWithKey = dup3 @Sym_Map map_foldrWithKey

-- Transforming
instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)

-- Typing
instance NameTyOf Map where
        nameTyOf _c = ["Map"] `Mod` "Map"
instance FixityOf Map
instance ClassInstancesFor Map where
        proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
         | Just HRefl <- proj_ConstKiTy @_ @Map m
         = case () of
                 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
                   | Just Refl <- proj_Const @Foldable    q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
         | Just HRefl <- proj_ConstKiTy @_ @Map m
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
                   , Just Dict <- proveConstraint (tq`tyApp`k)
                   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
                   , Just Dict <- proveConstraint (tq`tyApp`k)
                   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Monoid q
                   , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
                   | Just Refl <- proj_Const @Show q
                   , Just Dict <- proveConstraint (tq`tyApp`k)
                   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Map where
        expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @Map m
         = Just a
        expandFamFor _c _len _fam _as = Nothing

-- Compiling
instance Gram_Term_AtomsFor src ss g Map
instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
        moduleFor = ["Map"] `moduleWhere`
         [ "delete"       := teMap_delete
         , "difference"   := teMap_difference
         , "foldrWithKey" := teMap_foldrWithKey
         , "fromList"     := teMap_fromList
         , "insert"       := teMap_insert
         , "keys"         := teMap_keys
         , "lookup"       := teMap_lookup
         , "mapWithKey"   := teMap_mapWithKey
         , "member"       := teMap_member
         ]

-- ** 'Type's
tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a

k1 :: Source src => LenInj vs => KindInj (K k) =>
     Type src (a ': Proxy k ': vs) k
k1 = tyVar "k" $ VarS varZ

k2 :: Source src => LenInj vs => KindInj (K k) =>
     Type src (a ': b ': Proxy k ': vs) k
k2 = tyVar "k" $ VarS $ VarS varZ

-- ** 'Term's
teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))
teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete

teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))
teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert

teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))
teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference

teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))
teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList

teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))
teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup

teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member

teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey

teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey

teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys