+{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Traversable'.
module Language.Symantic.Lib.Traversable where
-import Control.Monad (liftM2)
-import Data.Proxy
-import qualified Data.Traversable as Traversable
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (traverse)
+import qualified Data.Traversable as Traversable
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Applicative (Sym_Applicative)
+import Language.Symantic
+import Language.Symantic.Lib.Applicative (tyApplicative)
+import Language.Symantic.Lib.Function (a0, b1)
+import Language.Symantic.Lib.Functor (f2)
-- * Class 'Sym_Traversable'
-class Sym_Applicative term => Sym_Traversable term where
- traverse :: (Traversable t, Applicative f)
- => term (a -> f b) -> term (t a) -> term (f (t b))
- default traverse :: (Trans tr term, Traversable t, Applicative f)
- => tr term (a -> f b) -> tr term (t a) -> tr term (f (t b))
- traverse = trans_map2 traverse
+type instance Sym (Proxy Traversable) = Sym_Traversable
+class Sym_Traversable term where
+ traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
+ default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
+ traverse = trans2 traverse
+
+-- Interpreting
+instance Sym_Traversable Eval where
+ traverse = eval2 Traversable.traverse
+instance Sym_Traversable View where
+ traverse = view2 "traverse"
+instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Dup r1 r2) where
+ traverse = dup2 @Sym_Traversable traverse
+
+-- Transforming
+instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term)
-type instance Sym_of_Iface (Proxy Traversable) = Sym_Traversable
-type instance TyConsts_of_Iface (Proxy Traversable) = Proxy Traversable ': TyConsts_imported_by Traversable
-type instance TyConsts_imported_by Traversable = '[]
+-- Typing
+instance FixityOf Traversable
+instance ClassInstancesFor Traversable
+instance TypeInstancesFor Traversable
-instance Sym_Traversable HostI where
- traverse = liftM2 Traversable.traverse
-instance Sym_Traversable TextI where
- traverse = textI2 "traverse"
-instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
- traverse = dupI2 (Proxy @Sym_Traversable) traverse
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Traversable
+instance (Source src, Inj_Sym ss Traversable) => ModuleFor src ss Traversable where
+ moduleFor _s = ["Traversable"] `moduleWhere`
+ [ "traverse" := teTraversable_traverse
+ ]
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Traversable
- ) => Read_TyNameR TyName cs (Proxy Traversable ': rs) where
- read_TyNameR _cs (TyName "Traversable") k = k (ty @Traversable)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Traversable ': cs) where
- show_TyConst TyConstZ{} = "Traversable"
- show_TyConst (TyConstS c) = show_TyConst c
+-- ** 'Type's
+tyTraversable :: Source src => Type src vs a -> Type src vs (Traversable a)
+tyTraversable a = tyConstLen @(K Traversable) @Traversable (lenVars a) `tyApp` a
-instance Proj_TyConC cs (Proxy Traversable)
-data instance TokenT meta (ts::[*]) (Proxy Traversable)
- = Token_Term_Traversable_traverse (EToken meta ts) (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Traversable))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Traversable))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Traversable
- , Inj_TyConst (TyConsts_of_Ifaces is) Applicative
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Traversable) where
- compileI tok ctx k =
- case tok of
- Token_Term_Traversable_traverse tok_a2fb tok_ta ->
- -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
- compileO tok_a2fb ctx $ \ty_a2fb (TermO a2fb) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb ->
- check_TyCon1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl TyCon ty_a2fb_fb_f ty_a2fb_fb_b ->
- check_TyCon1 (ty @Traversable) (At (Just tok_ta) ty_ta) $ \Refl TyCon ty_ta_t ty_ta_a ->
- check_TyEq
- (At (Just tok_a2fb) ty_a2fb_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- k (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermO $
- \c -> traverse (a2fb c) (ta c)
-instance -- TokenizeT
- Inj_Token meta ts Traversable =>
- TokenizeT meta ts (Proxy Traversable) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "traverse" infixN5 Token_Term_Traversable_traverse
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Traversable) g
+-- * 'Term's
+teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))
+teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse
+ where
+ t :: Source src => Inj_Len vs => Inj_Kind (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
+ t = tyVar "t" $ VarS $ VarS $ VarS varZ
sourcephile / git / haskell / symantic.git / blobdiff