{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for @(,)@. module Language.Symantic.Lib.Tuple2 where import Data.Semigroup ((<>)) import Prelude hiding (fst, snd) import qualified Data.Tuple as Tuple import qualified Data.MonoTraversable as MT import Language.Symantic import Language.Symantic.Grammar import Language.Symantic.Lib.Function (a0, b1) import Language.Symantic.Lib.MonoFunctor (Element) import Language.Symantic.Lib.Monoid (tyMonoid) -- * Class 'Sym_Tuple2' type instance Sym (,) = Sym_Tuple2 class Sym_Tuple2 term where tuple2 :: term a -> term b -> term (a, b) fst :: term (a, b) -> term a snd :: term (a, b) -> term b default tuple2 :: Sym_Tuple2 (UnT term) => Trans term => term a -> term b -> term (a, b) default fst :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term a default snd :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term b tuple2 = trans2 tuple2 fst = trans1 fst snd = trans1 snd -- Interpreting instance Sym_Tuple2 Eval where tuple2 = eval2 (,) fst = eval1 Tuple.fst snd = eval1 Tuple.snd instance Sym_Tuple2 View where tuple2 (View a) (View b) = View $ \_po v -> "(" <> a (op, SideL) v <> ", " <> b (op, SideR) v <> ")" where op = infixN 0 fst = view1 "fst" snd = view1 "snd" instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where tuple2 = dup2 @Sym_Tuple2 tuple2 fst = dup1 @Sym_Tuple2 fst snd = dup1 @Sym_Tuple2 snd -- Transforming instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term) -- Typing instance FixityOf (,) where fixityOf _c = Just $ Fixity2 $ infixN (-1) instance ClassInstancesFor (,) where proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a)) | Just HRefl <- proj_ConstKiTy @_ @(,) c = case () of _ | Just Refl <- proj_Const @Applicative q , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict | Just Refl <- proj_Const @Functor q -> Just Dict | Just Refl <- proj_Const @Foldable q -> Just Dict | Just Refl <- proj_Const @Monad q , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict | Just Refl <- proj_Const @Traversable q -> Just Dict _ -> Nothing proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b)) | Just HRefl <- proj_ConstKiTy @_ @(,) c = case () of _ | Just Refl <- proj_Const @Bounded q , Just Dict <- proveConstraint (tq `tyApp` a) , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict | Just Refl <- proj_Const @Eq q , Just Dict <- proveConstraint (tq `tyApp` a) , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict | Just Refl <- proj_Const @Monoid q , Just Dict <- proveConstraint (tq `tyApp` a) , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict | Just Refl <- proj_Const @Ord q , Just Dict <- proveConstraint (tq `tyApp` a) , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict | Just Refl <- proj_Const @Show q , Just Dict <- proveConstraint (tq `tyApp` a) , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict _ -> Nothing proveConstraintFor _c _q = Nothing instance TypeInstancesFor (,) where expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ) | Just HRefl <- proj_ConstKi @_ @Element f , Just HRefl <- proj_ConstKiTy @_ @(,) c = Just b expandFamFor _c _len _fam _as = Nothing -- Compiling instance ( Gram_Source src g , Gram_Alt g , Gram_Rule g , Gram_Comment g , Gram_Term src ss g , SymInj ss (,) ) => Gram_Term_AtomsFor src ss g (,) where g_term_atomsFor = -- TODO: proper TupleSections [ rule "teTuple2_2" $ source $ parens $ (\a b src -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b) <$> g_term <* symbol "," <*> g_term , rule "teTuple2" $ source $ (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) <$ symbol "(,)" ] instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where moduleFor = ["Tuple2"] `moduleWhere` [ "fst" := teTuple2_fst , "snd" := teTuple2_snd ] -- ** 'Term's tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b) tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b))) teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2 teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a)) teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b)) teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd