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

import Data.Map.Strict (Map)
import Data.MonoTraversable (MonoFunctor)
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 FixityOf Map
instance ClassInstancesFor Map where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
	 | Just HRefl <- proj_ConstKiTy @_ @Map c
	 = 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 _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))
	 | Just HRefl <- proj_ConstKiTy @_ @Map c
	 = 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 (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @Map c
	 = 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