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

import Data.MonoTraversable (MonoFunctor)
import qualified Data.MonoTraversable as MT

import Language.Symantic
import Language.Symantic.Lib.Function ()

-- * Type 'Element'
data Element
type instance Fam Element '[h] = MT.Element (UnProxy h)
instance NameTyOf Element where
	nameTyOf _c = ["MonoFunctor"] `Mod` "Element"
instance ClassInstancesFor Element
instance TypeInstancesFor Element where
	expandFamFor _c _len f (z:@_ty_r:@ a `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @(->) z
	 = Just a
	expandFamFor _c _len _fam _as = Nothing

-- ** 'Type's
famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)

-- * Class 'Sym_MonoFunctor'
type instance Sym MonoFunctor = Sym_MonoFunctor
class Sym_MonoFunctor term where
	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
	default omap ::
	 Sym_MonoFunctor (UnT term) =>
	 Trans term =>
	 MonoFunctor o =>
	 term (MT.Element o -> MT.Element o) -> term o -> term o
	omap = trans2 omap

-- Interpreting
instance Sym_MonoFunctor Eval where
	omap = eval2 MT.omap
instance Sym_MonoFunctor View where
	omap = view2 "omap"
instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Dup r1 r2) where
	omap = dup2 @Sym_MonoFunctor omap

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

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

-- Compiling
instance Gram_Term_AtomsFor src ss g MonoFunctor
instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where
	moduleFor = ["MonoFunctor"] `moduleWhere`
	 [ "omap" := teMonoFunctor_omap
	 ]

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

o0 :: Source src => LenInj vs => KindInj (K o) =>
     Type src (Proxy o ': vs) o
o0 = tyVar "o" varZ

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

-- ** 'Term's
teMonoFunctor_omap :: TermDef MonoFunctor '[Proxy o, Proxy e] (MonoFunctor o # e #~ MT.Element o #> ((e -> e) -> o -> o))
teMonoFunctor_omap = Term (tyMonoFunctor o0 # e1 #~ famElement o0) ((e1 ~> e1) ~> o0 ~> o0) $ teSym @MonoFunctor $ lam2 omap