]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Traversable.hs
Fix lambda application.
[haskell/symantic.git] / 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"