Add colorable and decorable.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / MonoFunctor.hs

diff --git a/symantic-lib/Language/Symantic/Lib/MonoFunctor.hs b/symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
index c3f48a8b005f2ead482b77d17945f57394031f1b..3e585412d0d6171ea08b83d04fb464caeb59d51c 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
+++ b/symantic-lib/Language/Symantic/Lib/MonoFunctor.hs
@@ -12,9 +12,11 @@ import Language.Symantic.Lib.Function ()
 -- * Type 'Element'
 data Element
 type instance Fam Element '[h] = MT.Element (UnProxy h)
+instance NameTyOf Element where
+       nameTyOf _c = ["MonoFunctor"] `Mod` "Element"
 instance ClassInstancesFor Element
 instance TypeInstancesFor Element where
-       expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)
+       expandFamFor _c _len f (z:@_ty_r:@ a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @(->) z
         = Just a
@@ -22,17 +24,17 @@ instance TypeInstancesFor Element where
 
 -- ** 'Type's
 famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
-famElement o = TyFam noSource (lenVars o) (inj_Const @Element) (o `TypesS` TypesZ)
+famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)
 
 -- * Class 'Sym_MonoFunctor'
 type instance Sym MonoFunctor = Sym_MonoFunctor
 class Sym_MonoFunctor term where
        omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
-       default omap
-        :: Sym_MonoFunctor (UnT term)
-        => Trans term
-        => MonoFunctor o
-        => term (MT.Element o -> MT.Element o) -> term o -> term o
+       default omap ::
+        Sym_MonoFunctor (UnT term) =>
+        Trans term =>
+        MonoFunctor o =>
+        term (MT.Element o -> MT.Element o) -> term o -> term o
        omap = trans2 omap
 
 -- Interpreting
@@ -47,13 +49,15 @@ instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Dup r1 r2)
 instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
 
 -- Typing
+instance NameTyOf MonoFunctor where
+       nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor"
 instance FixityOf MonoFunctor
 instance ClassInstancesFor MonoFunctor
 instance TypeInstancesFor MonoFunctor
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g MonoFunctor
-instance (Source src, Inj_Sym ss MonoFunctor) => ModuleFor src ss MonoFunctor where
+instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where
        moduleFor = ["MonoFunctor"] `moduleWhere`
         [ "omap" := teMonoFunctor_omap
         ]
@@ -62,11 +66,11 @@ instance (Source src, Inj_Sym ss MonoFunctor) => ModuleFor src ss MonoFunctor wh
 tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)
 tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a
 
-o0 :: Source src => Inj_Len vs => Inj_Kind (K o) =>
+o0 :: Source src => LenInj vs => KindInj (K o) =>
      Type src (Proxy o ': vs) o
 o0 = tyVar "o" varZ
 
-e1 :: Source src => Inj_Len vs => Inj_Kind (K e) =>
+e1 :: Source src => LenInj vs => KindInj (K e) =>
      Type src (a ': Proxy e ': vs) e
 e1 = tyVar "e" $ VarS varZ