]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
Integrate types to the module system.
[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 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