Add colorable and decorable.

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

diff --git a/symantic-lib/Language/Symantic/Lib/List.hs b/symantic-lib/Language/Symantic/Lib/List.hs
index 048d4d5e31da9616145e3c94290230848a56e0da..d4275ade639097229ff9b91987a68df0a684048e 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/List.hs
+++ b/symantic-lib/Language/Symantic/Lib/List.hs
@@ -13,12 +13,12 @@ import qualified Data.Text as Text
 import qualified Data.Traversable as Traversable
 
 import Language.Symantic
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
 import Language.Symantic.Lib.Function (a0, b1, c2)
 import Language.Symantic.Lib.MonoFunctor (Element)
 
 -- * Class 'Sym_List'
-type instance Sym (Proxy []) = Sym_List
+type instance Sym [] = Sym_List
 class Sym_List term where
        list_empty :: term [a]
        list_cons  :: term a -> term [a] -> term [a]; infixr 5 `list_cons`
@@ -62,9 +62,11 @@ instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where
 instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)
 
 -- Typing
-instance FixityOf [] where
+instance NameTyOf [] where
+       nameTyOf _c = [] `Mod` "[]"
+instance FixityOf []
 instance ClassInstancesFor [] where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+       proveConstraintFor _ (TyConst _ _ q :$ z)
         | Just HRefl <- proj_ConstKiTy @_ @[] z
         = case () of
                 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
@@ -73,16 +75,16 @@ instance ClassInstancesFor [] where
                   | Just Refl <- proj_Const @Monad       q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ z:@a)
         | Just HRefl <- proj_ConstKiTy @_ @[] z
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Monoid q -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict
                   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict
@@ -90,7 +92,7 @@ instance ClassInstancesFor [] where
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor [] where
-       expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)
+       expandFamFor _c _len f (z:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi   @_ @Element f
         , Just HRefl <- proj_ConstKiTy @_ @[] z
         = Just a
@@ -102,58 +104,47 @@ 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 _t =
+       g_term_atomsFor =
         [ rule "teList_list" $
                between (symbol "[") (symbol "]") listG
         , rule "teList_empty" $
-               withMeta $
-               (\src -> BinTree0 $ Token_Term $ TermVT_CF teList_empty `setSource` src)
+               G.source $
+               (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
                 <$ symbol "["
                 <* symbol "]"
         ]
                where
                listG :: CF g (AST_Term src ss)
                listG = rule "list" $
-                       withMeta $
+                       G.source $
                        (\a mb src ->
                                case mb of
-                                Just b_  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a) b_
+                                Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
                                 Nothing ->
                                        BinTree2
-                                        (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a)
-                                        (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_empty))
+                                        (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)
+                                        (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
                         <$> g_term
                         <*> option Nothing (Just <$ symbol "," <*> listG)
-instance (Source src, Inj_Sym ss []) => Module src ss [] where
-       module_ _s = [] `moduleWhere`
+instance (Source src, SymInj ss []) => ModuleFor src ss [] where
+       moduleFor = ["List"] `moduleWhere`
         [ "[]"      := teList_empty
         , "zipWith" := teList_zipWith
         , ":" `withInfixR` 5 := teList_cons
         ]
 
 -- ** 'Type's
-tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]
+tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]
 tyList = (tyConst @(K []) @[] `tyApp`)
 
 -- ** 'Term's
-teList_empty ::
- Source src => Inj_Sym ss [] =>
- Term src ss ts '[Proxy a] [a]
+teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])
 teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
 
-teList_cons ::
- Source src => Inj_Sym ss [] =>
- Term src ss ts '[Proxy a] (a -> [a] -> [a])
-teList_cons =
-       Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $
-       teSym @[] $ lam2 list_cons
+teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
+teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons
 
-teList_zipWith ::
- Source src => Inj_Sym ss [] =>
- Term src ss ts '[Proxy a, Proxy b, Proxy c]
-                 ((a -> b -> c) -> [a] -> [b] -> [c])
-teList_zipWith =
-       Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $
-       teSym @[] $ lam3 zipWith
+teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
+teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith