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 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.Parsing.Grammar
  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
  40  ( Read_TypeNameR Type_Name cs rs
  41  , Inj_Const cs Traversable
  42  ) => Read_TypeNameR Type_Name cs (Proxy Traversable ': rs) where
  43         read_typenameR _cs (Type_Name "Traversable") k = k (ty @Traversable)
  44         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  45 instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
  46         show_const ConstZ{} = "Traversable"
  47         show_const (ConstS c) = show_const c
  48
  49 instance Proj_ConC cs (Proxy Traversable)
  50 data instance TokenT meta (ts::[*]) (Proxy Traversable)
  51  = Token_Term_Traversable_traverse (EToken meta ts) (EToken meta ts)
  52 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Traversable))
  53 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Traversable))
  54 instance -- CompileI
  55  ( Inj_Const (Consts_of_Ifaces is) Traversable
  56  , Inj_Const (Consts_of_Ifaces is) Applicative
  57  , Inj_Const (Consts_of_Ifaces is) (->)
  58  , Proj_Con  (Consts_of_Ifaces is)
  59  , Compile is
  60  ) => CompileI is (Proxy Traversable) where
  61         compileI tok ctx k =
  62                 case tok of
  63                  Token_Term_Traversable_traverse tok_a2fb tok_ta ->
  64                         -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
  65                         compileO tok_a2fb ctx $ \ty_a2fb (TermO a2fb) ->
  66                         compileO tok_ta   ctx $ \ty_ta   (TermO ta) ->
  67                         check_type2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb ->
  68                         check_con1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl Con ty_a2fb_fb_f ty_a2fb_fb_b ->
  69                         check_con1 (ty @Traversable) (At (Just tok_ta)   ty_ta)      $ \Refl Con ty_ta_t ty_ta_a ->
  70                         check_type
  71                          (At (Just tok_a2fb) ty_a2fb_a)
  72                          (At (Just tok_ta) ty_ta_a) $ \Refl ->
  73                         k (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermO $
  74                          \c -> traverse (a2fb c) (ta c)
  75 instance -- TokenizeT
  76  Inj_Token meta ts Traversable =>
  77  TokenizeT meta ts (Proxy Traversable) where
  78         tokenizeT _t = mempty
  79          { tokenizers_infix = tokenizeTMod []
  80                  [ tokenize2 "traverse" infixN5 Token_Term_Traversable_traverse
  81                  ]
  82          }
  83 instance Gram_Term_AtomsT meta ts (Proxy Traversable) g