]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
Rename inj_* -> *Inj.
[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.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