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 = list_empty `Repr_Dup` list_empty
  73         list_cons (a1 `Repr_Dup` a2) (l1 `Repr_Dup` l2) = list_cons a1 l1 `Repr_Dup` list_cons a2 l2
  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 (f1 `Repr_Dup` f2) (l1 `Repr_Dup` l2) =
  80                 list_filter f1 l1 `Repr_Dup` list_filter f2 l2
  81         list_zipWith (f1 `Repr_Dup` f2) (la1 `Repr_Dup` la2) (lb1 `Repr_Dup` lb2) =
  82                 list_zipWith f1 la1 lb1 `Repr_Dup` list_zipWith f2 la2 lb2
  83         list_reverse (l1 `Repr_Dup` l2) =
  84                 list_reverse l1 `Repr_Dup` list_reverse l2
  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 $
 112                 error_expr ex $
 113                 Error_Expr_Type_mismatch ast
 114                  (Exists_Type0 (type_list $ type_var0 SZero
 115                  :: ty [Var0]))
 116                  (Exists_Type0 ty)
 117
 118 -- | Parse 'list_empty'.
 119 list_empty_from
 120  :: forall root ty ast hs ret.
 121  ( ty ~ Type_Root_of_Expr (Expr_List root)
 122  , Type0_From ast ty
 123  , Type0_Lift Type_List (Type_of_Expr root)
 124  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 125                    (Error_of_Expr ast root)
 126  , Root_of_Expr root ~ root
 127  ) => ast
 128  -> ExprFrom ast (Expr_List root) hs ret
 129 list_empty_from ast_ty_a ex ast _ctx k =
 130         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
 131         type0_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
 132         k (type_list ty_a) $ Forall_Repr_with_Context $
 133                 Fun.const list_empty
 134
 135 -- | Parse 'list_cons'.
 136 list_cons_from
 137  :: forall root ty ast hs ret.
 138  ( ty ~ Type_Root_of_Expr (Expr_List root)
 139  , Expr_From ast root
 140  , Type0_Eq ty
 141  , Type0_Lift   Type_List (Type_of_Expr root)
 142  , Type0_Unlift Type_List (Type_of_Expr root)
 143  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 144                    (Error_of_Expr ast root)
 145  , Root_of_Expr root ~ root
 146  ) => ast -> ast
 147  -> ExprFrom ast (Expr_List root) hs ret
 148 list_cons_from ast_a ast_l ex ast ctx k =
 149         expr_from (Proxy::Proxy root) ast_a ctx $
 150          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 151         expr_from (Proxy::Proxy root) ast_l ctx $
 152          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 153         check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
 154         check_type0_eq ex ast ty_a ty_l_a $ \Refl ->
 155         k (type_list ty_a) $ Forall_Repr_with_Context $
 156          \c -> list_cons (a c) (l c)
 157
 158 -- | Parse 'list'.
 159 list_from
 160  :: forall root ex ty ast hs ret.
 161  ( ty ~ Type_Root_of_Expr (Expr_List root)
 162  , ex ~ Expr_List root
 163  , Expr_From ast root
 164  , Type0_Eq ty
 165  , Type0_From ast ty
 166  , Type0_Lift   Type_List (Type_of_Expr root)
 167  , Type0_Unlift Type_List (Type_of_Expr root)
 168  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 169                    (Error_of_Expr ast root)
 170  , Root_of_Expr root ~ root
 171  ) => ast -> [ast]
 172  -> ExprFrom ast ex hs ret
 173 list_from ast_ty_a ast_as =
 174         case type0_from (Proxy::Proxy ty)
 175          ast_ty_a (Right . Exists_Type0) of
 176          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 177          Right (Exists_Type0 ty_a) -> go ty_a [] ast_as
 178         where
 179         go :: ty ty_a
 180            -> [Forall_Repr_with_Context root hs ty_a]
 181            -> [ast]
 182            -> ExprFrom ast (Expr_List root) hs ret
 183         go ty_a as [] _ex _ast _ctx k =
 184                 k (type_list ty_a) $ Forall_Repr_with_Context $
 185                  \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 186         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 187                 expr_from (Proxy::Proxy root) ast_x ctx $
 188                  \(ty_x::ty h_x) x ->
 189                 check_type0_eq ex ast ty_a ty_x $ \Refl ->
 190                 go ty_a (x:as) ast_xs ex ast ctx k
 191
 192 -- | Parse 'list_filter'.
 193 list_filter_from
 194  :: forall root ty ast hs ret.
 195  ( ty ~ Type_Root_of_Expr (Expr_List root)
 196  , Expr_From ast root
 197  , Type0_Eq ty
 198  , Type0_Lift   Type_Bool (Type_of_Expr root)
 199  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 200  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 201  , Type0_Lift   Type_List (Type_of_Expr root)
 202  , Type0_Unlift Type_List (Type_of_Expr root)
 203  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 204                    (Error_of_Expr ast root)
 205  , Root_of_Expr root ~ root
 206  ) => ast -> ast
 207  -> ExprFrom ast (Expr_List root) hs ret
 208 list_filter_from ast_f ast_l ex ast ctx k =
 209         expr_from (Proxy::Proxy root) ast_f ctx $
 210          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 211         expr_from (Proxy::Proxy root) ast_l ctx $
 212          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 213         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
 214         check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
 215         check_type_list ex ast ty_l $ \(Type1 _ ty_l_a) ->
 216         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 217         k ty_l $ Forall_Repr_with_Context $
 218          \c -> list_filter (f c) (l c)
 219
 220 -- | Parse 'list_zipWith'.
 221 list_zipWith_from
 222  :: forall root ty ast hs ret.
 223  ( ty ~ Type_Root_of_Expr (Expr_List root)
 224  , Expr_From ast root
 225  , Type0_Eq ty
 226  , Type0_Lift   Type_Fun  (Type_of_Expr root)
 227  , Type0_Unlift Type_Fun  (Type_of_Expr root)
 228  , Type0_Lift   Type_List (Type_of_Expr root)
 229  , Type0_Unlift Type_List (Type_of_Expr root)
 230  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 231                    (Error_of_Expr ast root)
 232  , Root_of_Expr root ~ root
 233  ) => ast -> ast -> ast
 234  -> ExprFrom ast (Expr_List root) hs ret
 235 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
 236  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 237         expr_from (Proxy::Proxy root) ast_f ctx $
 238          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 239         expr_from (Proxy::Proxy root) ast_la ctx $
 240          \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
 241         expr_from (Proxy::Proxy root) ast_lb ctx $
 242          \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
 243         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2c) ->
 244         check_type_fun ex ast ty_f_b2c $ \(Type2 Proxy ty_f_b ty_f_c) ->
 245         check_type_list ex ast ty_la $ \(Type1 _ ty_l_a) ->
 246         check_type_list ex ast ty_lb $ \(Type1 _ ty_l_b) ->
 247         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 248         check_type0_eq ex ast ty_f_b ty_l_b $ \Refl ->
 249         check_type0_eq ex ast ty_f_a ty_l_a $ \Refl ->
 250         k (type_list ty_f_c) $ Forall_Repr_with_Context $
 251          \c -> list_zipWith (f c) (la c) (lb c)
 252
 253 -- | Parse 'list_reverse'.
 254 list_reverse_from
 255  :: forall root ty ast hs ret.
 256  ( ty ~ Type_Root_of_Expr (Expr_List root)
 257  , Expr_From ast root
 258  , Type0_Eq ty
 259  , Type0_Lift   Type_List (Type_of_Expr root)
 260  , Type0_Unlift Type_List (Type_of_Expr root)
 261  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 262                    (Error_of_Expr ast root)
 263  , Root_of_Expr root ~ root
 264  ) => ast
 265  -> ExprFrom ast (Expr_List root) hs ret
 266 list_reverse_from ast_l ex ast ctx k =
 267         expr_from (Proxy::Proxy root) ast_l ctx $
 268          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 269         check_type_list ex ast ty_l $ \(Type1 _ _ty_l_a) ->
 270         k ty_l $ Forall_Repr_with_Context $
 271          \c -> list_reverse (l c)