]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Map.hs
polish names
[haskell/symantic.git] / Language / Symantic / Type / Map.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE PatternSynonyms #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# OPTIONS_GHC -fno-warn-orphans #-}
10 module Language.Symantic.Type.Map where
11
12 import Data.Map.Strict as Map
13 import qualified Data.MonoTraversable as MT
14 import Data.Proxy
15 import Data.Type.Equality ((:~:)(Refl))
16
17 import Language.Symantic.Type.Root
18 import Language.Symantic.Type.Type0
19 import Language.Symantic.Type.Type1
20 import Language.Symantic.Type.Type2
21 import Language.Symantic.Type.Constraint
22 import Language.Symantic.Type.Family
23
24 -- * Type 'Type_Map'
25 -- | The 'Map' type.
26 type Type_Map = Type2 (Proxy Map)
27
28 pattern Type_Map
29 :: root k -> root a
30 -> Type2 (Proxy Map) root (Map k a)
31 pattern Type_Map k a
32 = Type2 Proxy k a
33
34 instance Type1_Unlift Type_Map where
35 type1_unlift (Type2 px a b) k =
36 k ( Type1 (Proxy::Proxy (Map a)) b
37 , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
38 )
39 instance
40 Type0_Constraint Eq root =>
41 Type0_Constraint Eq (Type_Map root) where
42 type0_constraint c (Type2 _ k a)
43 | Just Dict <- type0_constraint c k
44 , Just Dict <- type0_constraint c a
45 = Just Dict
46 type0_constraint _c _ = Nothing
47 instance
48 Type0_Constraint Ord root =>
49 Type0_Constraint Ord (Type_Map root) where
50 type0_constraint c (Type2 _ k a)
51 | Just Dict <- type0_constraint c k
52 , Just Dict <- type0_constraint c a
53 = Just Dict
54 type0_constraint _c _ = Nothing
55 instance
56 Type0_Constraint Ord root =>
57 Type0_Constraint Monoid (Type_Map root) where
58 type0_constraint _c (Type2 _ k _a)
59 | Just Dict <- type0_constraint (Proxy::Proxy Ord) k
60 = Just Dict
61 type0_constraint _c _ = Nothing
62 instance Type0_Constraint Num (Type_Map root)
63 instance Type0_Constraint Integral (Type_Map root)
64 instance Type0_Constraint MT.MonoFunctor (Type_Map root) where
65 type0_constraint _c Type2{} = Just Dict
66 instance Type1_Constraint Functor (Type_Map root) where
67 type1_constraint _c Type2{} = Just Dict
68 instance Type1_Constraint Traversable (Type_Map root) where
69 type1_constraint _c Type2{} = Just Dict
70 instance Type1_Constraint Foldable (Type_Map root) where
71 type1_constraint _c Type2{} = Just Dict
72 instance Type0_Family Type_Family_MonoElement (Type_Map root) where
73 type0_family _at (Type2 _px _k a) = Just a
74 instance -- Type0_Eq
75 Type0_Eq root =>
76 Type0_Eq (Type_Map root) where
77 type0_eq (Type2 _px1 k1 a1) (Type2 _px2 k2 a2)
78 | Just Refl <- k1 `type0_eq` k2
79 , Just Refl <- a1 `type0_eq` a2
80 = Just Refl
81 type0_eq _ _ = Nothing
82 instance -- Type1_Eq
83 Type0_Eq root =>
84 Type1_Eq (Type_Map root) where
85 type1_eq (Type2 _px1 k1 _a1) (Type2 _px2 k2 _a2)
86 | Just Refl <- k1 `type0_eq` k2
87 = Just Refl
88 type1_eq _ _ = Nothing
89 instance -- String_from_Type
90 String_from_Type root =>
91 String_from_Type (Type_Map root) where
92 string_from_type (Type2 _ k a) =
93 "Map (" ++ string_from_type k ++ ")"
94 ++ " (" ++ string_from_type a ++ ")"
95
96 -- | Inject 'Type_Map' within a root type.
97 type_map
98 :: forall root h_k h_a.
99 (Type_Root_Lift Type_Map root)
100 => root h_k -> root h_a
101 -> root (Map h_k h_a)
102 type_map = type2