Language/Symantic/Expr/Tuple.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 -- | Expression for 'Tuple'.
   8 module Language.Symantic.Expr.Tuple where
   9
  10 -- import qualified Data.Tuple as Tuple
  11 import Data.Proxy (Proxy(..))
  12 -- import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (maybe)
  14
  15 import Language.Symantic.Type
  16 import Language.Symantic.Repr.Dup
  17 import Language.Symantic.Trans.Common
  18 import Language.Symantic.Expr.Common
  19 import Language.Symantic.Expr.Lambda
  20 import Language.Symantic.Expr.Bool
  21
  22 -- * Class 'Sym_Tuple_Lam'
  23 -- | Symantic.
  24 class Sym_Tuple2 repr where
  25         tuple2 :: repr a -> repr b -> repr (a, b)
  26         default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
  27         tuple2 = trans_map2 tuple2
  28
  29 instance -- Sym_Tuple2 Dup
  30  ( Sym_Tuple2 r1
  31  , Sym_Tuple2 r2
  32  ) => Sym_Tuple2 (Dup r1 r2) where
  33         tuple2 (a1 `Dup` a2) (b1 `Dup` b2) = tuple2 a1 b1 `Dup` tuple2 a2 b2
  34
  35 -- * Type 'Expr_Tuple2'
  36 -- | Expression.
  37 data Expr_Tuple2 (lam:: * -> *) (root:: *)
  38 type instance Root_of_Expr      (Expr_Tuple2 lam root)      = root
  39 type instance Type_of_Expr      (Expr_Tuple2 lam root)      = Type_Tuple2
  40 type instance Sym_of_Expr       (Expr_Tuple2 lam root) repr = (Sym_Tuple2 repr)
  41 type instance Error_of_Expr ast (Expr_Tuple2 lam 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  , Type_Lift   Type_Tuple2 (Type_of_Expr root)
  50  , Type_Unlift Type_Tuple2 (Type_of_Expr root)
  51  , Error_Expr_Lift (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 type_unlift $ unType_Root ty of
  59          Just ty_l -> k ty_l
  60          Nothing -> Left $
  61                 error_expr ex $
  62                 Error_Expr_Type_mismatch ast
  63                  (Exists_Type (type_tuple2 (type_var SZero) (type_var $ SSucc SZero)
  64                  :: Type_Root_of_Expr ex (Zero, Succ Zero)))
  65                  (Exists_Type ty)
  66
  67 -- | Parse 'list_cons'.
  68 tuple2_from
  69  :: forall root lam ty ast hs ret.
  70  ( ty ~ Type_Root_of_Expr (Expr_Tuple2 lam root)
  71  , Eq_Type (Type_Root_of_Expr root)
  72  , Expr_from ast root
  73  , Type_Lift   Type_Tuple2 (Type_of_Expr root)
  74  , Type_Unlift Type_Tuple2 (Type_of_Expr root)
  75  , Error_Expr_Lift (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 lam 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::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
  83         expr_from (Proxy::Proxy root) ast_b ctx $
  84          \(ty_b::Type_Root_of_Expr root 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 -- ** Type 'Expr_Lambda_Tuple2_Bool'
  89 -- | Convenient alias.
  90 type Expr_Lambda_Tuple2_Bool lam
  91  =   Expr_Root (Expr_Alt (Expr_Lambda lam)
  92                          (Expr_Alt (Expr_Tuple2 lam)
  93                                     Expr_Bool))
  94
  95 -- | Convenient alias around 'expr_from'.
  96 expr_lambda_tuple2_bool_from
  97  :: forall lam ast root.
  98  ( Expr_from ast (Expr_Lambda_Tuple2_Bool lam)
  99  , root ~ Expr_Lambda_Tuple2_Bool lam
 100  ) => Proxy lam
 101  -> ast
 102  -> Either (Error_of_Expr ast root)
 103            (Exists_Type_and_Repr (Type_Root_of_Expr root)
 104                                  (Forall_Repr root))
 105 expr_lambda_tuple2_bool_from _lam ast =
 106         expr_from (Proxy::Proxy root) ast
 107          Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
 108                 Right $ Exists_Type_and_Repr ty $
 109                         Forall_Repr $ repr Context_Empty