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