]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Traversable.hs
Rename Term_Name -> TeName
[haskell/symantic.git] / symantic-lib / 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 TyConsts_of_Iface (Proxy Traversable) = Proxy Traversable ': TyConsts_imported_by Traversable
29 type instance TyConsts_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 @Sym_Traversable traverse
37
38 instance
39 ( Read_TyNameR TyName cs rs
40 , Inj_TyConst cs Traversable
41 ) => Read_TyNameR TyName cs (Proxy Traversable ': rs) where
42 read_TyNameR _cs (TyName "Traversable") k = k (ty @Traversable)
43 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
44 instance Show_TyConst cs => Show_TyConst (Proxy Traversable ': cs) where
45 show_TyConst TyConstZ{} = "Traversable"
46 show_TyConst (TyConstS c) = show_TyConst c
47
48 instance Proj_TyConC 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_TyConst cs Traversable
55 , Inj_TyConst cs Applicative
56 , Inj_TyConst cs (->)
57 , Proj_TyCon cs
58 , Compile cs is
59 ) => CompileI cs 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_TyEq2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb ->
67 check_TyCon1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl TyCon ty_a2fb_fb_f ty_a2fb_fb_b ->
68 check_TyCon1 (ty @Traversable) (At (Just tok_ta) ty_ta) $ \Refl TyCon ty_ta_t ty_ta_a ->
69 check_TyEq
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