stack: bump to lts-12.25

[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 6b5f3c5619906d0bc0f42370e082f1609e6fae48..c8d776e60c40fc6329a339430b094da90e9ea760 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Map.hs
+++ b/symantic-lib/Language/Symantic/Lib/Map.hs
@@ -3,8 +3,18 @@
 -- | Symantic for 'Map'.
 module Language.Symantic.Lib.Map where
 
+import Data.Bool
+import Data.Eq (Eq)
+import Data.Foldable (Foldable)
+import Data.Function (($))
+import Data.Functor (Functor)
 import Data.Map.Strict (Map)
+import Data.Maybe (Maybe(..))
 import Data.MonoTraversable (MonoFunctor)
+import Data.Monoid (Monoid)
+import Data.Ord (Ord)
+import Data.Traversable (Traversable)
+import Text.Show (Show)
 import qualified Data.Map.Strict as Map
 
 import Language.Symantic
@@ -17,7 +27,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,43 +95,45 @@ 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
-       moduleFor _s = ["Map"] `moduleWhere`
+instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
+       moduleFor = ["Map"] `moduleWhere`
         [ "delete"       := teMap_delete
         , "difference"   := teMap_difference
         , "foldrWithKey" := teMap_foldrWithKey
@@ -134,14 +146,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
 
@@ -164,11 +176,11 @@ teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $
 teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
 teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
 
-teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] ((k -> a -> b -> b) -> b -> Map k a -> b)
+teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
 teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
 
-teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] ((k -> a -> b) -> Map k a -> Map k b)
+teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
 teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
 
-teMap_keys :: TermDef Map '[Proxy a, Proxy k] (Map k a -> [k])
+teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
 teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys