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
  22 -- * Type 'Type_Map'
  23 -- | The 'Map' type.
  24 type Type_Map = Type_Type2 (Proxy Map)
  25
  26 pattern Type_Map
  27  :: root k -> root a
  28  -> Type_Type2 (Proxy Map) root (Map k a)
  29 pattern Type_Map k a
  30  = Type_Type2 Proxy k a
  31
  32 instance Unlift_Type1 Type_Map where
  33         unlift_type1 (Type_Type2 px a b) k =
  34                 k ( Type_Type1 (Proxy::Proxy (Map a)) b
  35                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  36                   )
  37 instance
  38  Constraint_Type Eq root =>
  39  Constraint_Type Eq (Type_Map root) where
  40         constraint_type c (Type_Type2 _ k a)
  41          | Just Dict <- constraint_type c k
  42          , Just Dict <- constraint_type c a
  43          = Just Dict
  44         constraint_type _c _ = Nothing
  45 instance
  46  Constraint_Type Ord root =>
  47  Constraint_Type Ord (Type_Map root) where
  48         constraint_type c (Type_Type2 _ k a)
  49          | Just Dict <- constraint_type c k
  50          , Just Dict <- constraint_type c a
  51          = Just Dict
  52         constraint_type _c _ = Nothing
  53 instance
  54  Constraint_Type Ord root =>
  55  Constraint_Type Monoid (Type_Map root) where
  56         constraint_type _c (Type_Type2 _ k _a)
  57          | Just Dict <- constraint_type (Proxy::Proxy Ord) k
  58          = Just Dict
  59         constraint_type _c _ = Nothing
  60 instance Constraint_Type Num (Type_Map root)
  61 instance Constraint_Type Integral (Type_Map root)
  62 instance Constraint_Type MT.MonoFunctor (Type_Map root) where
  63         constraint_type _c Type_Type2{} = Just Dict
  64 instance Constraint_Type1 Functor (Type_Map root) where
  65         constraint_type1 _c Type_Type2{} = Just Dict
  66 instance Constraint_Type1 Traversable (Type_Map root) where
  67         constraint_type1 _c Type_Type2{} = Just Dict
  68 instance Constraint_Type1 Foldable (Type_Map root) where
  69         constraint_type1 _c Type_Type2{} = Just Dict
  70 instance -- Eq_Type
  71  Eq_Type root =>
  72  Eq_Type (Type_Map root) where
  73         eq_type (Type_Type2 _px1 k1 a1) (Type_Type2 _px2 k2 a2)
  74          | Just Refl <- k1 `eq_type` k2
  75          , Just Refl <- a1 `eq_type` a2
  76          = Just Refl
  77         eq_type _ _ = Nothing
  78 instance -- Eq_Type1
  79  Eq_Type root =>
  80  Eq_Type1 (Type_Map root) where
  81         eq_type1 (Type_Type2 _px1 k1 _a1) (Type_Type2 _px2 k2 _a2)
  82          | Just Refl <- k1 `eq_type` k2
  83          = Just Refl
  84         eq_type1 _ _ = Nothing
  85 instance -- String_from_Type
  86  String_from_Type root =>
  87  String_from_Type (Type_Map root) where
  88         string_from_type (Type_Type2 _ k a) =
  89                 "Map (" ++ string_from_type k ++ ")"
  90                  ++ " (" ++ string_from_type a ++ ")"
  91
  92 -- | Inject 'Type_Map' within a root type.
  93 type_map
  94  :: forall root h_k h_a.
  95  (Lift_Type_Root Type_Map root)
  96  => root h_k -> root h_a
  97  -> root (Map h_k h_a)
  98 type_map = type_type2