Language/Symantic/Expr/Map.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 -- | Expression for 'Map'.
   9 module Language.Symantic.Expr.Map where
  10
  11 import Data.Map.Strict as Map
  12 import Data.Proxy (Proxy(..))
  13 import Data.Type.Equality ((:~:)(Refl))
  14
  15 import Language.Symantic.Type
  16 import Language.Symantic.Trans.Common
  17 import Language.Symantic.Expr.Root
  18 import Language.Symantic.Expr.Error
  19 import Language.Symantic.Expr.From
  20 import Language.Symantic.Expr.Lambda
  21 -- import Language.Symantic.Expr.Bool
  22 import Language.Symantic.Expr.List
  23 import Language.Symantic.Expr.Tuple
  24
  25 -- * Class 'Sym_Map_Lam'
  26 -- | Symantic.
  27 class Sym_Map repr where
  28         map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
  29
  30         default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
  31         map_from_list = trans_map1 map_from_list
  32 -- | Symantic.
  33 class Sym_Map_Lam lam repr where
  34         map_map
  35          :: repr (Lambda lam a b)
  36          -> repr (Map k a)
  37          -> repr (Map k b)
  38
  39         default map_map
  40          :: Trans t repr
  41          => t repr (Lambda lam a b)
  42          -> t repr (Map k a)
  43          -> t repr (Map k b)
  44         map_map = trans_map2 map_map
  45
  46 -- | Parsing utility to check that the given type is a 'Type_List'
  47 -- or raise 'Error_Expr_Type_mismatch'.
  48 check_type_map
  49  :: forall ast ex root ty h ret.
  50  ( root ~ Root_of_Expr ex
  51  , ty ~ Type_Root_of_Expr ex
  52  , Lift_Type   Type_Map (Type_of_Expr root)
  53  , Unlift_Type Type_Map (Type_of_Expr root)
  54  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  55                    (Error_of_Expr ast root)
  56  )
  57  => Proxy ex -> ast -> ty h
  58  -> (Type_Map ty h -> Either (Error_of_Expr ast root) ret)
  59  -> Either (Error_of_Expr ast root) ret
  60 check_type_map ex ast ty k =
  61         case unlift_type $ unType_Root ty of
  62          Just ty_l -> k ty_l
  63          Nothing -> Left $
  64                 error_expr ex $
  65                 Error_Expr_Type_mismatch ast
  66                  (Exists_Type (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
  67                  :: ty (Map Var0 Var0)))
  68                  (Exists_Type ty)
  69
  70 -- | Parse 'map_from_list'.
  71 map_from_list_from
  72  :: forall root lam ty ast hs ret.
  73  ( ty ~ Type_Root_of_Expr (Expr_Map lam root)
  74  , Expr_from ast root
  75  , Lift_Type   Type_List   (Type_of_Expr root)
  76  , Unlift_Type Type_List   (Type_of_Expr root)
  77  , Lift_Type   Type_Map    (Type_of_Expr root)
  78  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  79  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  80  , Constraint_Type Ord ty
  81  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  82                    (Error_of_Expr ast root)
  83  , Root_of_Expr root ~ root
  84  ) => ast
  85  -> Expr_From ast (Expr_Map lam root) hs ret
  86 map_from_list_from ast_l ex ast ctx k =
  87         expr_from (Proxy::Proxy root) ast_l ctx $
  88          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
  89         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_t) ->
  90         check_type_tuple2 ex ast ty_l_t $ \(Type_Type2 Proxy ty_k ty_a) ->
  91         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
  92         k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
  93          \c -> map_from_list (l c)
  94
  95 -- | Parse 'map_map'.
  96 map_map_from
  97  :: forall root lam ty ast hs ret.
  98  ( ty ~ Type_Root_of_Expr (Expr_Map lam root)
  99  , Eq_Type ty
 100  , Expr_from ast root
 101  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 102  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 103  , Lift_Type   Type_Map       (Type_of_Expr root)
 104  , Unlift_Type Type_Map       (Type_of_Expr root)
 105  , Constraint_Type Ord ty
 106  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 107                    (Error_of_Expr ast root)
 108  , Root_of_Expr root ~ root
 109  ) => ast -> ast
 110  -> Expr_From ast (Expr_Map lam root) hs ret
 111 map_map_from ast_f ast_m ex ast ctx k =
 112         expr_from (Proxy::Proxy root) ast_f ctx $
 113          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 114         expr_from (Proxy::Proxy root) ast_m ctx $
 115          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 116         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 117          :: Type_Fun lam ty h_f) ->
 118         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 119         check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
 120         check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
 121         k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
 122          \c -> map_map (f c) (m c)
 123
 124 -- * Type 'Expr_Map'
 125 -- | Expression.
 126 data Expr_Map (lam:: * -> *) (root:: *)
 127 type instance Root_of_Expr      (Expr_Map lam root)      = root
 128 type instance Type_of_Expr      (Expr_Map lam root)      = Type_Map
 129 type instance Sym_of_Expr       (Expr_Map lam root) repr = (Sym_Map repr, Sym_Map_Lam lam repr)
 130 type instance Error_of_Expr ast (Expr_Map lam root)      = No_Error_Expr
 131
 132 instance Constraint_Type1 Functor (Type_Map root) where
 133         constraint_type1 _c Type_Type2{} = Just Dict
 134 instance Constraint_Type1 Functor (Type_Type1 (Proxy (Map k)) root) where
 135         constraint_type1 _c Type_Type1{} = Just Dict
 136 instance Constraint_Type1 Applicative (Type_Map root)
 137 instance Constraint_Type1 Applicative (Type_Type1 (Proxy (Map k)) root)
 138 instance Constraint_Type1 Traversable (Type_Map root) where
 139         constraint_type1 _c Type_Type2{} = Just Dict
 140 instance Constraint_Type1 Traversable (Type_Type1 (Proxy (Map k)) root) where
 141         constraint_type1 _c Type_Type1{} = Just Dict