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