Rename Dim -> Dimension.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Map.hs b/symantic-lib/Language/Symantic/Lib/Map.hs
index bf3f73bb5ca212c635878d908a111d5e04b94577..3de90fab5aa6543264ffe6b0f85d85557d1ed46b 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Map.hs
+++ b/symantic-lib/Language/Symantic/Lib/Map.hs
@@ -17,7 +17,7 @@ import Language.Symantic.Lib.Ord (tyOrd)
 import Language.Symantic.Lib.Tuple2 (tyTuple2)
 
 -- * Class 'Sym_Map'
-type instance Sym (Proxy Map) = Sym_Map
+type instance Sym Map = Sym_Map
 class Sym_Map term where
        map_fromList     :: Ord k => term [(k, a)] -> term (Map k a)
        map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
@@ -85,42 +85,44 @@ instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where
 instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
 
 -- Typing
+instance NameTyOf Map where
+       nameTyOf _c = ["Map"] `Mod` "Map"
 instance FixityOf Map
 instance ClassInstancesFor Map where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
-        | Just HRefl <- proj_ConstKiTy @_ @Map c
+       proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
+        | Just HRefl <- proj_ConstKiTy @_ @Map m
         = case () of
                 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
                   | 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 k) a))
-        | Just HRefl <- proj_ConstKiTy @_ @Map c
+       proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
+        | Just HRefl <- proj_ConstKiTy @_ @Map m
         = case () of
                 _ | Just Refl <- proj_Const @Eq q
-                  , Just Dict <- proveConstraint (tq `tyApp` k)
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`k)
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Ord q
-                  , Just Dict <- proveConstraint (tq `tyApp` k)
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`k)
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @Monoid q
                   , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
                   | Just Refl <- proj_Const @Show q
-                  , Just Dict <- proveConstraint (tq `tyApp` k)
-                  , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+                  , Just Dict <- proveConstraint (tq`tyApp`k)
+                  , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
                   | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Map where
-       expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)
+       expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
         | Just HRefl <- proj_ConstKi @_ @Element f
-        , Just HRefl <- proj_ConstKiTy @_ @Map c
+        , Just HRefl <- proj_ConstKiTy @_ @Map m
         = Just a
        expandFamFor _c _len _fam _as = Nothing
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Map
-instance (Source src, Inj_Sym ss Map) => ModuleFor src ss Map where
+instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
        moduleFor = ["Map"] `moduleWhere`
         [ "delete"       := teMap_delete
         , "difference"   := teMap_difference
@@ -134,14 +136,14 @@ instance (Source src, Inj_Sym ss Map) => ModuleFor src ss Map where
         ]
 
 -- ** 'Type's
-tyMap :: Source src => Inj_Len vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
+tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
 tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
 
-k1 :: Source src => Inj_Len vs => Inj_Kind (K k) =>
+k1 :: Source src => LenInj vs => KindInj (K k) =>
      Type src (a ': Proxy k ': vs) k
 k1 = tyVar "k" $ VarS varZ
 
-k2 :: Source src => Inj_Len vs => Inj_Kind (K k) =>
+k2 :: Source src => LenInj vs => KindInj (K k) =>
      Type src (a ': b ': Proxy k ': vs) k
 k2 = tyVar "k" $ VarS $ VarS varZ