Language/Symantic/Lib/Traversable.hs

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