]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Traversable.hs
factorizing Type1_From ast Type0
[haskell/symantic.git] / Language / Symantic / Expr / Traversable.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE GADTs #-}
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 -- | Expression for 'Traversable'.
14 module Language.Symantic.Expr.Traversable where
15
16 import Control.Monad
17 import Data.Traversable (Traversable)
18 import qualified Data.Traversable as Traversable
19 import Data.Proxy (Proxy(..))
20 import Data.Type.Equality ((:~:)(Refl))
21 import Prelude hiding (Traversable(..))
22
23 import Language.Symantic.Type
24 import Language.Symantic.Repr
25 import Language.Symantic.Expr.Root
26 import Language.Symantic.Expr.Error
27 import Language.Symantic.Expr.From
28 import Language.Symantic.Expr.Lambda
29 import Language.Symantic.Expr.Applicative
30 import Language.Symantic.Trans.Common
31
32 -- * Class 'Sym_Traversable'
33 -- | Symantic.
34 class Sym_Applicative repr => Sym_Traversable repr where
35 traverse :: (Traversable t, Applicative f)
36 => repr ((->) a (f b)) -> repr (t a) -> repr (f (t b))
37 default traverse :: (Trans tr repr, Traversable t, Applicative f)
38 => tr repr ((->) a (f b)) -> tr repr (t a) -> tr repr (f (t b))
39 traverse = trans_map2 traverse
40 instance Sym_Traversable Repr_Host where
41 traverse = liftM2 Traversable.traverse
42 instance Sym_Traversable Repr_Text where
43 traverse = repr_text_app2 "traverse"
44 instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (Repr_Dup r1 r2) where
45 traverse = repr_dup2 sym_Traversable traverse
46
47 sym_Traversable :: Proxy Sym_Traversable
48 sym_Traversable = Proxy
49
50 -- * Type 'Expr_Traversable'
51 -- | Expression.
52 data Expr_Traversable (root:: *)
53 type instance Root_of_Expr (Expr_Traversable root) = root
54 type instance Type_of_Expr (Expr_Traversable root) = No_Type
55 type instance Sym_of_Expr (Expr_Traversable root) repr = Sym_Traversable repr
56 type instance Error_of_Expr ast (Expr_Traversable root) = No_Error_Expr
57
58 traverse_from
59 :: forall root ty ast hs ret.
60 ( ty ~ Type_Root_of_Expr (Expr_Traversable root)
61 , Type0_Eq ty
62 , Type1_Eq ty
63 , Expr_From ast root
64 , Type0_Lift Type_Fun (Type_of_Expr root)
65 , Type0_Unlift Type_Fun (Type_of_Expr root)
66 , Type1_Unlift (Type_of_Expr root)
67 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
68 (Error_of_Expr ast root)
69 , Root_of_Expr root ~ root
70 , Type1_Constraint Applicative ty
71 , Type1_Constraint Traversable ty
72 ) => ast -> ast
73 -> ExprFrom ast (Expr_Traversable root) hs ret
74 traverse_from ast_g ast_ta ex ast ctx k =
75 -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
76 expr_from (Proxy::Proxy root) ast_g ctx $
77 \(ty_g::ty h_g) (Forall_Repr_with_Context g) ->
78 expr_from (Proxy::Proxy root) ast_ta ctx $
79 \ty_ta (Forall_Repr_with_Context ta) ->
80
81 check_type_fun ex ast ty_g $ \(Type2 Proxy ty_g_a ty_g_fb) ->
82
83 check_type1 ex ast ty_g_fb $ \(Type1 f ty_g_fb_b, Type1_Lift ty_f) ->
84 check_type1 ex ast ty_ta $ \(Type1 t ty_ta_a, Type1_Lift ty_t) ->
85
86 check_type1_constraint ex (Proxy::Proxy Applicative) ast ty_g_fb $ \Dict ->
87 check_type1_constraint ex (Proxy::Proxy Traversable) ast ty_ta $ \Dict ->
88
89 check_type0_eq ex ast ty_g_a ty_ta_a $ \Refl ->
90
91 k (
92 Type_Root $ ty_f $ Type1 f $
93 Type_Root $ ty_t $ Type1 t ty_g_fb_b
94 ) $ Forall_Repr_with_Context $
95 \c -> traverse (g c) (ta c)