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