Language/Symantic/Expr/Tuple.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 -- | Expression for tuples.
  10 module Language.Symantic.Expr.Tuple where
  11
  12 import Control.Monad
  13 import Data.Monoid
  14 import Data.Proxy (Proxy(..))
  15 import qualified Data.Tuple as Tuple
  16 import Prelude hiding (maybe, fst, snd)
  17
  18 import Language.Symantic.Type
  19 import Language.Symantic.Repr
  20 import Language.Symantic.Expr.Root
  21 import Language.Symantic.Expr.Error
  22 import Language.Symantic.Expr.From
  23 import Language.Symantic.Trans.Common
  24
  25 -- * Class 'Sym_Tuple_Lam'
  26 -- | Symantic.
  27 class Sym_Tuple2 repr where
  28         tuple2 :: repr a -> repr b -> repr (a, b)
  29         fst :: repr (a, b) -> repr a
  30         snd :: repr (a, b) -> repr b
  31
  32         default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
  33         default fst :: Trans t repr => t repr (a, b) -> t repr a
  34         default snd :: Trans t repr => t repr (a, b) -> t repr b
  35
  36         tuple2 = trans_map2 tuple2
  37         fst    = trans_map1 fst
  38         snd    = trans_map1 snd
  39 instance Sym_Tuple2 Repr_Host where
  40         tuple2 = liftM2 (,)
  41         fst    = liftM  Tuple.fst
  42         snd    = liftM  Tuple.snd
  43 instance Sym_Tuple2 Repr_Text where
  44         tuple2 (Repr_Text a) (Repr_Text b) =
  45                 Repr_Text $ \_p v ->
  46                         let p' = precedence_Toplevel in
  47                         "(" <> a p' v <> ", " <> b p' v <> ")"
  48         fst = repr_text_app1 "fst"
  49         snd = repr_text_app1 "snd"
  50 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Repr_Dup r1 r2) where
  51         tuple2 = repr_dup2 sym_Tuple2 tuple2
  52         fst    = repr_dup1 sym_Tuple2 fst
  53         snd    = repr_dup1 sym_Tuple2 snd
  54
  55 sym_Tuple2 :: Proxy Sym_Tuple2
  56 sym_Tuple2 = Proxy
  57
  58 -- * Type 'Expr_Tuple2'
  59 -- | Expression.
  60 data Expr_Tuple2 (root:: *)
  61 type instance Root_of_Expr      (Expr_Tuple2 root)      = root
  62 type instance Type_of_Expr      (Expr_Tuple2 root)      = Type_Tuple2
  63 type instance Sym_of_Expr       (Expr_Tuple2 root) repr = (Sym_Tuple2 repr)
  64 type instance Error_of_Expr ast (Expr_Tuple2 root)      = No_Error_Expr
  65
  66 -- | Parsing utility to check that the given type is a 'Type_Tuple2'
  67 -- or raise 'Error_Expr_Type_mismatch'.
  68 check_type_tuple2
  69  :: forall ast ex root ty h ret.
  70  ( root ~ Root_of_Expr ex
  71  , ty ~ Type_Root_of_Expr ex
  72  , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
  73  , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
  74  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  75                    (Error_of_Expr ast root)
  76  )
  77  => Proxy ex -> ast -> ty h
  78  -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
  79  -> Either (Error_of_Expr ast root) ret
  80 check_type_tuple2 ex ast ty k =
  81         case type0_unlift $ unType_Root ty of
  82          Just ty_t -> k ty_t
  83          Nothing -> Left $
  84                 error_expr ex $
  85                 Error_Expr_Type_mismatch ast
  86                  (Exists_Type0 (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
  87                  :: ty (Var0, Var0)))
  88                  (Exists_Type0 ty)
  89
  90 -- | Parse 'tuple2'.
  91 tuple2_from
  92  :: forall root ty ast hs ret.
  93  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
  94  , Type0_Eq ty
  95  , Expr_From ast root
  96  , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
  97  , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
  98  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  99                    (Error_of_Expr ast root)
 100  , Root_of_Expr root ~ root
 101  ) => ast -> ast
 102  -> ExprFrom ast (Expr_Tuple2 root) hs ret
 103 tuple2_from ast_a ast_b _ex _ast ctx k =
 104         expr_from (Proxy::Proxy root) ast_a ctx $
 105          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 106         expr_from (Proxy::Proxy root) ast_b ctx $
 107          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 108         k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
 109          \c -> tuple2 (a c) (b c)
 110
 111 -- | Parse 'fst'.
 112 fst_from
 113  :: forall root ty ast hs ret.
 114  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 115  , Type0_Eq ty
 116  , Expr_From ast root
 117  , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 118  , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 119  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 120                    (Error_of_Expr ast root)
 121  , Root_of_Expr root ~ root
 122  ) => ast
 123  -> ExprFrom ast (Expr_Tuple2 root) hs ret
 124 fst_from ast_t ex ast ctx k =
 125         expr_from (Proxy::Proxy root) ast_t ctx $
 126          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 127         check_type_tuple2 ex ast ty_t $ \(Type2 _ ty_a _ty_b) ->
 128         k ty_a $ Forall_Repr_with_Context $
 129          \c -> fst (t c)
 130
 131 -- | Parse 'snd'.
 132 snd_from
 133  :: forall root ty ast hs ret.
 134  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 135  , Type0_Eq ty
 136  , Expr_From ast root
 137  , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 138  , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 139  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 140                    (Error_of_Expr ast root)
 141  , Root_of_Expr root ~ root
 142  ) => ast
 143  -> ExprFrom ast (Expr_Tuple2 root) hs ret
 144 snd_from ast_t ex ast ctx k =
 145         expr_from (Proxy::Proxy root) ast_t ctx $
 146          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 147         check_type_tuple2 ex ast ty_t $ \(Type2 _ _ty_a ty_b) ->
 148         k ty_b $ Forall_Repr_with_Context $
 149          \c -> snd (t c)