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 'Tuple'.
   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.Common
  17
  18 -- * Class 'Sym_Tuple_Lam'
  19 -- | Symantic.
  20 class Sym_Tuple2 repr where
  21         tuple2 :: repr a -> repr b -> repr (a, b)
  22         default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
  23         tuple2 = trans_map2 tuple2
  24
  25 instance Constraint_Type1 Functor (Type_Type1 (Proxy ((,) fst)) root) where
  26         constraint_type1 _c Type_Type1{} = Just Dict
  27
  28 -- * Type 'Expr_Tuple2'
  29 -- | Expression.
  30 data Expr_Tuple2 (lam:: * -> *) (root:: *)
  31 type instance Root_of_Expr      (Expr_Tuple2 lam root)      = root
  32 type instance Type_of_Expr      (Expr_Tuple2 lam root)      = Type_Tuple2
  33 type instance Sym_of_Expr       (Expr_Tuple2 lam root) repr = (Sym_Tuple2 repr)
  34 type instance Error_of_Expr ast (Expr_Tuple2 lam root)      = No_Error_Expr
  35
  36 -- | Parsing utility to check that the given type is a 'Type_Tuple2'
  37 -- or raise 'Error_Expr_Type_mismatch'.
  38 check_type_tuple2
  39  :: forall ast ex root ty h ret.
  40  ( root ~ Root_of_Expr ex
  41  , ty ~ Type_Root_of_Expr ex
  42  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  43  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  44  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  45                    (Error_of_Expr ast root)
  46  )
  47  => Proxy ex -> ast -> ty h
  48  -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
  49  -> Either (Error_of_Expr ast root) ret
  50 check_type_tuple2 ex ast ty k =
  51         case unlift_type $ unType_Root ty of
  52          Just ty_l -> k ty_l
  53          Nothing -> Left $
  54                 error_expr ex $
  55                 Error_Expr_Type_mismatch ast
  56                  (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
  57                  :: Type_Root_of_Expr ex (Var0, Var0)))
  58                  (Exists_Type ty)
  59
  60 -- | Parse 'tuple2'.
  61 tuple2_from
  62  :: forall root lam ty ast hs ret.
  63  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 lam root)
  64  , Eq_Type (Type_Root_of_Expr root)
  65  , Expr_from ast root
  66  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  67  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  68  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  69                    (Error_of_Expr ast root)
  70  , Root_of_Expr root ~ root
  71  ) => ast -> ast
  72  -> Expr_From ast (Expr_Tuple2 lam root) hs ret
  73 tuple2_from ast_a ast_b _ex _ast ctx k =
  74         expr_from (Proxy::Proxy root) ast_a ctx $
  75          \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  76         expr_from (Proxy::Proxy root) ast_b ctx $
  77          \(ty_b::Type_Root_of_Expr root h_b) (Forall_Repr_with_Context b) ->
  78         k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
  79                 \c -> tuple2 (a c) (b c)