Language/Symantic/Compiling/Traversable.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Traversable'.
  14 module Language.Symantic.Compiling.Traversable where
  15
  16 import Control.Monad (liftM2)
  17 import Data.Proxy
  18 import Data.String (IsString)
  19 import Data.Text (Text)
  20 import qualified Data.Traversable as Traversable
  21 import Data.Type.Equality ((:~:)(Refl))
  22 import Prelude hiding (traverse)
  23
  24 import Language.Symantic.Typing
  25 import Language.Symantic.Compiling.Term
  26 import Language.Symantic.Compiling.Applicative (Sym_Applicative, tyApplicative)
  27 import Language.Symantic.Interpreting
  28 import Language.Symantic.Transforming.Trans
  29
  30 -- * Class 'Sym_Traversable'
  31 class Sym_Applicative term => Sym_Traversable term where
  32         traverse :: (Traversable t, Applicative f)
  33          => term (a -> f b) -> term (t a) -> term (f (t b))
  34         default traverse :: (Trans tr term, Traversable t, Applicative f)
  35          => tr term (a -> f b) -> tr term (t a) -> tr term (f (t b))
  36         traverse = trans_map2 traverse
  37
  38 type instance Sym_of_Iface (Proxy Traversable) = Sym_Traversable
  39 type instance Consts_of_Iface (Proxy Traversable) = Proxy Traversable ': Consts_imported_by Traversable
  40 type instance Consts_imported_by Traversable = '[]
  41
  42 instance Sym_Traversable HostI where
  43         traverse = liftM2 Traversable.traverse
  44 instance Sym_Traversable TextI where
  45         traverse = textI_app2 "traverse"
  46 instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
  47         traverse = dupI2 sym_Traversable traverse
  48
  49 instance Const_from Text cs => Const_from Text (Proxy Traversable ': cs) where
  50         const_from "Traversable" k = k (ConstZ kind)
  51         const_from s k = const_from s $ k . ConstS
  52 instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
  53         show_const ConstZ{} = "Traversable"
  54         show_const (ConstS c) = show_const c
  55
  56 instance -- Proj_ConC
  57  Proj_ConC cs (Proxy Traversable)
  58 instance -- Term_fromI
  59  ( AST ast
  60  , Lexem ast ~ LamVarName
  61  , Inj_Const (Consts_of_Ifaces is) Traversable
  62  , Inj_Const (Consts_of_Ifaces is) Applicative
  63  , Inj_Const (Consts_of_Ifaces is) (->)
  64  , Proj_Con  (Consts_of_Ifaces is)
  65  , Term_from is ast
  66  ) => Term_fromI is (Proxy Traversable) ast where
  67         term_fromI ast ctx k =
  68                 case ast_lexem ast of
  69                  "traverse" -> traverse_from
  70                  _ -> Left $ Error_Term_unsupported
  71                 where
  72                 traverse_from =
  73                  -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
  74                         from_ast2 ast $ \ast_a2fb ast_ta as ->
  75                         term_from ast_a2fb ctx $ \ty_a2fb (TermLC a2fb) ->
  76                         term_from ast_ta   ctx $ \ty_ta   (TermLC ta) ->
  77                         check_type2 tyFun ast_a2fb ty_a2fb $ \Refl ty_a2fb_a ty_a2fb_fb ->
  78                         check_constraint1 tyApplicative ast_a2fb ty_a2fb_fb $ \Refl Con ty_a2fb_fb_f ty_a2fb_fb_b ->
  79                         check_constraint1 tyTraversable ast_ta   ty_ta      $ \Refl Con ty_ta_t ty_ta_a ->
  80                         check_type (At (Just ast_a2fb) ty_a2fb_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
  81                         k as (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermLC $
  82                          \c -> traverse (a2fb c) (ta c)
  83
  84 -- | The 'Traversable' 'Type'
  85 tyTraversable :: Inj_Const cs Traversable => Type cs Traversable
  86 tyTraversable = TyConst inj_const
  87
  88 sym_Traversable :: Proxy Sym_Traversable
  89 sym_Traversable = Proxy
  90
  91 syTraversable :: IsString a => [Syntax a] -> Syntax a
  92 syTraversable = Syntax "Traversable"