Language/Symantic/Expr/List.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE TypeOperators #-}
   9 {-# OPTIONS_GHC -fno-warn-orphans #-}
  10 -- | Expression for 'List'.
  11 module Language.Symantic.Expr.List where
  12
  13 import Control.Monad
  14 import qualified Data.Function as Fun
  15 import qualified Data.List as List
  16 import Data.Monoid
  17 import Data.Proxy (Proxy(..))
  18 import qualified Data.Text as Text
  19 import Data.Type.Equality ((:~:)(Refl))
  20
  21 import Language.Symantic.Type
  22 import Language.Symantic.Repr
  23 import Language.Symantic.Expr.Root
  24 import Language.Symantic.Expr.Error
  25 import Language.Symantic.Expr.From
  26 import Language.Symantic.Expr.Lambda
  27 import Language.Symantic.Trans.Common
  28
  29 -- * Class 'Sym_List_Lam'
  30 -- | Symantic.
  31 class Sym_List repr where
  32         list_empty   :: repr [a]
  33         list_cons    :: repr a -> repr [a] -> repr [a]
  34         list         :: [repr a] -> repr [a]
  35         list_filter  :: repr (a -> Bool) -> repr [a] -> repr [a]
  36         list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c]
  37         list_reverse :: repr [a] -> repr [a]
  38
  39         default list_empty   :: Trans t repr => t repr [a]
  40         default list_cons    :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
  41         default list         :: Trans t repr => [t repr a] -> t repr [a]
  42         default list_filter  :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a]
  43         default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c]
  44         default list_reverse :: Trans t repr => t repr [a] -> t repr [a]
  45
  46         list_empty   = trans_lift list_empty
  47         list_cons    = trans_map2 list_cons
  48         list l       = trans_lift (list (trans_apply Prelude.<$> l))
  49         list_filter  = trans_map2 list_filter
  50         list_zipWith = trans_map3 list_zipWith
  51         list_reverse = trans_map1 list_reverse
  52 instance Sym_List Repr_Host where
  53         list_empty   = return []
  54         list_cons    = liftM2 (:)
  55         list         = sequence
  56         list_filter  = liftM2 List.filter
  57         list_zipWith = liftM3 List.zipWith
  58         list_reverse = liftM  List.reverse
  59 instance Sym_List Repr_Text where
  60         list_empty = Repr_Text $ \_p _v -> "[]"
  61         list_cons (Repr_Text x) (Repr_Text xs) =
  62                 Repr_Text $ \p v ->
  63                         let p' = Precedence 5 in
  64                         paren p p' $ x p' v <> ":" <> xs p' v
  65         list l = Repr_Text $ \_p v ->
  66                 let p' = precedence_Toplevel in
  67                 "[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]"
  68         list_filter  = repr_text_app2 "list_filter"
  69         list_zipWith = repr_text_app3 "list_zipWith"
  70         list_reverse = repr_text_app1 "list_reverse"
  71 instance (Sym_List r1, Sym_List r2) => Sym_List (Repr_Dup r1 r2) where
  72         list_empty = repr_dup0 sym_List list_empty
  73         list_cons  = repr_dup2 sym_List list_cons
  74         list l =
  75                 let (l1, l2) =
  76                         foldr (\(x1 `Repr_Dup` x2) (xs1, xs2) ->
  77                                 (x1:xs1, x2:xs2)) ([], []) l in
  78                 list l1 `Repr_Dup` list l2
  79         list_filter  = repr_dup2 sym_List list_filter
  80         list_zipWith = repr_dup3 sym_List list_zipWith
  81         list_reverse = repr_dup1 sym_List list_reverse
  82
  83 sym_List :: Proxy Sym_List
  84 sym_List = Proxy
  85
  86 -- * Type 'Expr_List'
  87 -- | Expression.
  88 data Expr_List (root:: *)
  89 type instance Root_of_Expr      (Expr_List root)      = root
  90 type instance Type_of_Expr      (Expr_List root)      = Type_List
  91 type instance Sym_of_Expr       (Expr_List root) repr = Sym_List repr
  92 type instance Error_of_Expr ast (Expr_List root)      = No_Error_Expr
  93
  94 -- | Parsing utility to check that the given type is a 'Type_List'
  95 -- or raise 'Error_Expr_Type_mismatch'.
  96 check_type_list
  97  :: forall ast ex root ty h ret.
  98  ( root ~ Root_of_Expr ex
  99  , ty ~ Type_Root_of_Expr ex
 100  , Type0_Lift   Type_List (Type_of_Expr root)
 101  , Type0_Unlift Type_List (Type_of_Expr root)
 102  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 103                    (Error_of_Expr ast root)
 104  )
 105  => Proxy ex -> ast -> ty h
 106  -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
 107  -> Either (Error_of_Expr ast root) ret
 108 check_type_list ex ast ty k =
 109         case type0_unlift $ unType_Root ty of
 110          Just ty_l -> k ty_l
 111          Nothing -> Left $ error_expr ex $
 112                 Error_Expr_Type_mismatch ast
 113                  (Exists_Type0 (type_list $ type_var0 SZero :: ty [Var0]))
 114                  (Exists_Type0 ty)
 115
 116 -- | Parse 'list_empty'.
 117 list_empty_from
 118  :: forall root ty ast hs ret.
 119  ( ty ~ Type_Root_of_Expr (Expr_List root)
 120  , Type0_From ast ty
 121  , Type0_Lift Type_List (Type_of_Expr root)
 122  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 123                    (Error_of_Expr ast root)
 124  , Root_of_Expr root ~ root
 125  ) => ast
 126  -> ExprFrom ast (Expr_List root) hs ret
 127 list_empty_from ast_ty_a ex ast _ctx k =
 128         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
 129         type0_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
 130         k (type_list ty_a) $ Forall_Repr_with_Context $
 131                 Fun.const list_empty
 132
 133 -- | Parse 'list_cons'.
 134 list_cons_from
 135  :: forall root ty ast hs ret.
 136  ( ty ~ Type_Root_of_Expr (Expr_List root)
 137  , Expr_From ast root
 138  , Type0_Eq ty
 139  , Type0_Lift   Type_List (Type_of_Expr root)
 140  , Type0_Unlift Type_List (Type_of_Expr root)
 141  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 142                    (Error_of_Expr ast root)
 143  , Root_of_Expr root ~ root
 144  ) => ast -> ast
 145  -> ExprFrom ast (Expr_List root) hs ret
 146 list_cons_from ast_a ast_l ex ast ctx k =
 147         expr_from (Proxy::Proxy root) ast_a ctx $
 148          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 149         expr_from (Proxy::Proxy root) ast_l ctx $
 150          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 151         check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
 152         check_type0_eq ex ast ty_a ty_l_a $ \Refl ->
 153         k (type_list ty_a) $ Forall_Repr_with_Context $
 154          \c -> list_cons (a c) (l c)
 155
 156 -- | Parse 'list'.
 157 list_from
 158  :: forall root ex ty ast hs ret.
 159  ( ty ~ Type_Root_of_Expr (Expr_List root)
 160  , ex ~ Expr_List root
 161  , Expr_From ast root
 162  , Type0_Eq ty
 163  , Type0_From ast ty
 164  , Type0_Lift   Type_List (Type_of_Expr root)
 165  , Type0_Unlift Type_List (Type_of_Expr root)
 166  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 167                    (Error_of_Expr ast root)
 168  , Root_of_Expr root ~ root
 169  ) => ast -> [ast]
 170  -> ExprFrom ast ex hs ret
 171 list_from ast_ty_a ast_as =
 172         case type0_from (Proxy::Proxy ty)
 173          ast_ty_a (Right . Exists_Type0) of
 174          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 175          Right (Exists_Type0 ty_a) -> go ty_a [] ast_as
 176         where
 177         go :: ty ty_a
 178            -> [Forall_Repr_with_Context root hs ty_a]
 179            -> [ast]
 180            -> ExprFrom ast (Expr_List root) hs ret
 181         go ty_a as [] _ex _ast _ctx k =
 182                 k (type_list ty_a) $ Forall_Repr_with_Context $
 183                  \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 184         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 185                 expr_from (Proxy::Proxy root) ast_x ctx $
 186                  \(ty_x::ty h_x) x ->
 187                 check_type0_eq ex ast ty_a ty_x $ \Refl ->
 188                 go ty_a (x:as) ast_xs ex ast ctx k
 189
 190 -- | Parse 'list_filter'.
 191 list_filter_from
 192  :: forall root ty ast hs ret.
 193  ( ty ~ Type_Root_of_Expr (Expr_List root)
 194  , Expr_From ast root
 195  , Type0_Eq ty
 196  , Type0_Lift   Type_Bool (Type_of_Expr root)
 197  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 198  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 199  , Type0_Lift   Type_List (Type_of_Expr root)
 200  , Type0_Unlift Type_List (Type_of_Expr root)
 201  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 202                    (Error_of_Expr ast root)
 203  , Root_of_Expr root ~ root
 204  ) => ast -> ast
 205  -> ExprFrom ast (Expr_List root) hs ret
 206 list_filter_from ast_f ast_l ex ast ctx k =
 207         expr_from (Proxy::Proxy root) ast_f ctx $
 208          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 209         expr_from (Proxy::Proxy root) ast_l ctx $
 210          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 211         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
 212         check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
 213         check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
 214         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 215         k ty_l $ Forall_Repr_with_Context $
 216          \c -> list_filter (f c) (l c)
 217
 218 -- | Parse 'list_zipWith'.
 219 list_zipWith_from
 220  :: forall root ty ast hs ret.
 221  ( ty ~ Type_Root_of_Expr (Expr_List root)
 222  , Expr_From ast root
 223  , Type0_Eq ty
 224  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 225  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 226  , Type0_Lift   Type_List (Type_of_Expr root)
 227  , Type0_Unlift Type_List (Type_of_Expr root)
 228  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 229                    (Error_of_Expr ast root)
 230  , Root_of_Expr root ~ root
 231  ) => ast -> ast -> ast
 232  -> ExprFrom ast (Expr_List root) hs ret
 233 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
 234  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 235         expr_from (Proxy::Proxy root) ast_f ctx $
 236          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 237         expr_from (Proxy::Proxy root) ast_la ctx $
 238          \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
 239         expr_from (Proxy::Proxy root) ast_lb ctx $
 240          \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
 241         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2c) ->
 242         check_type_fun ex ast ty_f_b2c $ \(Type2 Proxy ty_f_b ty_f_c) ->
 243         check_type_list ex ast ty_la $ \(Type1 _ ty_l_a) ->
 244         check_type_list ex ast ty_lb $ \(Type1 _ ty_l_b) ->
 245         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 246         check_type0_eq ex ast ty_f_b ty_l_b $ \Refl ->
 247         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 248         k (type_list ty_f_c) $ Forall_Repr_with_Context $
 249          \c -> list_zipWith (f c) (la c) (lb c)
 250
 251 -- | Parse 'list_reverse'.
 252 list_reverse_from
 253  :: forall root ty ast hs ret.
 254  ( ty ~ Type_Root_of_Expr (Expr_List root)
 255  , Expr_From ast root
 256  , Type0_Eq ty
 257  , Type0_Lift   Type_List (Type_of_Expr root)
 258  , Type0_Unlift Type_List (Type_of_Expr root)
 259  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 260                    (Error_of_Expr ast root)
 261  , Root_of_Expr root ~ root
 262  ) => ast
 263  -> ExprFrom ast (Expr_List root) hs ret
 264 list_reverse_from ast_l ex ast ctx k =
 265         expr_from (Proxy::Proxy root) ast_l ctx $
 266          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 267         check_type_list ex ast ty_l $ \(Type1 _ _ty_l_a) ->
 268         k ty_l $ Forall_Repr_with_Context $
 269          \c -> list_reverse (l c)