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