{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Expression for tuples. module Language.Symantic.Expr.Tuple where import Control.Monad import Data.Monoid import Data.Proxy (Proxy(..)) import qualified Data.Tuple as Tuple import Prelude hiding (maybe, fst, snd) import Language.Symantic.Type import Language.Symantic.Repr import Language.Symantic.Expr.Root import Language.Symantic.Expr.Error import Language.Symantic.Expr.From import Language.Symantic.Trans.Common -- * Class 'Sym_Tuple_Lam' -- | Symantic. class Sym_Tuple2 repr where tuple2 :: repr a -> repr b -> repr (a, b) fst :: repr (a, b) -> repr a snd :: repr (a, b) -> repr b default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b) default fst :: Trans t repr => t repr (a, b) -> t repr a default snd :: Trans t repr => t repr (a, b) -> t repr b tuple2 = trans_map2 tuple2 fst = trans_map1 fst snd = trans_map1 snd instance Sym_Tuple2 Repr_Host where tuple2 = liftM2 (,) fst = liftM Tuple.fst snd = liftM Tuple.snd instance Sym_Tuple2 Repr_Text where tuple2 (Repr_Text a) (Repr_Text b) = Repr_Text $ \_p v -> let p' = precedence_Toplevel in "(" <> a p' v <> ", " <> b p' v <> ")" fst = repr_text_app1 "fst" snd = repr_text_app1 "snd" instance ( Sym_Tuple2 r1 , Sym_Tuple2 r2 ) => Sym_Tuple2 (Dup r1 r2) where tuple2 (a1 `Dup` a2) (b1 `Dup` b2) = tuple2 a1 b1 `Dup` tuple2 a2 b2 fst (t1 `Dup` t2) = fst t1 `Dup` fst t2 snd (t1 `Dup` t2) = snd t1 `Dup` snd t2 -- * Type 'Expr_Tuple2' -- | Expression. data Expr_Tuple2 (root:: *) type instance Root_of_Expr (Expr_Tuple2 root) = root type instance Type_of_Expr (Expr_Tuple2 root) = Type_Tuple2 type instance Sym_of_Expr (Expr_Tuple2 root) repr = (Sym_Tuple2 repr) type instance Error_of_Expr ast (Expr_Tuple2 root) = No_Error_Expr -- | Parsing utility to check that the given type is a 'Type_Tuple2' -- or raise 'Error_Expr_Type_mismatch'. check_type_tuple2 :: forall ast ex root ty h ret. ( root ~ Root_of_Expr ex , ty ~ Type_Root_of_Expr ex , Lift_Type Type_Tuple2 (Type_of_Expr root) , Unlift_Type Type_Tuple2 (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) ) => Proxy ex -> ast -> ty h -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret) -> Either (Error_of_Expr ast root) ret check_type_tuple2 ex ast ty k = case unlift_type $ unType_Root ty of Just ty_t -> k ty_t Nothing -> Left $ error_expr ex $ Error_Expr_Type_mismatch ast (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero) :: ty (Var0, Var0))) (Exists_Type ty) -- | Parse 'tuple2'. tuple2_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_Tuple2 (Type_of_Expr root) , Unlift_Type Type_Tuple2 (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> ast -> Expr_From ast (Expr_Tuple2 root) hs ret tuple2_from ast_a ast_b _ex _ast ctx k = expr_from (Proxy::Proxy root) ast_a ctx $ \(ty_a::ty h_a) (Forall_Repr_with_Context a) -> expr_from (Proxy::Proxy root) ast_b ctx $ \(ty_b::ty h_b) (Forall_Repr_with_Context b) -> k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $ \c -> tuple2 (a c) (b c) -- | Parse 'fst'. fst_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_Tuple2 (Type_of_Expr root) , Unlift_Type Type_Tuple2 (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> Expr_From ast (Expr_Tuple2 root) hs ret fst_from ast_t ex ast ctx k = expr_from (Proxy::Proxy root) ast_t ctx $ \(ty_t::ty h_t) (Forall_Repr_with_Context t) -> check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ ty_a _ty_b) -> k ty_a $ Forall_Repr_with_Context $ \c -> fst (t c) -- | Parse 'snd'. snd_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root) , Eq_Type ty , Expr_from ast root , Lift_Type Type_Tuple2 (Type_of_Expr root) , Unlift_Type Type_Tuple2 (Type_of_Expr root) , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root ) => ast -> Expr_From ast (Expr_Tuple2 root) hs ret snd_from ast_t ex ast ctx k = expr_from (Proxy::Proxy root) ast_t ctx $ \(ty_t::ty h_t) (Forall_Repr_with_Context t) -> check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ _ty_a ty_b) -> k ty_b $ Forall_Repr_with_Context $ \c -> snd (t c)