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, fst, snd)
  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         fst :: repr (a, b) -> repr a
  25         snd :: repr (a, b) -> repr b
  26
  27         default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
  28         default fst :: Trans t repr => t repr (a, b) -> t repr a
  29         default snd :: Trans t repr => t repr (a, b) -> t repr b
  30
  31         tuple2 = trans_map2 tuple2
  32         fst    = trans_map1 fst
  33         snd    = trans_map1 snd
  34
  35 -- * Type 'Expr_Tuple2'
  36 -- | Expression.
  37 data Expr_Tuple2 (root:: *)
  38 type instance Root_of_Expr      (Expr_Tuple2 root)      = root
  39 type instance Type_of_Expr      (Expr_Tuple2 root)      = Type_Tuple2
  40 type instance Sym_of_Expr       (Expr_Tuple2 root) repr = (Sym_Tuple2 repr)
  41 type instance Error_of_Expr ast (Expr_Tuple2 root)      = No_Error_Expr
  42
  43 -- | Parsing utility to check that the given type is a 'Type_Tuple2'
  44 -- or raise 'Error_Expr_Type_mismatch'.
  45 check_type_tuple2
  46  :: forall ast ex root ty h ret.
  47  ( root ~ Root_of_Expr ex
  48  , ty ~ Type_Root_of_Expr ex
  49  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  50  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  51  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  52                    (Error_of_Expr ast root)
  53  )
  54  => Proxy ex -> ast -> ty h
  55  -> (Type_Tuple2 ty h -> Either (Error_of_Expr ast root) ret)
  56  -> Either (Error_of_Expr ast root) ret
  57 check_type_tuple2 ex ast ty k =
  58         case unlift_type $ unType_Root ty of
  59          Just ty_t -> k ty_t
  60          Nothing -> Left $
  61                 error_expr ex $
  62                 Error_Expr_Type_mismatch ast
  63                  (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
  64                  :: ty (Var0, Var0)))
  65                  (Exists_Type ty)
  66
  67 -- | Parse 'tuple2'.
  68 tuple2_from
  69  :: forall root ty ast hs ret.
  70  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
  71  , Eq_Type ty
  72  , Expr_from ast root
  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  , Root_of_Expr root ~ root
  78  ) => ast -> ast
  79  -> Expr_From ast (Expr_Tuple2 root) hs ret
  80 tuple2_from ast_a ast_b _ex _ast ctx k =
  81         expr_from (Proxy::Proxy root) ast_a ctx $
  82          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
  83         expr_from (Proxy::Proxy root) ast_b ctx $
  84          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
  85         k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
  86          \c -> tuple2 (a c) (b c)
  87
  88 -- | Parse 'fst'.
  89 fst_from
  90  :: forall root ty ast hs ret.
  91  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
  92  , Eq_Type ty
  93  , Expr_from ast root
  94  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
  95  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
  96  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  97                    (Error_of_Expr ast root)
  98  , Root_of_Expr root ~ root
  99  ) => ast
 100  -> Expr_From ast (Expr_Tuple2 root) hs ret
 101 fst_from ast_t ex ast ctx k =
 102         expr_from (Proxy::Proxy root) ast_t ctx $
 103          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 104         check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ ty_a _ty_b) ->
 105         k ty_a $ Forall_Repr_with_Context $
 106          \c -> fst (t c)
 107
 108 -- | Parse 'snd'.
 109 snd_from
 110  :: forall root ty ast hs ret.
 111  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
 112  , Eq_Type ty
 113  , Expr_from ast root
 114  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 115  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 116  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 117                    (Error_of_Expr ast root)
 118  , Root_of_Expr root ~ root
 119  ) => ast
 120  -> Expr_From ast (Expr_Tuple2 root) hs ret
 121 snd_from ast_t ex ast ctx k =
 122         expr_from (Proxy::Proxy root) ast_t ctx $
 123          \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
 124         check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ _ty_a ty_b) ->
 125         k ty_b $ Forall_Repr_with_Context $
 126          \c -> snd (t c)