]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/MonoFunctor.hs
Type1_From instances
[haskell/symantic.git] / Language / Symantic / Expr / MonoFunctor.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE MultiParamTypeClasses #-}
7 {-# LANGUAGE OverloadedStrings #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# OPTIONS_GHC -fno-warn-orphans #-}
13 -- | Expression for 'MonoFunctor'.
14 module Language.Symantic.Expr.MonoFunctor where
15
16 import Control.Monad (liftM2)
17 import Data.Proxy (Proxy(..))
18 import Data.Type.Equality ((:~:)(Refl))
19 import Prelude hiding (fmap)
20 -- import qualified Data.Function as Fun
21 import qualified Data.MonoTraversable as MT
22 import Data.MonoTraversable (MonoFunctor)
23
24 import Language.Symantic.Type
25 import Language.Symantic.Repr
26 import Language.Symantic.Expr.Root
27 import Language.Symantic.Expr.Error
28 import Language.Symantic.Expr.From
29 import Language.Symantic.Expr.Lambda
30 import Language.Symantic.Trans.Common
31
32 -- * Class 'Sym_MonoFunctor'
33 -- | Symantic.
34 class Sym_Lambda repr => Sym_MonoFunctor repr where
35 omap :: MonoFunctor o => repr (MT.Element o -> MT.Element o) -> repr o -> repr o
36 default omap :: (Trans t repr, MonoFunctor o)
37 => t repr (MT.Element o -> MT.Element o) -> t repr o -> t repr o
38 omap = trans_map2 omap
39 instance Sym_MonoFunctor Repr_Host where
40 omap = liftM2 MT.omap
41 instance Sym_MonoFunctor Repr_Text where
42 omap = repr_text_app2 "omap"
43 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Repr_Dup r1 r2) where
44 omap = repr_dup2 sym_MonoFunctor omap
45
46 sym_MonoFunctor :: Proxy Sym_MonoFunctor
47 sym_MonoFunctor = Proxy
48
49 -- * Type 'Expr_MonoFunctor'
50 -- | Expression.
51 data Expr_MonoFunctor (root:: *)
52 type instance Root_of_Expr (Expr_MonoFunctor root) = root
53 type instance Type_of_Expr (Expr_MonoFunctor root) = No_Type
54 type instance Sym_of_Expr (Expr_MonoFunctor root) repr = Sym_MonoFunctor repr
55 type instance Error_of_Expr ast (Expr_MonoFunctor root) = No_Error_Expr
56
57 -- | Parse 'omap'.
58 omap_from
59 :: forall root ty ast hs ret.
60 ( ty ~ Type_Root_of_Expr (Expr_MonoFunctor root)
61 , Expr_From ast root
62 , Type0_Eq ty
63 , Type0_Lift Type_Fun (Type_of_Expr root)
64 , Type0_Unlift Type_Fun (Type_of_Expr root)
65 , Type0_Constraint MonoFunctor ty
66 , Type0_Family Type_Family_MonoElement ty
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 ) => ast -> ast
71 -> ExprFrom ast (Expr_MonoFunctor root) hs ret
72 omap_from ast_f ast_m ex ast ctx k =
73 -- omap :: (Element mono -> Element mono) -> mono -> mono
74 expr_from (Proxy::Proxy root) ast_f ctx $
75 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
76 expr_from (Proxy::Proxy root) ast_m ctx $
77 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
78 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
79 check_type0_constraint ex (Proxy::Proxy MonoFunctor) ast ty_m $ \Dict ->
80 check_type0_eq ex ast ty_f_a ty_f_b $ \Refl ->
81 check_type0_family (Proxy::Proxy Type_Family_MonoElement) ex ast ty_m $ \ty_m_ele ->
82 check_type0_eq ex ast ty_f_a ty_m_ele $ \Refl ->
83 k ty_m $ Forall_Repr_with_Context $
84 \c -> omap (f c) (m c)