Add tar GNUmakefile target.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Char.hs b/symantic-lib/Language/Symantic/Lib/Char.hs
index f19a262128119f8e79cdc9015ad14d87dfbed0cd..74b319b5f83d8d017d7e1c239a8a4e7e97630110 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Char.hs
+++ b/symantic-lib/Language/Symantic/Lib/Char.hs
@@ -7,12 +7,12 @@ import qualified Data.Char as Char
 import qualified Data.Text as Text
 
 import Language.Symantic.Grammar hiding (char, any)
-import qualified Language.Symantic.Grammar as Gram
+import qualified Language.Symantic.Grammar as G
 import Language.Symantic
 import Language.Symantic.Lib.List (tyList)
 
 -- * Class 'Sym_Char'
-type instance Sym (Proxy Char) = Sym_Char
+type instance Sym Char = Sym_Char
 class Sym_Char term where
        char :: Char -> term Char
        char_toUpper :: term Char -> term Char
@@ -45,6 +45,8 @@ instance (Sym_Char r1, Sym_Char r2) => Sym_Char (Dup r1 r2) where
 instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)
 
 -- Typing
+instance NameTyOf Char where
+       nameTyOf _c = ["Char"] `Mod` "Char"
 instance ClassInstancesFor Char where
        proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
         | Just HRefl <- proj_ConstKiTy @_ @Char z
@@ -64,37 +66,37 @@ instance
  , Gram_Alt g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss Char
+ , SymInj ss Char
  ) => Gram_Term_AtomsFor src ss g Char where
-       g_term_atomsFor _t =
+       g_term_atomsFor =
         [ rule "teChar" $
-               lexeme $ g_source $
-               (\c src -> BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teChar c)
+               lexeme $ source $
+               (\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
                 <$> between tickG tickG (
-                       cf_of_Terminal (Gram.any `but` tickG) <+>
+                       cfOf (G.any `but` tickG) <+>
                        '\'' <$ string "\\'"
                 )
         ]
                where
                tickG :: Gram_Terminal g' => g' Char
-               tickG = Gram.char '\''
-instance (Source src, Inj_Sym ss Char) => Module src ss Char where
-       module_ _s = [NameMod "Char"] `moduleWhere`
+               tickG = G.char '\''
+instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
+       moduleFor = ["Char"] `moduleWhere`
         [ "toLower" := teChar_toLower
         , "toUpper" := teChar_toUpper
         ]
 
 -- ** 'Type's
-tyChar :: Source src => Inj_Len vs => Type src vs Char
+tyChar :: Source src => LenInj vs => Type src vs Char
 tyChar = tyConst @(K Char) @Char
 
-tyString :: Source src => Inj_Len vs => Type src vs String
+tyString :: Source src => LenInj vs => Type src vs String
 tyString = tyList tyChar
 
 -- ** 'Term's
-teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] Char
+teChar :: Source src => SymInj ss Char => Char -> Term src ss ts '[] (() #> Char)
 teChar b = Term noConstraint tyChar $ teSym @Char $ char b
 
-teChar_toUpper, teChar_toLower :: TermDef Char '[] (Char -> Char)
+teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))
 teChar_toUpper = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toUpper
 teChar_toLower = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toLower