grammar: rename At -> Sourced

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

diff --git a/symantic-lib/Language/Symantic/Lib/Maybe.hs b/symantic-lib/Language/Symantic/Lib/Maybe.hs
index 055d36513350f23e0fbaa7685fb2d2581aaf925b..12093fce4a8f76ac2553b13ab79a6dfeb7a81461 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Maybe.hs
+++ b/symantic-lib/Language/Symantic/Lib/Maybe.hs
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Function (a0, b1)
 import Language.Symantic.Lib.MonoFunctor (Element)
 
 -- * Class 'Sym_Maybe'
-type instance Sym (Proxy Maybe) = Sym_Maybe
+type instance Sym Maybe = Sym_Maybe
 class Sym_Maybe term where
        _Nothing :: term (Maybe a)
        _Just    :: term a -> term (Maybe a)
@@ -45,56 +45,58 @@ instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
 instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
 
 -- Typing
+instance NameTyOf Maybe where
+       nameTyOf _c = ["Maybe"] `Mod` "Maybe"
 instance FixityOf Maybe
 instance ClassInstancesFor Maybe where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
-        | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+       proveConstraintFor _ (TyConst _ _ q :$ m)
+        | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = case () of
                 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
-                  | Just Refl <- proj_Const @Foldable q    -> Just Dict
-                  | Just Refl <- proj_Const @Functor q     -> Just Dict
-                  | Just Refl <- proj_Const @Monad q       -> Just Dict
+                  | Just Refl <- proj_Const @Foldable    q -> Just Dict
+                  | Just Refl <- proj_Const @Functor     q -> Just Dict
+                  | Just Refl <- proj_Const @Monad       q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
-        | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@a)
+        | Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = 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 <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> 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 @MT.MonoFoldable q -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Maybe where
-       expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
+       expandFamFor _c _len f (m:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
-        , Just HRefl <- proj_ConstKiTy @_ @Maybe c
+        , Just HRefl <- proj_ConstKiTy @_ @Maybe m
         = Just a
        expandFamFor _c _len _fam _as = Nothing
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Maybe
-instance (Source src, Inj_Sym ss Maybe) => Module src ss Maybe where
-       module_ _s = [] `moduleWhere`
+instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
+       moduleFor = ["Maybe"] `moduleWhere`
         [ "Nothing" := teMaybe_Nothing
         , "Just"    := teMaybe_Just
         , "maybe"   := teMaybe_maybe
         ]
 
 -- ** 'Type's
-tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)
+tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
 
 -- ** 'Term's
-teMaybe_Nothing :: TermDef Maybe '[Proxy a] (Maybe a)
+teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
 teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
 
-teMaybe_Just :: TermDef Maybe '[Proxy a] (a -> Maybe a)
+teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
 teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
 
-teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (b -> (a -> b) -> Maybe a -> b)
+teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
 teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'