{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
-- | Symantic for @(,)@.
module Language.Symantic.Lib.Tuple2 where
-import Control.Monad (liftM, liftM2)
-import Data.Monoid ((<>))
-import Data.Proxy
-import qualified Data.Tuple as Tuple
-import Data.Type.Equality ((:~:)(Refl))
+import Data.Semigroup ((<>))
import Prelude hiding (fst, snd)
+import qualified Data.Tuple as Tuple
+import qualified Data.MonoTraversable as MT
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+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 :: Trans t term => t term a -> t term b -> t term (a, b)
- default fst :: Trans t term => t term (a, b) -> t term a
- default snd :: Trans t term => t term (a, b) -> t 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 = trans_map2 tuple2
- fst = trans_map1 fst
- snd = trans_map1 snd
-
-type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
-type instance TyConsts_of_Iface (Proxy (,)) = Proxy (,) ': TyConsts_imported_by (,)
-type instance TyConsts_imported_by (,) =
- [ Proxy Applicative
- , Proxy Bounded
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Monad
- , Proxy Monoid
- , Proxy Ord
- , Proxy Show
- , Proxy Traversable
- ]
+ tuple2 = trans2 tuple2
+ fst = trans1 fst
+ snd = trans1 snd
-instance Sym_Tuple2 HostI where
- tuple2 = liftM2 (,)
- fst = liftM Tuple.fst
- snd = liftM Tuple.snd
-instance Sym_Tuple2 TextI where
- tuple2 (TextI a) (TextI b) =
- TextI $ \_po v ->
- "(" <> a (op, L) v <> ", " <> b (op, R) v <> ")"
+-- 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 = textI1 "fst"
- snd = textI1 "snd"
-instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
- tuple2 = dupI2 @Sym_Tuple2 tuple2
- fst = dupI1 @Sym_Tuple2 fst
- snd = dupI1 @Sym_Tuple2 snd
+ 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
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs (,)
- ) => Read_TyNameR TyName cs (Proxy (,) ': rs) where
- read_TyNameR _cs (TyName "(,)") k = k (ty @(,))
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy (,) ': cs) where
- show_TyConst TyConstZ{} = "(,)"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Transforming
+instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
-instance -- Proj_TyConC
- ( Proj_TyConst cs (,)
- , Proj_TyConsts cs (TyConsts_imported_by (,))
- , Proj_TyCon cs
- , Inj_TyConst cs Monoid
- ) => Proj_TyConC cs (Proxy (,)) where
- proj_TyConC _ (TyConst q :$ (TyConst c :$ a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @(,))
+-- Typing
+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_TyConst q (Proxy @Applicative)
- , Just TyCon <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monad)
- , Just TyCon <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
+ _ | 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
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @(,))
+ proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
+ | Just HRefl <- proj_ConstKiTy @_ @(,) c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Bounded)
- , Just TyCon <- proj_TyCon (t :$ a)
- , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ a)
- , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monoid)
- , Just TyCon <- proj_TyCon (t :$ a)
- , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord)
- , Just TyCon <- proj_TyCon (t :$ a)
- , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ a)
- , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
+ _ | 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
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy (,))
- = Token_Term_Tuple2 (EToken meta ts) (EToken meta ts)
- | Token_Term_Tuple2_fst (EToken meta ts)
- | Token_Term_Tuple2_snd (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) (,)
- , Compile is
- ) => CompileI is (Proxy (,)) where
- compileI tok ctx k =
- case tok of
- Token_Term_Tuple2 tok_a tok_b ->
- -- (,) :: a -> b -> (a, b)
- compileO tok_a ctx $ \ty_a (TermO a) ->
- compileO tok_b ctx $ \ty_b (TermO b) ->
- k (ty @(,) :$ ty_a :$ ty_b) $ TermO $
- \c -> tuple2 (a c) (b c)
- Token_Term_Tuple2_fst tok_ab ->
- -- fst :: (a, b) -> a
- compileO tok_ab ctx $ \ty_ab (TermO ab) ->
- check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
- k ty_a $ TermO $
- \c -> fst (ab c)
- Token_Term_Tuple2_snd tok_ab ->
- -- snd :: (a, b) -> b
- compileO tok_ab ctx $ \ty_ab (TermO ab) ->
- check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
- k ty_b $ TermO $
- \c -> snd (ab c)
-instance -- TokenizeT
- Inj_Token meta ts (,) =>
- TokenizeT meta ts (Proxy (,)) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize1 "fst" infixN5 Token_Term_Tuple2_fst
- , tokenize1 "snd" infixN5 Token_Term_Tuple2_snd
- ]
- }
-instance -- Gram_Term_AtomsT
- ( Alt g
+ 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_Lexer g
- , Gram_Meta meta g
- , Gram_Term ts meta g
- , Inj_Token meta ts (->)
- , Inj_Token meta ts (,)
- ) => Gram_Term_AtomsT meta ts (Proxy (,)) g where
- term_atomsT _t =
- [ rule "term_tuple2" $
- metaG $ parens $
- (\a b meta -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
- <$> termG
+ , 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 ","
- <*> termG
- , rule "term_tuple2" $
- metaG $
- (\meta -> ProTokLam $ \a -> ProTokLam $ \b -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
+ <*> 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
sourcephile / git / haskell / symantic.git / blobdiff