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 (,) = 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 NameTyOf (,) where
  54         nameTyOf _c = ["Tuple2"] `Mod` ","
  55 instance FixityOf (,) where
  56         fixityOf _c = Just $ Fixity2 $ infixN (-1)
  57 instance ClassInstancesFor (,) where
  58         proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
  59          | Just HRefl <- proj_ConstKiTy @_ @(,) c
  60          = case () of
  61                  _ | Just Refl <- proj_Const @Applicative q
  62                    , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
  63                    | Just Refl <- proj_Const @Functor q  -> Just Dict
  64                    | Just Refl <- proj_Const @Foldable q -> Just Dict
  65                    | Just Refl <- proj_Const @Monad q
  66                    , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
  67                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  68                  _ -> Nothing
  69         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
  70          | Just HRefl <- proj_ConstKiTy @_ @(,) c
  71          = case () of
  72                  _ | Just Refl <- proj_Const @Bounded q
  73                    , Just Dict <- proveConstraint (tq `tyApp` a)
  74                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  75                    | Just Refl <- proj_Const @Eq q
  76                    , Just Dict <- proveConstraint (tq `tyApp` a)
  77                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  78                    | Just Refl <- proj_Const @Monoid q
  79                    , Just Dict <- proveConstraint (tq `tyApp` a)
  80                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  81                    | Just Refl <- proj_Const @Ord q
  82                    , Just Dict <- proveConstraint (tq `tyApp` a)
  83                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  84                    | Just Refl <- proj_Const @Show q
  85                    , Just Dict <- proveConstraint (tq `tyApp` a)
  86                    , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
  87                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  88                    | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
  89                  _ -> Nothing
  90         proveConstraintFor _c _q = Nothing
  91 instance TypeInstancesFor (,) where
  92         expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
  93          | Just HRefl <- proj_ConstKi @_ @Element f
  94          , Just HRefl <- proj_ConstKiTy @_ @(,) c
  95          = Just b
  96         expandFamFor _c _len _fam _as = Nothing
  97
  98 -- Compiling
  99 instance
 100  ( Gram_Source src g
 101  , Gram_Alt g
 102  , Gram_Rule g
 103  , Gram_Comment g
 104  , Gram_Term src ss g
 105  , SymInj ss (,)
 106  ) => Gram_Term_AtomsFor src ss g (,) where
 107         g_term_atomsFor =
 108          -- TODO: proper TupleSections
 109          [ rule "teTuple2_2" $
 110                 source $ parens $
 111                 (\a b src ->
 112                         BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
 113                  <$> g_term
 114                  <*  symbol ","
 115                  <*> g_term
 116          , rule "teTuple2" $
 117                 source $
 118                 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
 119                  <$ symbol "(,)"
 120          ]
 121 instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where
 122         moduleFor = ["Tuple2"] `moduleWhere`
 123          [ "fst" := teTuple2_fst
 124          , "snd" := teTuple2_snd
 125          ]
 126
 127 -- ** 'Term's
 128 tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
 129 tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b
 130
 131 teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
 132 teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2
 133 teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))
 134 teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst
 135 teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))
 136 teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd