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