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