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

import Prelude hiding (traverse)
import qualified Data.Traversable as Traversable

import Language.Symantic
import Language.Symantic.Lib.Applicative (tyApplicative)
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.Functor (f2)

-- * Class 'Sym_Traversable'
type instance Sym Traversable = Sym_Traversable
class Sym_Traversable term where
	traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
	default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
	traverse = trans2 traverse

-- Interpreting
instance Sym_Traversable Eval where
	traverse = eval2 Traversable.traverse
instance Sym_Traversable View where
	traverse = view2 "traverse"
instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Dup r1 r2) where
	traverse = dup2 @Sym_Traversable traverse

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

-- Typing
instance NameTyOf Traversable where
	nameTyOf _c = ["Traversable"] `Mod` "Traversable"
instance FixityOf Traversable
instance ClassInstancesFor Traversable
instance TypeInstancesFor Traversable

-- Compiling
instance Gram_Term_AtomsFor src ss g Traversable
instance (Source src, SymInj ss Traversable) => ModuleFor src ss Traversable where
	moduleFor = ["Traversable"] `moduleWhere`
	 [ "traverse" := teTraversable_traverse
	 ]

-- ** 'Type's
tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a)
tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a

-- * 'Term's
teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))
teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse
	where
	t :: Source src => LenInj vs => KindInj (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
	t = tyVar "t" $ VarS $ VarS $ VarS varZ