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.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 Prelude.<$> 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 -- * Type 'Expr_List'
  48 -- | Expression.
  49 data Expr_List (lam:: * -> *) (root:: *)
  50 type instance Root_of_Expr      (Expr_List lam root)      = root
  51 type instance Type_of_Expr      (Expr_List lam root)      = Type_List
  52 type instance Sym_of_Expr       (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr)
  53 type instance Error_of_Expr ast (Expr_List lam root)      = No_Error_Expr
  54
  55 instance Constraint_Type1 Functor (Type_List root) where
  56         constraint_type1 _c (Type_Type1 _ _) = Just Dict
  57 instance Constraint_Type1 Applicative (Type_List root) where
  58         constraint_type1 _c (Type_Type1 _ _) = Just Dict
  59
  60 -- | Parsing utility to check that the given type is a 'Type_List'
  61 -- or raise 'Error_Expr_Type_mismatch'.
  62 check_type_list
  63  :: forall ast ex root ty h ret.
  64  ( root ~ Root_of_Expr ex
  65  , ty ~ Type_Root_of_Expr ex
  66  , Lift_Type   Type_List (Type_of_Expr root)
  67  , Unlift_Type Type_List (Type_of_Expr root)
  68  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  69                    (Error_of_Expr ast root)
  70  )
  71  => Proxy ex -> ast -> ty h
  72  -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
  73  -> Either (Error_of_Expr ast root) ret
  74 check_type_list ex ast ty k =
  75         case unlift_type $ unType_Root ty of
  76          Just ty_l -> k ty_l
  77          Nothing -> Left $
  78                 error_expr ex $
  79                 Error_Expr_Type_mismatch ast
  80                  (Exists_Type (type_list $ type_var0 SZero
  81                  :: Type_Root_of_Expr ex [Var0]))
  82                  (Exists_Type ty)
  83
  84 -- | Parse 'list_empty'.
  85 list_empty_from
  86  :: forall root lam ty ty_root ast hs ret.
  87  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
  88  , ty_root ~ Type_Root_of_Expr root
  89  , Type_from ast ty_root
  90  , Lift_Type_Root Type_List ty_root
  91  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  92                    (Error_of_Expr ast root)
  93  , Root_of_Expr root ~ root
  94  ) => ast
  95  -> Expr_From ast (Expr_List lam root) hs ret
  96 list_empty_from ast_ty_a ex ast _ctx k =
  97         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  98         type_from (Proxy::Proxy ty_root) ast_ty_a $ \ty_a -> Right $
  99         k (type_list ty_a) $ Forall_Repr_with_Context $
 100                 const list_empty
 101
 102 -- | Parse 'list_cons'.
 103 list_cons_from
 104  :: forall root lam ty ast hs ret.
 105  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 106  , Eq_Type (Type_Root_of_Expr root)
 107  , Expr_from ast root
 108  , Lift_Type   Type_List (Type_of_Expr root)
 109  , Unlift_Type Type_List (Type_of_Expr root)
 110  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 111                    (Error_of_Expr ast root)
 112  , Root_of_Expr root ~ root
 113  ) => ast -> ast
 114  -> Expr_From ast (Expr_List lam root) hs ret
 115 list_cons_from ast_a ast_l ex ast ctx k =
 116         expr_from (Proxy::Proxy root) ast_a ctx $
 117          \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 118         expr_from (Proxy::Proxy root) ast_l ctx $
 119          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
 120         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 121         check_eq_type ex ast ty_a ty_l_a $ \Refl ->
 122         k (type_list ty_a) $ Forall_Repr_with_Context $
 123                 \c -> list_cons (a c) (l c)
 124
 125 -- | Parse 'list'.
 126 list_from
 127  :: forall root lam ex ty ty_root ast hs ret.
 128  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 129  , ty_root ~ Type_Root_of_Expr root
 130  , ex ~ Expr_List lam root
 131  , Eq_Type (Type_Root_of_Expr root)
 132  , Type_from ast ty_root
 133  , Expr_from ast root
 134  , Lift_Type   Type_List (Type_of_Expr root)
 135  , Unlift_Type Type_List (Type_of_Expr root)
 136  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 137                    (Error_of_Expr ast root)
 138  , Root_of_Expr root ~ root
 139  , Root_of_Type ty_root ~ ty_root
 140  ) => ast -> [ast]
 141  -> Expr_From ast ex hs ret
 142 list_from ast_ty_a ast_as =
 143         case type_from (Proxy::Proxy ty_root)
 144          ast_ty_a (Right . Exists_Type) of
 145          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 146          Right (Exists_Type ty_a) -> go ty_a [] ast_as
 147         where
 148         go :: Type_Root_of_Expr root ty_a
 149            -> [Forall_Repr_with_Context root hs ty_a]
 150            -> [ast]
 151            -> Expr_From ast (Expr_List lam root) hs ret
 152         go ty_a as [] _ex _ast _ctx k =
 153                 k (type_list ty_a) $ Forall_Repr_with_Context $
 154                         \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 155         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 156                 expr_from (Proxy::Proxy root) ast_x ctx $
 157                  \(ty_x::Type_Root_of_Expr root h_x) x ->
 158                 check_eq_type ex ast ty_a ty_x $ \Refl ->
 159                 go ty_a (x:as) ast_xs ex ast ctx k
 160
 161 -- | Parse 'list_filter'.
 162 list_filter_from
 163  :: forall root lam ty ty_root ast hs ret.
 164  ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 165  , ty_root ~ Type_of_Expr root
 166  , Eq_Type (Type_Root_of_Expr root)
 167  , Expr_from ast root
 168  , Lift_Type   Type_Bool      ty_root
 169  , Lift_Type   (Type_Fun lam) ty_root
 170  , Unlift_Type (Type_Fun lam) ty_root
 171  , Lift_Type   Type_List      ty_root
 172  , Unlift_Type Type_List      ty_root
 173  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 174                    (Error_of_Expr ast root)
 175  , Root_of_Expr root ~ root
 176  ) => ast -> ast
 177  -> Expr_From ast (Expr_List lam root) hs ret
 178 list_filter_from ast_f ast_l ex ast ctx k =
 179         expr_from (Proxy::Proxy root) ast_f ctx $
 180          \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
 181         expr_from (Proxy::Proxy root) ast_l ctx $
 182          \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
 183         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 184          :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
 185         check_eq_type ex ast type_bool ty_f_b $ \Refl ->
 186         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 187         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 188         k ty_l $ Forall_Repr_with_Context $
 189          \c -> list_filter (f c) (l c)