symantic-lib/Language/Symantic/Lib/MonoFunctor.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'MonoFunctor'.
   4 module Language.Symantic.Lib.MonoFunctor where
   5
   6 import Data.MonoTraversable (MonoFunctor)
   7 import qualified Data.MonoTraversable as MT
   8
   9 import Language.Symantic
  10 import Language.Symantic.Lib.Function ()
  11
  12 -- * Type 'Element'
  13 data Element
  14 type instance Fam Element '[h] = MT.Element (UnProxy h)
  15 instance ClassInstancesFor Element
  16 instance TypeInstancesFor Element where
  17         expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)
  18          | Just HRefl <- proj_ConstKi @_ @Element f
  19          , Just HRefl <- proj_ConstKiTy @_ @(->) z
  20          = Just a
  21         expandFamFor _c _len _fam _as = Nothing
  22
  23 -- ** 'Type's
  24 famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
  25 famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)
  26
  27 -- * Class 'Sym_MonoFunctor'
  28 type instance Sym MonoFunctor = Sym_MonoFunctor
  29 class Sym_MonoFunctor term where
  30         omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
  31         default omap
  32          :: Sym_MonoFunctor (UnT term)
  33          => Trans term
  34          => MonoFunctor o
  35          => term (MT.Element o -> MT.Element o) -> term o -> term o
  36         omap = trans2 omap
  37
  38 -- Interpreting
  39 instance Sym_MonoFunctor Eval where
  40         omap = eval2 MT.omap
  41 instance Sym_MonoFunctor View where
  42         omap = view2 "omap"
  43 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Dup r1 r2) where
  44         omap = dup2 @Sym_MonoFunctor omap
  45
  46 -- Transforming
  47 instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
  48
  49 -- Typing
  50 instance FixityOf MonoFunctor
  51 instance ClassInstancesFor MonoFunctor
  52 instance TypeInstancesFor MonoFunctor
  53
  54 -- Compiling
  55 instance Gram_Term_AtomsFor src ss g MonoFunctor
  56 instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where
  57         moduleFor = ["MonoFunctor"] `moduleWhere`
  58          [ "omap" := teMonoFunctor_omap
  59          ]
  60
  61 -- ** 'Type's
  62 tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)
  63 tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a
  64
  65 o0 :: Source src => LenInj vs => KindInj (K o) =>
  66      Type src (Proxy o ': vs) o
  67 o0 = tyVar "o" varZ
  68
  69 e1 :: Source src => LenInj vs => KindInj (K e) =>
  70      Type src (a ': Proxy e ': vs) e
  71 e1 = tyVar "e" $ VarS varZ
  72
  73 -- ** 'Term's
  74 teMonoFunctor_omap :: TermDef MonoFunctor '[Proxy o, Proxy e] (MonoFunctor o # e #~ MT.Element o #> ((e -> e) -> o -> o))
  75 teMonoFunctor_omap = Term (tyMonoFunctor o0 # e1 #~ famElement o0) ((e1 ~> e1) ~> o0 ~> o0) $ teSym @MonoFunctor $ lam2 omap