]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Traversable.hs
Move libraries in Lib.
[haskell/symantic.git] / 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.Parsing.Grammar
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming.Trans
18 import Language.Symantic.Lib.Applicative (Sym_Applicative)
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