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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for @(,)@.
   4 module Language.Symantic.Lib.Tuple2 where
   5
   6 import Data.Semigroup ((<>))
   7 import Prelude hiding (fst, snd)
   8 import qualified Data.Tuple as Tuple
   9 import qualified Data.MonoTraversable as MT
  10
  11 import Language.Symantic
  12 import Language.Symantic.Grammar
  13 import Language.Symantic.Lib.Function (a0, b1)
  14 import Language.Symantic.Lib.MonoFunctor (Element)
  15 import Language.Symantic.Lib.Monoid (tyMonoid)
  16
  17 -- * Class 'Sym_Tuple2'
  18 type instance Sym (Proxy (,)) = Sym_Tuple2
  19 class Sym_Tuple2 term where
  20         tuple2 :: term a -> term b -> term (a, b)
  21         fst :: term (a, b) -> term a
  22         snd :: term (a, b) -> term b
  23
  24         default tuple2 :: Sym_Tuple2 (UnT term) => Trans term => term a -> term b -> term (a, b)
  25         default fst    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term a
  26         default snd    :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term b
  27
  28         tuple2 = trans2 tuple2
  29         fst    = trans1 fst
  30         snd    = trans1 snd
  31
  32 -- Interpreting
  33 instance Sym_Tuple2 Eval where
  34         tuple2 = eval2 (,)
  35         fst    = eval1 Tuple.fst
  36         snd    = eval1 Tuple.snd
  37 instance Sym_Tuple2 View where
  38         tuple2 (View a) (View b) =
  39                 View $ \_po v ->
  40                         "(" <> a (op, SideL) v <> ", " <> b (op, SideR) v <> ")"
  41                         where op = infixN 0
  42         fst = view1 "fst"
  43         snd = view1 "snd"
  44 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where
  45         tuple2 = dup2 @Sym_Tuple2 tuple2
  46         fst    = dup1 @Sym_Tuple2 fst
  47         snd    = dup1 @Sym_Tuple2 snd
  48
  49 -- Transforming
  50 instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
  51
  52 -- Typing
  53 instance FixityOf (,) where
  54         fixityOf _c = Fixity2 $ infixN (-1)
  55 instance ClassInstancesFor (,) where
  56         proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
  57          | Just HRefl <- proj_ConstKiTy @_ @(,) c
  58          = case () of
  59                  _ | Just Refl <- proj_Const @Applicative q
  60                    , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
  61                    | Just Refl <- proj_Const @Functor q  -> Just Dict
  62                    | Just Refl <- proj_Const @Foldable q -> Just Dict
  63                    | Just Refl <- proj_Const @Monad q
  64                    , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
  65                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  66                  _ -> Nothing
  67         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
  68          | Just HRefl <- proj_ConstKiTy @_ @(,) c
  69          = case () of
  70                  _ | Just Refl <- proj_Const @Bounded q
  71                    , Just Dict <- proveConstraint (tq `tyApp` a)
  72                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  73                    | Just Refl <- proj_Const @Eq q
  74                    , Just Dict <- proveConstraint (tq `tyApp` a)
  75                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  76                    | Just Refl <- proj_Const @Monoid q
  77                    , Just Dict <- proveConstraint (tq `tyApp` a)
  78                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  79                    | Just Refl <- proj_Const @Ord q
  80                    , Just Dict <- proveConstraint (tq `tyApp` a)
  81                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  82                    | Just Refl <- proj_Const @Show q
  83                    , Just Dict <- proveConstraint (tq `tyApp` a)
  84                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  85                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  86                    | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
  87                  _ -> Nothing
  88         proveConstraintFor _c _q = Nothing
  89 instance TypeInstancesFor (,) where
  90         expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
  91          | Just HRefl <- proj_ConstKi @_ @Element f
  92          , Just HRefl <- proj_ConstKiTy @_ @(,) c
  93          = Just b
  94         expandFamFor _c _len _fam _as = Nothing
  95
  96 -- Compiling
  97 instance
  98  ( Gram_Source src g
  99  , Gram_Alt g
 100  , Gram_Rule g
 101  , Gram_Comment g
 102  , Gram_Term src ss g
 103  , Inj_Sym ss (,)
 104  ) => Gram_Term_AtomsFor src ss g (,) where
 105         g_term_atomsFor =
 106          -- TODO: proper TupleSections
 107          [ rule "teTuple2_2" $
 108                 g_source $ parens $
 109                 (\a b src ->
 110                         BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
 111                  <$> g_term
 112                  <*  symbol ","
 113                  <*> g_term
 114          , rule "teTuple2" $
 115                 g_source $
 116                 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
 117                  <$ symbol "(,)"
 118          ]
 119 instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where
 120         moduleFor = ["Tuple2"] `moduleWhere`
 121          [ "fst" := teTuple2_fst
 122          , "snd" := teTuple2_snd
 123          ]
 124
 125 -- ** 'Term's
 126 tyTuple2 :: Source src => Inj_Len vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
 127 tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b
 128
 129 teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
 130 teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2
 131 teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))
 132 teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst
 133 teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))
 134 teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd