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 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
  22 -- * Class 'Sym_List_Lam'
  23 -- | Symantic.
  24 class Sym_List repr where
  25         list_empty :: repr [a]
  26         list_cons  :: repr a -> repr [a] -> repr [a]
  27         list       :: [repr a] -> repr [a]
  28
  29         default list_empty :: Trans t repr => t repr [a]
  30         default list_cons  :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
  31         default list       :: Trans t repr => [t repr a] -> t repr [a]
  32         list_empty = trans_lift list_empty
  33         list_cons  = trans_map2 list_cons
  34         list l     = trans_lift $ list (trans_apply Prelude.<$> l)
  35 -- | Symantic requiring a 'Lambda'.
  36 class Sym_List_Lam lam repr where
  37         list_filter
  38          :: repr (Lambda lam a Bool)
  39          -> repr [a]
  40          -> repr [a]
  41
  42         default list_filter
  43          :: Trans t repr
  44          => t repr (Lambda lam a Bool)
  45          -> t repr [a]
  46          -> t repr [a]
  47         list_filter = trans_map2 list_filter
  48
  49 -- * Type 'Expr_List'
  50 -- | Expression.
  51 data Expr_List (lam:: * -> *) (root:: *)
  52 type instance Root_of_Expr      (Expr_List lam root)      = root
  53 type instance Type_of_Expr      (Expr_List lam root)      = Type_List
  54 type instance Sym_of_Expr       (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr)
  55 type instance Error_of_Expr ast (Expr_List lam root)      = No_Error_Expr
  56
  57 -- | Parsing utility to check that the given type is a 'Type_List'
  58 -- or raise 'Error_Expr_Type_mismatch'.
  59 check_type_list
  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_List (Type_of_Expr root)
  64  , Unlift_Type Type_List (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_List ty h -> Either (Error_of_Expr ast root) ret)
  70  -> Either (Error_of_Expr ast root) ret
  71 check_type_list 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_list $ type_var0 SZero
  78                  :: ty [Var0]))
  79                  (Exists_Type ty)
  80
  81 -- | Parse 'list_empty'.
  82 list_empty_from
  83  :: forall root lam ty ast hs ret.
  84  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
  85  , Type_from ast ty
  86  , Lift_Type Type_List (Type_of_Expr root)
  87  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  88                    (Error_of_Expr ast root)
  89  , Root_of_Expr root ~ root
  90  ) => ast
  91  -> Expr_From ast (Expr_List lam root) hs ret
  92 list_empty_from ast_ty_a ex ast _ctx k =
  93         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  94         type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
  95         k (type_list ty_a) $ Forall_Repr_with_Context $
  96                 const list_empty
  97
  98 -- | Parse 'list_cons'.
  99 list_cons_from
 100  :: forall root lam ty ast hs ret.
 101  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 102  , Eq_Type ty
 103  , Expr_from ast root
 104  , Lift_Type   Type_List (Type_of_Expr root)
 105  , Unlift_Type Type_List (Type_of_Expr root)
 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_List lam root) hs ret
 111 list_cons_from ast_a ast_l ex ast ctx k =
 112         expr_from (Proxy::Proxy root) ast_a ctx $
 113          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 114         expr_from (Proxy::Proxy root) ast_l ctx $
 115          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 116         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 117         check_eq_type ex ast ty_a ty_l_a $ \Refl ->
 118         k (type_list ty_a) $ Forall_Repr_with_Context $
 119                 \c -> list_cons (a c) (l c)
 120
 121 -- | Parse 'list'.
 122 list_from
 123  :: forall root lam ex ty ast hs ret.
 124  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 125  , ex ~ Expr_List lam root
 126  , Eq_Type ty
 127  , Type_from ast ty
 128  , Expr_from ast root
 129  , Lift_Type   Type_List (Type_of_Expr root)
 130  , Unlift_Type Type_List (Type_of_Expr root)
 131  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 132                    (Error_of_Expr ast root)
 133  , Root_of_Expr root ~ root
 134  ) => ast -> [ast]
 135  -> Expr_From ast ex hs ret
 136 list_from ast_ty_a ast_as =
 137         case type_from (Proxy::Proxy ty)
 138          ast_ty_a (Right . Exists_Type) of
 139          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 140          Right (Exists_Type ty_a) -> go ty_a [] ast_as
 141         where
 142         go :: ty ty_a
 143            -> [Forall_Repr_with_Context root hs ty_a]
 144            -> [ast]
 145            -> Expr_From ast (Expr_List lam root) hs ret
 146         go ty_a as [] _ex _ast _ctx k =
 147                 k (type_list ty_a) $ Forall_Repr_with_Context $
 148                         \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 149         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 150                 expr_from (Proxy::Proxy root) ast_x ctx $
 151                  \(ty_x::ty h_x) x ->
 152                 check_eq_type ex ast ty_a ty_x $ \Refl ->
 153                 go ty_a (x:as) ast_xs ex ast ctx k
 154
 155 -- | Parse 'list_filter'.
 156 list_filter_from
 157  :: forall root lam ty ast hs ret.
 158  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 159  , Eq_Type ty
 160  , Expr_from ast root
 161  , Lift_Type   Type_Bool      (Type_of_Expr root)
 162  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 163  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 164  , Lift_Type   Type_List      (Type_of_Expr root)
 165  , Unlift_Type Type_List      (Type_of_Expr root)
 166  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 167                    (Error_of_Expr ast root)
 168  , Root_of_Expr root ~ root
 169  ) => ast -> ast
 170  -> Expr_From ast (Expr_List lam root) hs ret
 171 list_filter_from ast_f ast_l ex ast ctx k =
 172         expr_from (Proxy::Proxy root) ast_f ctx $
 173          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 174         expr_from (Proxy::Proxy root) ast_l ctx $
 175          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 176         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 177          :: Type_Fun lam ty h_f) ->
 178         check_eq_type ex ast type_bool ty_f_b $ \Refl ->
 179         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 180         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 181         k ty_l $ Forall_Repr_with_Context $
 182          \c -> list_filter (f c) (l c)