module Language.Symantic.Lib.MonoFunctor where
import Data.MonoTraversable (MonoFunctor)
import qualified Data.MonoTraversable as MT
import Language.Symantic
import Language.Symantic.Lib.Function ()
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 (TyApp _ (TyApp _ 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
famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)
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
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
instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
instance NameTyOf MonoFunctor where
nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor"
instance FixityOf MonoFunctor
instance ClassInstancesFor MonoFunctor
instance TypeInstancesFor MonoFunctor
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
]
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
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