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
  51  ( Sym_Tuple2 r1
  52  , Sym_Tuple2 r2
  53  ) => Sym_Tuple2 (Dup r1 r2) where
  54         tuple2 (a1 `Dup` a2) (b1 `Dup` b2) =
  55                 tuple2 a1 b1 `Dup` tuple2 a2 b2
  56         fst (t1 `Dup` t2) = fst t1 `Dup` fst t2
  57         snd (t1 `Dup` t2) = snd t1 `Dup` snd t2
  58
  59 -- * Type 'Expr_Tuple2'
  60 -- | Expression.
  61 data Expr_Tuple2 (root:: *)
  62 type instance Root_of_Expr      (Expr_Tuple2 root)      = root
  63 type instance Type_of_Expr      (Expr_Tuple2 root)      = Type_Tuple2
  64 type instance Sym_of_Expr       (Expr_Tuple2 root) repr = (Sym_Tuple2 repr)
  65 type instance Error_of_Expr ast (Expr_Tuple2 root)      = No_Error_Expr
  66
  67 -- | Parsing utility to check that the given type is a 'Type_Tuple2'
  68 -- or raise 'Error_Expr_Type_mismatch'.
  69 check_type_tuple2
  70  :: forall ast ex root ty h ret.
  71  ( root ~ Root_of_Expr ex
  72  , ty ~ Type_Root_of_Expr ex
  73  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  74  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  75  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  76                    (Error_of_Expr ast root)
  77  )
  78  => Proxy ex -> ast -> ty h
  79  -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
  80  -> Either (Error_of_Expr ast root) ret
  81 check_type_tuple2 ex ast ty k =
  82         case unlift_type $ unType_Root ty of
  83          Just ty_t -> k ty_t
  84          Nothing -> Left $
  85                 error_expr ex $
  86                 Error_Expr_Type_mismatch ast
  87                  (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
  88                  :: ty (Var0, Var0)))
  89                  (Exists_Type ty)
  90
  91 -- | Parse 'tuple2'.
  92 tuple2_from
  93  :: forall root ty ast hs ret.
  94  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
  95  , Eq_Type ty
  96  , Expr_from ast root
  97  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  98  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  99  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 100                    (Error_of_Expr ast root)
 101  , Root_of_Expr root ~ root
 102  ) => ast -> ast
 103  -> Expr_From ast (Expr_Tuple2 root) hs ret
 104 tuple2_from ast_a ast_b _ex _ast ctx k =
 105         expr_from (Proxy::Proxy root) ast_a ctx $
 106          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 107         expr_from (Proxy::Proxy root) ast_b ctx $
 108          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 109         k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
 110          \c -> tuple2 (a c) (b c)
 111
 112 -- | Parse 'fst'.
 113 fst_from
 114  :: forall root ty ast hs ret.
 115  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 116  , Eq_Type ty
 117  , Expr_from ast root
 118  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 119  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 120  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 121                    (Error_of_Expr ast root)
 122  , Root_of_Expr root ~ root
 123  ) => ast
 124  -> Expr_From ast (Expr_Tuple2 root) hs ret
 125 fst_from ast_t ex ast ctx k =
 126         expr_from (Proxy::Proxy root) ast_t ctx $
 127          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 128         check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ ty_a _ty_b) ->
 129         k ty_a $ Forall_Repr_with_Context $
 130          \c -> fst (t c)
 131
 132 -- | Parse 'snd'.
 133 snd_from
 134  :: forall root ty ast hs ret.
 135  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 136  , Eq_Type ty
 137  , Expr_from ast root
 138  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 139  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 140  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 141                    (Error_of_Expr ast root)
 142  , Root_of_Expr root ~ root
 143  ) => ast
 144  -> Expr_From ast (Expr_Tuple2 root) hs ret
 145 snd_from ast_t ex ast ctx k =
 146         expr_from (Proxy::Proxy root) ast_t ctx $
 147          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 148         check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ _ty_a ty_b) ->
 149         k ty_b $ Forall_Repr_with_Context $
 150          \c -> snd (t c)