Add colorable and decorable.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Tuple2.hs b/symantic-lib/Language/Symantic/Lib/Tuple2.hs
index 6bcb7151a51991c2e6579970a1aa163064a62b35..4d31667ecd57105dddc6ec26a94e04560e4281cc 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Tuple2.hs
+++ b/symantic-lib/Language/Symantic/Lib/Tuple2.hs
@@ -50,11 +50,13 @@ instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where
 instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
 
 -- Typing
+instance NameTyOf (,) where
+       nameTyOf _c = ["Tuple2"] `Mod` ","
 instance FixityOf (,) where
        fixityOf _c = Just $ Fixity2 $ infixN (-1)
 instance ClassInstancesFor (,) where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
-        | Just HRefl <- proj_ConstKiTy @_ @(,) c
+       proveConstraintFor _ (TyConst _ _ q :$ t:@a)
+        | Just HRefl <- proj_ConstKiTy @_ @(,) t
         = case () of
                 _ | Just Refl <- proj_Const @Applicative q
                   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
@@ -64,32 +66,32 @@ instance ClassInstancesFor (,) where
                   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
-        | Just HRefl <- proj_ConstKiTy @_ @(,) c
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ t:@a:@b)
+        | Just HRefl <- proj_ConstKiTy @_ @(,) t
         = case () of
                 _ | Just Refl <- proj_Const @Bounded q
-                  , Just Dict <- proveConstraint (tq `tyApp` a)
-                  , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` a)
-                  , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @Monoid q
-                  , Just Dict <- proveConstraint (tq `tyApp` a)
-                  , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
-                  , Just Dict <- proveConstraint (tq `tyApp` a)
-                  , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` a)
-                  , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a)
+                  , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
-                  | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
+                  | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (,) where
-       expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
+       expandFamFor _c _len f (t:@_a:@b `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
-        , Just HRefl <- proj_ConstKiTy @_ @(,) c
+        , Just HRefl <- proj_ConstKiTy @_ @(,) t
         = Just b
        expandFamFor _c _len _fam _as = Nothing
 
@@ -100,7 +102,7 @@ instance
  , Gram_Rule g
  , Gram_Comment g
  , Gram_Term src ss g
- , Inj_Sym ss (,)
+ , SymInj ss (,)
  ) => Gram_Term_AtomsFor src ss g (,) where
        g_term_atomsFor =
         -- TODO: proper TupleSections
@@ -116,14 +118,14 @@ instance
                (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
                 <$ symbol "(,)"
         ]
-instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where
+instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where
        moduleFor = ["Tuple2"] `moduleWhere`
         [ "fst" := teTuple2_fst
         , "snd" := teTuple2_snd
         ]
 
 -- ** 'Term's
-tyTuple2 :: Source src => Inj_Len vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
+tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
 tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b
 
 teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))