symantic-lib/Language/Symantic/Lib/Tuple2.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
   4 -- | Symantic for @(,)@.
   5 module Language.Symantic.Lib.Tuple2 where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Monoid ((<>))
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Prelude hiding (fst, snd)
  12 import qualified Data.Tuple as Tuple
  13 import qualified Data.MonoTraversable as MT
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming
  20 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
  21
  22 -- * Class 'Sym_Tuple2'
  23 class Sym_Tuple2 term where
  24         tuple2 :: term a -> term b -> term (a, b)
  25         fst :: term (a, b) -> term a
  26         snd :: term (a, b) -> term b
  27
  28         default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
  29         default fst :: Trans t term => t term (a, b) -> t term a
  30         default snd :: Trans t term => t term (a, b) -> t term b
  31
  32         tuple2 = trans_map2 tuple2
  33         fst    = trans_map1 fst
  34         snd    = trans_map1 snd
  35
  36 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
  37 type instance TyConsts_of_Iface (Proxy (,)) = Proxy (,) ': TyConsts_imported_by (Proxy (,))
  38 type instance TyConsts_imported_by (Proxy (,)) =
  39  [ Proxy Applicative
  40  , Proxy Bounded
  41  , Proxy Eq
  42  , Proxy Foldable
  43  , Proxy Functor
  44  , Proxy Monad
  45  , Proxy MT.MonoFoldable
  46  , Proxy MT.MonoFunctor
  47  , Proxy Monoid
  48  , Proxy Ord
  49  , Proxy Show
  50  , Proxy Traversable
  51  ]
  52
  53 instance Sym_Tuple2 HostI where
  54         tuple2 = liftM2 (,)
  55         fst    = liftM  Tuple.fst
  56         snd    = liftM  Tuple.snd
  57 instance Sym_Tuple2 TextI where
  58         tuple2 (TextI a) (TextI b) =
  59                 TextI $ \_po v ->
  60                         "(" <> a (op, L) v <> ", " <> b (op, R) v <> ")"
  61                         where op = infixN 0
  62         fst = textI1 "fst"
  63         snd = textI1 "snd"
  64 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
  65         tuple2 = dupI2 @Sym_Tuple2 tuple2
  66         fst    = dupI1 @Sym_Tuple2 fst
  67         snd    = dupI1 @Sym_Tuple2 snd
  68
  69 instance
  70  ( Read_TyNameR TyName cs rs
  71  , Inj_TyConst cs (,)
  72  ) => Read_TyNameR TyName cs (Proxy (,) ': rs) where
  73         read_TyNameR _cs (TyName "(,)") k = k (ty @(,))
  74         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  75 instance Show_TyConst cs => Show_TyConst (Proxy (,) ': cs) where
  76         show_TyConst TyConstZ{} = "(,)"
  77         show_TyConst (TyConstS c) = show_TyConst c
  78
  79 instance -- Proj_TyFamC TyFam_MonoElement
  80  ( Proj_TyConst cs (,)
  81  ) => Proj_TyFamC cs TyFam_MonoElement (,) where
  82         proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
  83          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  84          , Just Refl <- proj_TyConst c (Proxy @(,))
  85          = Just ty_b
  86         proj_TyFamC _c _fam _ty = Nothing
  87
  88 instance -- Proj_TyConC
  89  ( Proj_TyConst cs (,)
  90  , Proj_TyConsts cs (TyConsts_imported_by (Proxy (,)))
  91  , Proj_TyCon cs
  92  , Inj_TyConst cs Monoid
  93  ) => Proj_TyConC cs (Proxy (,)) where
  94         proj_TyConC _ (TyConst q :$ (TyConst c :$ a))
  95          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  96          , Just Refl <- proj_TyConst c (Proxy @(,))
  97          = case () of
  98                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative)
  99                    , Just TyCon  <- proj_TyCon (ty @Monoid :$ a)     -> Just TyCon
 100                    | Just Refl <- proj_TyConst q (Proxy @Functor)  -> Just TyCon
 101                    | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
 102                    | Just Refl <- proj_TyConst q (Proxy @Monad)
 103                    , Just TyCon  <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
 104                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
 105                  _ -> Nothing
 106         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
 107          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 108          , Just Refl <- proj_TyConst c (Proxy @(,))
 109          = case () of
 110                  _ | Just Refl <- proj_TyConst q (Proxy @Bounded)
 111                    , Just TyCon  <- proj_TyCon (t :$ a)
 112                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 113                    | Just Refl <- proj_TyConst q (Proxy @Eq)
 114                    , Just TyCon  <- proj_TyCon (t :$ a)
 115                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 116                    | Just Refl <- proj_TyConst q (Proxy @Monoid)
 117                    , Just TyCon  <- proj_TyCon (t :$ a)
 118                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 119                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 120                    , Just TyCon  <- proj_TyCon (t :$ a)
 121                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 122                    | Just Refl <- proj_TyConst q (Proxy @Show)
 123                    , Just TyCon  <- proj_TyCon (t :$ a)
 124                    , Just TyCon  <- proj_TyCon (t :$ b) -> Just TyCon
 125                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
 126                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)  -> Just TyCon
 127                  _ -> Nothing
 128         proj_TyConC _c _q = Nothing
 129 data instance TokenT meta (ts::[*]) (Proxy (,))
 130  = Token_Term_Tuple2     (EToken meta ts) (EToken meta ts)
 131  | Token_Term_Tuple2_fst (EToken meta ts)
 132  | Token_Term_Tuple2_snd (EToken meta ts)
 133 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
 134 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
 135
 136 instance -- CompileI
 137  ( Inj_TyConst cs (,)
 138  , Compile cs is
 139  ) => CompileI cs is (Proxy (,)) where
 140         compileI tok ctx k =
 141                 case tok of
 142                  Token_Term_Tuple2 tok_a tok_b ->
 143                         -- (,) :: a -> b -> (a, b)
 144                         compile tok_a ctx $ \ty_a (Term a) ->
 145                         compile tok_b ctx $ \ty_b (Term b) ->
 146                         k (ty @(,) :$ ty_a :$ ty_b) $ Term $
 147                          \c -> tuple2 (a c) (b c)
 148                  Token_Term_Tuple2_fst tok_ab ->
 149                         -- fst :: (a, b) -> a
 150                         compile tok_ab ctx $ \ty_ab (Term ab) ->
 151                         check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
 152                         k ty_a $ Term $
 153                          \c -> fst (ab c)
 154                  Token_Term_Tuple2_snd tok_ab ->
 155                         -- snd :: (a, b) -> b
 156                         compile tok_ab ctx $ \ty_ab (Term ab) ->
 157                         check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
 158                         k ty_b $ Term $
 159                          \c -> snd (ab c)
 160 instance -- TokenizeT
 161  Inj_Token meta ts (,) =>
 162  TokenizeT meta ts (Proxy (,)) where
 163         tokenizeT _t = mempty
 164          { tokenizers_infix = tokenizeTMod []
 165                  [ tokenize1 "fst" infixN5 Token_Term_Tuple2_fst
 166                  , tokenize1 "snd" infixN5 Token_Term_Tuple2_snd
 167                  ]
 168          }
 169 instance -- Gram_Term_AtomsT
 170  ( Alt g
 171  , Gram_Rule g
 172  , Gram_Lexer g
 173  , Gram_Meta meta g
 174  , Gram_Term ts meta g
 175  , Inj_Token meta ts (->)
 176  , Inj_Token meta ts (,)
 177  ) => Gram_Term_AtomsT meta ts (Proxy (,)) g where
 178         gs_term_atomsT _t =
 179          [ rule "term_tuple2" $
 180                 metaG $ parens $
 181                 (\a b meta -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
 182                  <$> g_term
 183                  <*  symbol ","
 184                  <*> g_term
 185          , rule "term_tuple2" $
 186                 metaG $
 187                 (\meta -> ProTokLam $ \a -> ProTokLam $ \b -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
 188                  <$ symbol "(,)"
 189          ]