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 m => repr (MT.Element m -> MT.Element m) -> repr m -> repr m
  36         default omap :: (Trans t repr, MonoFunctor m)
  37          => t repr (MT.Element m -> MT.Element m) -> t repr m -> t repr m
  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
  44  ( Sym_MonoFunctor r1
  45  , Sym_MonoFunctor r2
  46  ) => Sym_MonoFunctor (Repr_Dup r1 r2) where
  47         omap (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
  48                 omap f1 m1 `Repr_Dup` omap f2 m2
  49
  50 -- * Type 'Expr_MonoFunctor'
  51 -- | Expression.
  52 data Expr_MonoFunctor (root:: *)
  53 type instance Root_of_Expr      (Expr_MonoFunctor root)      = root
  54 type instance Type_of_Expr      (Expr_MonoFunctor root)      = No_Type
  55 type instance Sym_of_Expr       (Expr_MonoFunctor root) repr = (Sym_MonoFunctor repr)
  56 type instance Error_of_Expr ast (Expr_MonoFunctor root)      = No_Error_Expr
  57
  58 -- | Parse 'omap'.
  59 omap_from
  60  :: forall root ty ast hs ret.
  61  ( ty ~ Type_Root_of_Expr (Expr_MonoFunctor root)
  62  , Type0_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  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  67                    (Error_of_Expr ast root)
  68  , Root_of_Expr root ~ root
  69  , Type0_Constraint MonoFunctor ty
  70  , Type0_Family Type_Family_MonoElement ty
  71  ) => ast -> ast
  72  -> ExprFrom ast (Expr_MonoFunctor root) hs ret
  73 omap_from ast_f ast_m ex ast ctx k =
  74  -- NOTE: omap :: (Element mono -> Element mono) -> mono -> mono
  75         expr_from (Proxy::Proxy root) ast_f ctx $
  76          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
  77         expr_from (Proxy::Proxy root) ast_m ctx $
  78          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
  79         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
  80         check_type0_constraint ex (Proxy::Proxy MonoFunctor) ast ty_m $ \Dict ->
  81         check_type0_eq ex ast ty_f_a ty_f_b $ \Refl ->
  82         check_type0_family (Proxy::Proxy Type_Family_MonoElement) ex ast ty_m $ \ty_m_ele ->
  83         check_type0_eq ex ast ty_f_a ty_m_ele $ \Refl ->
  84         k ty_m $ Forall_Repr_with_Context $
  85          \c -> omap (f c) (m c)