Language/Symantic/Expr/Map.hs

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