Add common instances to Interpreting.Dup.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Either.hs b/symantic-lib/Language/Symantic/Lib/Either.hs
index 4e0712c021603cfe773d8507b2a1ab77f62dfab1..a6203fac0e64031d7dec3ce9fe34ec5829d0780e 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Either.hs
+++ b/symantic-lib/Language/Symantic/Lib/Either.hs
@@ -12,7 +12,7 @@ import Language.Symantic.Lib.MonoFunctor (Element)
 import Language.Symantic.Lib.Function (a0, b1, c2)
 
 -- * Class 'Sym_Either'
-type instance Sym (Proxy Either) = Sym_Either
+type instance Sym Either = Sym_Either
 class Sym_Either term where
        _Left  :: term l -> term (Either l r)
        _Right :: term r -> term (Either l r)
@@ -44,10 +44,12 @@ instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where
 instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
 
 -- Typing
+instance NameTyOf Either where
+       nameTyOf _c = ["Either"] `Mod` "Either"
 instance FixityOf Either
 instance ClassInstancesFor Either where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
-        | Just HRefl <- proj_ConstKiTy @_ @Either c
+       proveConstraintFor _ (TyConst _ _ q :$ e:@_l)
+        | Just HRefl <- proj_ConstKiTy @_ @Either e
         = case () of
                 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
                   | Just Refl <- proj_Const @Applicative q -> Just Dict
@@ -55,32 +57,32 @@ instance ClassInstancesFor Either where
                   | Just Refl <- proj_Const @Foldable    q -> Just Dict
                   | Just Refl <- proj_Const @Traversable q -> Just Dict
                 _ -> Nothing
-       proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
-        | Just HRefl <- proj_ConstKiTy @_ @Either c
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ e:@l:@r)
+        | Just HRefl <- proj_ConstKiTy @_ @Either e
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` l)
-                  , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`l)
+                  , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
-                  , Just Dict <- proveConstraint (tq `tyApp` l)
-                  , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`l)
+                  , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` l)
-                  , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`l)
+                  , Just Dict <- proveConstraint (tq`tyApp`r) -> 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 Either where
-       expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
+       expandFamFor _c _len f (e:@_ty_l:@r `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
-        , Just HRefl <- proj_ConstKiTy @_ @Either c
+        , Just HRefl <- proj_ConstKiTy @_ @Either e
         = Just r
        expandFamFor _c _len _fam _as = Nothing
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Either
-instance (Source src, Inj_Sym ss Either) => ModuleFor src ss Either where
+instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
        moduleFor = ["Either"] `moduleWhere`
         [ "Left"   := teEither_Left
         , "Right"  := teEither_Right