]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
cabal: bump GHC version
[haskell/symantic.git] / 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