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                 "[]"
  62         list_cons (Repr_Text x) (Repr_Text xs) =
  63                 Repr_Text $ \p v ->
  64                         let p' = precedence_List_Cons in
  65                         paren p p' $ x p' v <> ":" <> xs p' v
  66         list l = Repr_Text $ \_p v ->
  67                 let p' = precedence_Toplevel in
  68                 "[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]"
  69         list_filter  = repr_text_app2 "list_filter"
  70         list_zipWith = repr_text_app3 "list_zipWith"
  71         list_reverse = repr_text_app1 "list_reverse"
  72 instance
  73  ( Sym_List r1
  74  , Sym_List r2
  75  ) => Sym_List (Dup r1 r2) where
  76         list_empty = list_empty `Dup` list_empty
  77         list_cons (a1 `Dup` a2) (l1 `Dup` l2) = list_cons a1 l1 `Dup` list_cons a2 l2
  78         list l =
  79                 let (l1, l2) =
  80                         foldr (\(x1 `Dup` x2) (xs1, xs2) ->
  81                                 (x1:xs1, x2:xs2)) ([], []) l in
  82                 list l1 `Dup` list l2
  83         list_filter (f1 `Dup` f2) (l1 `Dup` l2) =
  84                 list_filter f1 l1 `Dup` list_filter f2 l2
  85         list_zipWith (f1 `Dup` f2) (la1 `Dup` la2) (lb1 `Dup` lb2) =
  86                 list_zipWith f1 la1 lb1 `Dup` list_zipWith f2 la2 lb2
  87         list_reverse (l1 `Dup` l2) =
  88                 list_reverse l1 `Dup` list_reverse l2
  89
  90 -- * Type 'Expr_List'
  91 -- | Expression.
  92 data Expr_List (root:: *)
  93 type instance Root_of_Expr      (Expr_List root)      = root
  94 type instance Type_of_Expr      (Expr_List root)      = Type_List
  95 type instance Sym_of_Expr       (Expr_List root) repr = (Sym_List repr)
  96 type instance Error_of_Expr ast (Expr_List root)      = No_Error_Expr
  97
  98 -- | Parsing utility to check that the given type is a 'Type_List'
  99 -- or raise 'Error_Expr_Type_mismatch'.
 100 check_type_list
 101  :: forall ast ex root ty h ret.
 102  ( root ~ Root_of_Expr ex
 103  , ty ~ Type_Root_of_Expr ex
 104  , Lift_Type   Type_List (Type_of_Expr root)
 105  , Unlift_Type Type_List (Type_of_Expr root)
 106  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 107                    (Error_of_Expr ast root)
 108  )
 109  => Proxy ex -> ast -> ty h
 110  -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
 111  -> Either (Error_of_Expr ast root) ret
 112 check_type_list ex ast ty k =
 113         case unlift_type $ unType_Root ty of
 114          Just ty_l -> k ty_l
 115          Nothing -> Left $
 116                 error_expr ex $
 117                 Error_Expr_Type_mismatch ast
 118                  (Exists_Type (type_list $ type_var0 SZero
 119                  :: ty [Var0]))
 120                  (Exists_Type ty)
 121
 122 -- | Parse 'list_empty'.
 123 list_empty_from
 124  :: forall root ty ast hs ret.
 125  ( ty ~ Type_Root_of_Expr (Expr_List root)
 126  , Type_from ast ty
 127  , Lift_Type Type_List (Type_of_Expr root)
 128  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 129                    (Error_of_Expr ast root)
 130  , Root_of_Expr root ~ root
 131  ) => ast
 132  -> Expr_From ast (Expr_List root) hs ret
 133 list_empty_from ast_ty_a ex ast _ctx k =
 134         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
 135         type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
 136         k (type_list ty_a) $ Forall_Repr_with_Context $
 137                 Fun.const list_empty
 138
 139 -- | Parse 'list_cons'.
 140 list_cons_from
 141  :: forall root ty ast hs ret.
 142  ( ty ~ Type_Root_of_Expr (Expr_List root)
 143  , Eq_Type ty
 144  , Expr_from ast root
 145  , Lift_Type   Type_List (Type_of_Expr root)
 146  , Unlift_Type Type_List (Type_of_Expr root)
 147  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 148                    (Error_of_Expr ast root)
 149  , Root_of_Expr root ~ root
 150  ) => ast -> ast
 151  -> Expr_From ast (Expr_List root) hs ret
 152 list_cons_from ast_a ast_l ex ast ctx k =
 153         expr_from (Proxy::Proxy root) ast_a ctx $
 154          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 155         expr_from (Proxy::Proxy root) ast_l ctx $
 156          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 157         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 158         check_eq_type ex ast ty_a ty_l_a $ \Refl ->
 159         k (type_list ty_a) $ Forall_Repr_with_Context $
 160          \c -> list_cons (a c) (l c)
 161
 162 -- | Parse 'list'.
 163 list_from
 164  :: forall root ex ty ast hs ret.
 165  ( ty ~ Type_Root_of_Expr (Expr_List root)
 166  , ex ~ Expr_List root
 167  , Eq_Type ty
 168  , Type_from ast ty
 169  , Expr_from ast root
 170  , Lift_Type   Type_List (Type_of_Expr root)
 171  , Unlift_Type Type_List (Type_of_Expr root)
 172  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 173                    (Error_of_Expr ast root)
 174  , Root_of_Expr root ~ root
 175  ) => ast -> [ast]
 176  -> Expr_From ast ex hs ret
 177 list_from ast_ty_a ast_as =
 178         case type_from (Proxy::Proxy ty)
 179          ast_ty_a (Right . Exists_Type) of
 180          Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
 181          Right (Exists_Type ty_a) -> go ty_a [] ast_as
 182         where
 183         go :: ty ty_a
 184            -> [Forall_Repr_with_Context root hs ty_a]
 185            -> [ast]
 186            -> Expr_From ast (Expr_List root) hs ret
 187         go ty_a as [] _ex _ast _ctx k =
 188                 k (type_list ty_a) $ Forall_Repr_with_Context $
 189                  \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
 190         go ty_a as (ast_x:ast_xs) ex ast ctx k =
 191                 expr_from (Proxy::Proxy root) ast_x ctx $
 192                  \(ty_x::ty h_x) x ->
 193                 check_eq_type ex ast ty_a ty_x $ \Refl ->
 194                 go ty_a (x:as) ast_xs ex ast ctx k
 195
 196 -- | Parse 'list_filter'.
 197 list_filter_from
 198  :: forall root ty ast hs ret.
 199  ( ty ~ Type_Root_of_Expr (Expr_List root)
 200  , Eq_Type ty
 201  , Expr_from ast root
 202  , Lift_Type   Type_Bool (Type_of_Expr root)
 203  , Lift_Type   Type_Fun  (Type_of_Expr root)
 204  , Unlift_Type Type_Fun  (Type_of_Expr root)
 205  , Lift_Type   Type_List (Type_of_Expr root)
 206  , Unlift_Type Type_List (Type_of_Expr root)
 207  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 208                    (Error_of_Expr ast root)
 209  , Root_of_Expr root ~ root
 210  ) => ast -> ast
 211  -> Expr_From ast (Expr_List root) hs ret
 212 list_filter_from ast_f ast_l ex ast ctx k =
 213         expr_from (Proxy::Proxy root) ast_f ctx $
 214          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 215         expr_from (Proxy::Proxy root) ast_l ctx $
 216          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 217         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 218          :: Type_Fun ty h_f) ->
 219         check_eq_type ex ast type_bool ty_f_b $ \Refl ->
 220         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
 221         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 222         k ty_l $ Forall_Repr_with_Context $
 223          \c -> list_filter (f c) (l c)
 224
 225 -- | Parse 'list_zipWith'.
 226 list_zipWith_from
 227  :: forall root ty ast hs ret.
 228  ( ty ~ Type_Root_of_Expr (Expr_List root)
 229  , Eq_Type ty
 230  , Expr_from ast root
 231  , Lift_Type   Type_Fun  (Type_of_Expr root)
 232  , Unlift_Type Type_Fun  (Type_of_Expr root)
 233  , Lift_Type   Type_List (Type_of_Expr root)
 234  , Unlift_Type Type_List (Type_of_Expr root)
 235  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 236                    (Error_of_Expr ast root)
 237  , Root_of_Expr root ~ root
 238  ) => ast -> ast -> ast
 239  -> Expr_From ast (Expr_List root) hs ret
 240 list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
 241  -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 242         expr_from (Proxy::Proxy root) ast_f ctx $
 243          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 244         expr_from (Proxy::Proxy root) ast_la ctx $
 245          \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
 246         expr_from (Proxy::Proxy root) ast_lb ctx $
 247          \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
 248         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b2c
 249          :: Type_Fun ty h_f) ->
 250         check_type_fun ex ast ty_f_b2c $ \(Type_Type2 Proxy ty_f_b ty_f_c
 251          :: Type_Fun ty h_f_b2c) ->
 252         check_type_list ex ast ty_la $ \(Type_Type1 _ ty_l_a) ->
 253         check_type_list ex ast ty_lb $ \(Type_Type1 _ ty_l_b) ->
 254         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 255         check_eq_type ex ast ty_f_b ty_l_b $ \Refl ->
 256         check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
 257         k (type_list ty_f_c) $ Forall_Repr_with_Context $
 258          \c -> list_zipWith (f c) (la c) (lb c)
 259
 260 -- | Parse 'list_reverse'.
 261 list_reverse_from
 262  :: forall root ty ast hs ret.
 263  ( ty ~ Type_Root_of_Expr (Expr_List root)
 264  , Eq_Type ty
 265  , Expr_from ast root
 266  , Lift_Type   Type_List (Type_of_Expr root)
 267  , Unlift_Type Type_List (Type_of_Expr root)
 268  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 269                    (Error_of_Expr ast root)
 270  , Root_of_Expr root ~ root
 271  ) => ast
 272  -> Expr_From ast (Expr_List root) hs ret
 273 list_reverse_from ast_l ex ast ctx k =
 274         expr_from (Proxy::Proxy root) ast_l ctx $
 275          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 276         check_type_list ex ast ty_l $ \(Type_Type1 _ _ty_l_a) ->
 277         k ty_l $ Forall_Repr_with_Context $
 278          \c -> list_reverse (l c)