Language/Symantic/Expr/List.hs

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