Language/Symantic/Expr/Tuple.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 -- | Expression for tuples.
   9 module Language.Symantic.Expr.Tuple where
  10
  11 import Data.Proxy (Proxy(..))
  12 import Prelude hiding (maybe)
  13
  14 import Language.Symantic.Type
  15 import Language.Symantic.Trans.Common
  16 import Language.Symantic.Expr.Root
  17 import Language.Symantic.Expr.Error
  18 import Language.Symantic.Expr.From
  19
  20 -- * Class 'Sym_Tuple_Lam'
  21 -- | Symantic.
  22 class Sym_Tuple2 repr where
  23         tuple2 :: repr a -> repr b -> repr (a, b)
  24         default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
  25         tuple2 = trans_map2 tuple2
  26
  27 -- * Type 'Expr_Tuple2'
  28 -- | Expression.
  29 data Expr_Tuple2 (lam:: * -> *) (root:: *)
  30 type instance Root_of_Expr      (Expr_Tuple2 lam root)      = root
  31 type instance Type_of_Expr      (Expr_Tuple2 lam root)      = Type_Tuple2
  32 type instance Sym_of_Expr       (Expr_Tuple2 lam root) repr = (Sym_Tuple2 repr)
  33 type instance Error_of_Expr ast (Expr_Tuple2 lam root)      = No_Error_Expr
  34
  35 instance Constraint_Type1 Functor (Type_Type1 (Proxy ((,) fst)) root) where
  36         constraint_type1 _c Type_Type1{} = Just Dict
  37 instance Constraint_Type1 Functor (Type_Tuple2 root) where
  38         constraint_type1 _c Type_Type2{} = Just Dict
  39 instance Constraint_Type1 Applicative (Type_Type1 (Proxy ((,) fst)) root)
  40
  41 -- | Parsing utility to check that the given type is a 'Type_Tuple2'
  42 -- or raise 'Error_Expr_Type_mismatch'.
  43 check_type_tuple2
  44  :: forall ast ex root ty h ret.
  45  ( root ~ Root_of_Expr ex
  46  , ty ~ Type_Root_of_Expr ex
  47  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  48  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  49  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  50                    (Error_of_Expr ast root)
  51  )
  52  => Proxy ex -> ast -> ty h
  53  -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
  54  -> Either (Error_of_Expr ast root) ret
  55 check_type_tuple2 ex ast ty k =
  56         case unlift_type $ unType_Root ty of
  57          Just ty_t -> k ty_t
  58          Nothing -> Left $
  59                 error_expr ex $
  60                 Error_Expr_Type_mismatch ast
  61                  (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
  62                  :: Type_Root_of_Expr ex (Var0, Var0)))
  63                  (Exists_Type ty)
  64
  65 -- | Parse 'tuple2'.
  66 tuple2_from
  67  :: forall root lam ty ast hs ret.
  68  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 lam root)
  69  , Eq_Type (Type_Root_of_Expr root)
  70  , Expr_from ast root
  71  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  72  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  73  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  74                    (Error_of_Expr ast root)
  75  , Root_of_Expr root ~ root
  76  ) => ast -> ast
  77  -> Expr_From ast (Expr_Tuple2 lam root) hs ret
  78 tuple2_from ast_a ast_b _ex _ast ctx k =
  79         expr_from (Proxy::Proxy root) ast_a ctx $
  80          \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  81         expr_from (Proxy::Proxy root) ast_b ctx $
  82          \(ty_b::Type_Root_of_Expr root h_b) (Forall_Repr_with_Context b) ->
  83         k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
  84                 \c -> tuple2 (a c) (b c)