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)
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
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
instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
instance NameTyOf (,) where
nameTyOf _c = ["Tuple2"] `Mod` ","
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
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 =
[ 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
]
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