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