Bump versions.

[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 0a7d6a722d2df4b4c30df1e544a3b4b028af6a83..43a49a6e63b7a91032c8621a16585ae21f04fd0b 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,7 +62,9 @@ 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)
         | Just HRefl <- proj_ConstKiTy @_ @[] z
@@ -102,13 +104,13 @@ 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" $
-               g_source $
+               G.source $
                (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
                 <$ symbol "["
                 <* symbol "]"
@@ -116,7 +118,7 @@ instance
                where
                listG :: CF g (AST_Term src ss)
                listG = rule "list" $
-                       g_source $
+                       G.source $
                        (\a mb src ->
                                case mb of
                                 Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
@@ -126,23 +128,23 @@ instance
                                         (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
                         <$> g_term
                         <*> option Nothing (Just <$ symbol "," <*> listG)
-instance (Source src, Inj_Sym ss []) => ModuleFor src ss [] where
-       moduleFor _s = ["List"] `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 :: 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 :: 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