{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Traversable'. module Language.Symantic.Compiling.Traversable where import Control.Monad (liftM2) import Data.Proxy import Data.Text (Text) import qualified Data.Traversable as Traversable import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (traverse) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Compiling.Applicative (Sym_Applicative) import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * 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_of_Iface (Proxy Traversable) = Sym_Traversable type instance Consts_of_Iface (Proxy Traversable) = Proxy Traversable ': Consts_imported_by Traversable type instance Consts_imported_by Traversable = '[] instance Sym_Traversable HostI where traverse = liftM2 Traversable.traverse instance Sym_Traversable TextI where traverse = textI_app2 "traverse" instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where traverse = dupI2 (Proxy @Sym_Traversable) traverse instance Const_from Text cs => Const_from Text (Proxy Traversable ': cs) where const_from "Traversable" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where show_const ConstZ{} = "Traversable" show_const (ConstS c) = show_const c instance Proj_ConC 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_Const (Consts_of_Ifaces is) Traversable , Inj_Const (Consts_of_Ifaces is) Applicative , Inj_Const (Consts_of_Ifaces is) (->) , Proj_Con (Consts_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_type2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb -> check_con1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl Con ty_a2fb_fb_f ty_a2fb_fb_b -> check_con1 (ty @Traversable) (At (Just tok_ta) ty_ta) $ \Refl Con ty_ta_t ty_ta_a -> check_type (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)