Language/Symantic/Expr/List.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 -- | Expression for 'List'.
  10 module Language.Symantic.Expr.List where
  11
  12 import qualified Data.Function as Fun
  13 import Data.Proxy (Proxy(..))
  14 import Data.Type.Equality ((:~:)(Refl))
  15
  16 import Language.Symantic.Type
  17 import Language.Symantic.Trans.Common
  18 import Language.Symantic.Expr.Root
  19 import Language.Symantic.Expr.Error
  20 import Language.Symantic.Expr.From
  21 import Language.Symantic.Expr.Lambda
  22
  23 -- * Class 'Sym_List_Lam'
  24 -- | Symantic.
  25 class Sym_List repr where
  26         list_empty :: repr [a]
  27         list_cons :: repr a -> repr [a] -> repr [a]
  28         list :: [repr a] -> repr [a]
  29         list_filter :: repr (a -> Bool) -> repr [a] -> repr [a]
  30         list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c]
  31         list_reverse :: repr [a] -> repr [a]
  32
  33         default list_empty   :: Trans t repr => t repr [a]
  34         default list_cons    :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
  35         default list         :: Trans t repr => [t repr a] -> t repr [a]
  36         default list_filter  :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a]
  37         default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c]
  38         default list_reverse :: Trans t repr => t repr [a] -> t repr [a]
  39
  40         list_empty   = trans_lift list_empty
  41         list_cons    = trans_map2 list_cons
  42         list l       = trans_lift $ list (trans_apply Prelude.<$> l)
  43         list_filter  = trans_map2 list_filter
  44         list_zipWith = trans_map3 list_zipWith
  45         list_reverse = trans_map1 list_reverse
  46
  47 -- * Type 'Expr_List'
  48 -- | Expression.
  49 data Expr_List (root:: *)
  50 type instance Root_of_Expr      (Expr_List root)      = root
  51 type instance Type_of_Expr      (Expr_List root)      = Type_List
  52 type instance Sym_of_Expr       (Expr_List root) repr = (Sym_List repr)
  53 type instance Error_of_Expr ast (Expr_List root)      = No_Error_Expr
  54
  55 -- | Parsing utility to check that the given type is a 'Type_List'
  56 -- or raise 'Error_Expr_Type_mismatch'.
  57 check_type_list
  58  :: forall ast ex root ty h ret.
  59  ( root ~ Root_of_Expr ex
  60  , ty ~ Type_Root_of_Expr ex
  61  , Lift_Type   Type_List (Type_of_Expr root)
  62  , Unlift_Type Type_List (Type_of_Expr root)
  63  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  64                    (Error_of_Expr ast root)
  65  )
  66  => Proxy ex -> ast -> ty h
  67  -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
  68  -> Either (Error_of_Expr ast root) ret
  69 check_type_list ex ast ty k =
  70         case unlift_type $ unType_Root ty of
  71          Just ty_l -> k ty_l
  72          Nothing -> Left $
  73                 error_expr ex $
  74                 Error_Expr_Type_mismatch ast
  75                  (Exists_Type (type_list $ type_var0 SZero
  76                  :: ty [Var0]))
  77                  (Exists_Type ty)
  78
  79 -- | Parse 'list_empty'.
  80 list_empty_from
  81  :: forall root ty ast hs ret.
  82  ( ty ~ Type_Root_of_Expr (Expr_List root)
  83  , Type_from ast ty
  84  , Lift_Type Type_List (Type_of_Expr root)
  85  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  86                    (Error_of_Expr ast root)
  87  , Root_of_Expr root ~ root
  88  ) => ast
  89  -> Expr_From ast (Expr_List root) hs ret
  90 list_empty_from ast_ty_a ex ast _ctx k =
  91         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
  92         type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
  93         k (type_list ty_a) $ Forall_Repr_with_Context $
  94                 Fun.const list_empty
  95
  96 -- | Parse 'list_cons'.
  97 list_cons_from
  98  :: forall root ty ast hs ret.
  99  ( ty ~ Type_Root_of_Expr (Expr_List root)
 100  , Eq_Type ty
 101  , Expr_from ast root
 102  , Lift_Type   Type_List (Type_of_Expr root)
 103  , Unlift_Type Type_List (Type_of_Expr root)
 104  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 105                    (Error_of_Expr ast root)
 106  , Root_of_Expr root ~ root
 107  ) => ast -> ast
 108  -> Expr_From ast (Expr_List root) hs ret
 109 list_cons_from ast_a ast_l ex ast ctx k =
 110         expr_from (Proxy::Proxy root) ast_a ctx $
 111          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 112         expr_from (Proxy::Proxy root) ast_l ctx $
 113          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 114         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 115         check_eq_type ex ast ty_a ty_l_a $ \Refl ->
 116         k (type_list ty_a) $ Forall_Repr_with_Context $
 117          \c -> list_cons (a c) (l c)
 118
 119 -- | Parse 'list'.
 120 list_from
 121  :: forall root ex ty ast hs ret.
 122  ( ty ~ Type_Root_of_Expr (Expr_List root)
 123  , ex ~ Expr_List root
 124  , Eq_Type ty
 125  , Type_from ast ty
 126  , Expr_from ast root
 127  , Lift_Type   Type_List (Type_of_Expr root)
 128  , Unlift_Type Type_List (Type_of_Expr root)
 129  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 130                    (Error_of_Expr ast root)
 131  , Root_of_Expr root ~ root
 132  ) => ast -> [ast]
 133  -> Expr_From ast ex hs ret
 134 list_from ast_ty_a ast_as =
 135         case type_from (Proxy::Proxy ty)
 136          ast_ty_a (Right . Exists_Type) of
 137          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 138          Right (Exists_Type ty_a) -> go ty_a [] ast_as
 139         where
 140         go :: ty ty_a
 141            -> [Forall_Repr_with_Context root hs ty_a]
 142            -> [ast]
 143            -> Expr_From ast (Expr_List root) hs ret
 144         go ty_a as [] _ex _ast _ctx k =
 145                 k (type_list ty_a) $ Forall_Repr_with_Context $
 146                  \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 147         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 148                 expr_from (Proxy::Proxy root) ast_x ctx $
 149                  \(ty_x::ty h_x) x ->
 150                 check_eq_type ex ast ty_a ty_x $ \Refl ->
 151                 go ty_a (x:as) ast_xs ex ast ctx k
 152
 153 -- | Parse 'list_filter'.
 154 list_filter_from
 155  :: forall root ty ast hs ret.
 156  ( ty ~ Type_Root_of_Expr (Expr_List root)
 157  , Eq_Type ty
 158  , Expr_from ast root
 159  , Lift_Type   Type_Bool (Type_of_Expr root)
 160  , Lift_Type   Type_Fun  (Type_of_Expr root)
 161  , Unlift_Type Type_Fun  (Type_of_Expr root)
 162  , Lift_Type   Type_List (Type_of_Expr root)
 163  , Unlift_Type Type_List (Type_of_Expr root)
 164  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 165                    (Error_of_Expr ast root)
 166  , Root_of_Expr root ~ root
 167  ) => ast -> ast
 168  -> Expr_From ast (Expr_List root) hs ret
 169 list_filter_from ast_f ast_l ex ast ctx k =
 170         expr_from (Proxy::Proxy root) ast_f ctx $
 171          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 172         expr_from (Proxy::Proxy root) ast_l ctx $
 173          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 174         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 175          :: Type_Fun ty h_f) ->
 176         check_eq_type ex ast type_bool ty_f_b $ \Refl ->
 177         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 178         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 179         k ty_l $ Forall_Repr_with_Context $
 180          \c -> list_filter (f c) (l c)
 181
 182 -- | Parse 'list_zipWith'.
 183 list_zipWith_from
 184  :: forall root ty ast hs ret.
 185  ( ty ~ Type_Root_of_Expr (Expr_List root)
 186  , Eq_Type ty
 187  , Expr_from ast root
 188  , Lift_Type   Type_Fun  (Type_of_Expr root)
 189  , Unlift_Type Type_Fun  (Type_of_Expr root)
 190  , Lift_Type   Type_List (Type_of_Expr root)
 191  , Unlift_Type Type_List (Type_of_Expr root)
 192  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 193                    (Error_of_Expr ast root)
 194  , Root_of_Expr root ~ root
 195  ) => ast -> ast -> ast
 196  -> Expr_From ast (Expr_List root) hs ret
 197 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
 198  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 199         expr_from (Proxy::Proxy root) ast_f ctx $
 200          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 201         expr_from (Proxy::Proxy root) ast_la ctx $
 202          \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
 203         expr_from (Proxy::Proxy root) ast_lb ctx $
 204          \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
 205         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b2c
 206          :: Type_Fun ty h_f) ->
 207         check_type_fun ex ast ty_f_b2c $ \(Type_Type2 Proxy ty_f_b ty_f_c
 208          :: Type_Fun ty h_f_b2c) ->
 209         check_type_list ex ast ty_la $ \(Type_Type1 _ ty_l_a) ->
 210         check_type_list ex ast ty_lb $ \(Type_Type1 _ ty_l_b) ->
 211         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 212         check_eq_type ex ast ty_f_b ty_l_b $ \Refl ->
 213         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 214         k (type_list ty_f_c) $ Forall_Repr_with_Context $
 215          \c -> list_zipWith (f c) (la c) (lb c)
 216
 217 -- | Parse 'list_reverse'.
 218 list_reverse_from
 219  :: forall root ty ast hs ret.
 220  ( ty ~ Type_Root_of_Expr (Expr_List root)
 221  , Eq_Type ty
 222  , Expr_from ast root
 223  , Lift_Type   Type_List (Type_of_Expr root)
 224  , Unlift_Type Type_List (Type_of_Expr root)
 225  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 226                    (Error_of_Expr ast root)
 227  , Root_of_Expr root ~ root
 228  ) => ast
 229  -> Expr_From ast (Expr_List root) hs ret
 230 list_reverse_from ast_l ex ast ctx k =
 231         expr_from (Proxy::Proxy root) ast_l ctx $
 232          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 233         check_type_list ex ast ty_l $ \(Type_Type1 _ _ty_l_a) ->
 234         k ty_l $ Forall_Repr_with_Context $
 235          \c -> list_reverse (l c)