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