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 -- | Expression for 'List'.
   9 module Language.Symantic.Expr.List where
  10
  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
  21 -- * Class 'Sym_List_Lam'
  22 -- | Symantic.
  23 class Sym_List repr where
  24         list_empty :: repr [a]
  25         list_cons  :: repr a -> repr [a] -> repr [a]
  26         list       :: [repr a] -> repr [a]
  27
  28         default list_empty :: Trans t repr => t repr [a]
  29         default list_cons  :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
  30         default list       :: Trans t repr => [t repr a] -> t repr [a]
  31         list_empty = trans_lift list_empty
  32         list_cons  = trans_map2 list_cons
  33         list l     = trans_lift $ list (trans_apply <$> l)
  34 -- | Symantic requiring a 'Lambda'.
  35 class Sym_List_Lam lam repr where
  36         list_filter
  37          :: repr (Lambda lam a Bool)
  38          -> repr [a]
  39          -> repr [a]
  40
  41         default list_filter
  42          :: Trans t repr
  43          => t repr (Lambda lam a Bool)
  44          -> t repr [a]
  45          -> t repr [a]
  46         list_filter = trans_map2 list_filter
  47
  48 instance -- Sym_List Dup
  49  ( Sym_List r1
  50  , Sym_List r2
  51  ) => Sym_List (Dup r1 r2) where
  52         list_empty = list_empty `Dup` list_empty
  53         list_cons (a1 `Dup` a2) (l1 `Dup` l2) = list_cons a1 l1 `Dup` list_cons a2 l2
  54         list l =
  55                 let (l1, l2) =
  56                         foldr (\(x1 `Dup` x2) (xs1, xs2) ->
  57                                 (x1:xs1, x2:xs2)) ([], []) l in
  58                 list l1 `Dup` list l2
  59 instance -- Sym_List_Lam Dup
  60  ( Sym_List_Lam lam r1
  61  , Sym_List_Lam lam r2
  62  ) => Sym_List_Lam lam (Dup r1 r2) where
  63         list_filter (f1 `Dup` f2) (l1 `Dup` l2) =
  64                 list_filter f1 l1 `Dup` list_filter f2 l2
  65
  66 -- * Type 'Expr_List'
  67 -- | Expression.
  68 data Expr_List (lam:: * -> *) (root:: *)
  69 type instance Root_of_Expr      (Expr_List lam root)      = root
  70 type instance Type_of_Expr      (Expr_List lam root)      = Type_List
  71 type instance Sym_of_Expr       (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr)
  72 type instance Error_of_Expr ast (Expr_List lam root)      = No_Error_Expr
  73
  74 -- | Parsing utility to check that the given type is a 'Type_List'
  75 -- or raise 'Error_Expr_Type_mismatch'.
  76 check_type_list
  77  :: forall ast ex root ty h ret.
  78  ( root ~ Root_of_Expr ex
  79  , ty ~ Type_Root_of_Expr ex
  80  , Type_Lift   Type_List (Type_of_Expr root)
  81  , Type_Unlift Type_List (Type_of_Expr root)
  82  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  83                    (Error_of_Expr ast root)
  84  )
  85  => Proxy ex -> ast -> ty h
  86  -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
  87  -> Either (Error_of_Expr ast root) ret
  88 check_type_list ex ast ty k =
  89         case type_unlift $ unType_Root ty of
  90          Just ty_l -> k ty_l
  91          Nothing -> Left $
  92                 error_expr ex $
  93                 Error_Expr_Type_mismatch ast
  94                  (Exists_Type (type_list $ type_var SZero
  95                  :: Type_Root_of_Expr ex [Zero]))
  96                  (Exists_Type ty)
  97
  98 -- | Parse 'list_empty'.
  99 list_empty_from
 100  :: forall root lam ty ty_root ast hs ret.
 101  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 102  , ty_root ~ Type_Root_of_Expr root
 103  , Type_from ast ty_root
 104  , Type_Root_Lift Type_List ty_root
 105  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 106                    (Error_of_Expr ast root)
 107  , Root_of_Expr root ~ root
 108  ) => ast
 109  -> Expr_From ast (Expr_List lam root) hs ret
 110 list_empty_from ast_ty_a ex ast _ctx k =
 111         case type_from (Proxy::Proxy ty_root)
 112          ast_ty_a (Right . Exists_Type) of
 113          Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
 114          Right (Exists_Type ty_a) ->
 115                 k (type_list ty_a) $ Forall_Repr_with_Context $
 116                         const list_empty
 117
 118 -- | Parse 'list_cons'.
 119 list_cons_from
 120  :: forall root lam ty ast hs ret.
 121  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 122  , Type_Eq (Type_Root_of_Expr root)
 123  , Expr_from ast root
 124  , Type_Lift   Type_List (Type_of_Expr root)
 125  , Type_Unlift Type_List (Type_of_Expr root)
 126  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 127                    (Error_of_Expr ast root)
 128  , Root_of_Expr root ~ root
 129  ) => ast -> ast
 130  -> Expr_From ast (Expr_List lam root) hs ret
 131 list_cons_from ast_a ast_l ex ast ctx k =
 132         expr_from (Proxy::Proxy root) ast_a ctx $
 133          \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 134         expr_from (Proxy::Proxy root) ast_l ctx $
 135          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
 136         check_type_list ex ast ty_l $ \(Type_List ty_l_a) ->
 137         check_type_eq ex ast ty_a ty_l_a $ \Refl ->
 138         k (type_list ty_a) $ Forall_Repr_with_Context $
 139                 \c -> list_cons (a c) (l c)
 140
 141 -- | Parse 'list_filter'.
 142 list_filter_from
 143  :: forall root lam ty ty_root ast hs ret.
 144  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 145  , ty_root ~ Type_of_Expr root
 146  , Type_Eq (Type_Root_of_Expr root)
 147  , Expr_from ast root
 148  , Type_Lift   Type_Bool      ty_root
 149  , Type_Lift   (Type_Fun lam) ty_root
 150  , Type_Unlift (Type_Fun lam) ty_root
 151  , Type_Lift   Type_List      ty_root
 152  , Type_Unlift Type_List      ty_root
 153  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 154                    (Error_of_Expr ast root)
 155  , Root_of_Expr root ~ root
 156  ) => ast -> ast
 157  -> Expr_From ast (Expr_List lam root) hs ret
 158 list_filter_from ast_f ast_l ex ast ctx k =
 159         expr_from (Proxy::Proxy root) ast_f ctx $
 160          \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
 161         expr_from (Proxy::Proxy root) ast_l ctx $
 162          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
 163         check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
 164          :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
 165         check_type_eq ex ast type_bool ty_f_b $ \Refl ->
 166         check_type_list ex ast ty_l $ \(Type_List ty_l_a) ->
 167         check_type_eq ex ast ty_f_a ty_l_a $ \Refl ->
 168         k ty_l $ Forall_Repr_with_Context $
 169          \c -> list_filter (f c) (l c)
 170
 171 -- ** Type 'Expr_Lambda_List_Bool'
 172 -- | Convenient alias.
 173 type Expr_Lambda_List_Bool lam
 174  =   Expr_Root (Expr_Lambda lam .|. Expr_List lam .|. Expr_Bool)
 175
 176 -- | Convenient alias around 'expr_from'.
 177 expr_lambda_list_bool_from
 178  :: forall lam ast root.
 179  ( Expr_from ast (Expr_Lambda_List_Bool lam)
 180  , root ~ Expr_Lambda_List_Bool lam
 181  ) => Proxy lam
 182  -> ast
 183  -> Either (Error_of_Expr ast root)
 184            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 185                                  (Forall_Repr root))
 186 expr_lambda_list_bool_from _lam ast =
 187         expr_from (Proxy::Proxy root) ast
 188          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
 189                 Right $ Exists_Type_and_Repr ty $
 190                         Forall_Repr $ repr Context_Empty