Language/Symantic/Compiling/Traversable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Traversable'.
   4 module Language.Symantic.Compiling.Traversable where
   5
   6 import Control.Monad (liftM2)
   7 import Data.Proxy
   8 import Data.Text (Text)
   9 import qualified Data.Traversable as Traversable
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Prelude hiding (traverse)
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling.Term
  16 import Language.Symantic.Compiling.Applicative (Sym_Applicative)
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  19
  20 -- * Class 'Sym_Traversable'
  21 class Sym_Applicative term => Sym_Traversable term where
  22         traverse :: (Traversable t, Applicative f)
  23          => term (a -> f b) -> term (t a) -> term (f (t b))
  24         default traverse :: (Trans tr term, Traversable t, Applicative f)
  25          => tr term (a -> f b) -> tr term (t a) -> tr term (f (t b))
  26         traverse = trans_map2 traverse
  27
  28 type instance Sym_of_Iface (Proxy Traversable) = Sym_Traversable
  29 type instance Consts_of_Iface (Proxy Traversable) = Proxy Traversable ': Consts_imported_by Traversable
  30 type instance Consts_imported_by Traversable = '[]
  31
  32 instance Sym_Traversable HostI where
  33         traverse = liftM2 Traversable.traverse
  34 instance Sym_Traversable TextI where
  35         traverse = textI2 "traverse"
  36 instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
  37         traverse = dupI2 (Proxy @Sym_Traversable) traverse
  38
  39 instance Const_from Text cs => Const_from Text (Proxy Traversable ': cs) where
  40         const_from "Traversable" k = k (ConstZ kind)
  41         const_from s k = const_from s $ k . ConstS
  42 instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
  43         show_const ConstZ{} = "Traversable"
  44         show_const (ConstS c) = show_const c
  45
  46 instance Proj_ConC cs (Proxy Traversable)
  47 data instance TokenT meta (ts::[*]) (Proxy Traversable)
  48  = Token_Term_Traversable_traverse (EToken meta ts) (EToken meta ts)
  49 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Traversable))
  50 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Traversable))
  51 instance -- CompileI
  52  ( Inj_Const (Consts_of_Ifaces is) Traversable
  53  , Inj_Const (Consts_of_Ifaces is) Applicative
  54  , Inj_Const (Consts_of_Ifaces is) (->)
  55  , Proj_Con  (Consts_of_Ifaces is)
  56  , Compile is
  57  ) => CompileI is (Proxy Traversable) where
  58         compileI tok ctx k =
  59                 case tok of
  60                  Token_Term_Traversable_traverse tok_a2fb tok_ta ->
  61                         -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
  62                         compileO tok_a2fb ctx $ \ty_a2fb (TermO a2fb) ->
  63                         compileO tok_ta   ctx $ \ty_ta   (TermO ta) ->
  64                         check_type2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb ->
  65                         check_con1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl Con ty_a2fb_fb_f ty_a2fb_fb_b ->
  66                         check_con1 (ty @Traversable) (At (Just tok_ta)   ty_ta)      $ \Refl Con ty_ta_t ty_ta_a ->
  67                         check_type
  68                          (At (Just tok_a2fb) ty_a2fb_a)
  69                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
  70                         k (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermO $
  71                          \c -> traverse (a2fb c) (ta c)