Language/Symantic/Compiling/Monoid.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 'Monoid'.
  14 module Language.Symantic.Compiling.Monoid where
  15
  16 import Control.Monad
  17 import qualified Data.Function as Fun
  18 import Data.Monoid (Monoid)
  19 import qualified Data.Monoid as Monoid
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (Monoid(..))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Interpreting
  29 import Language.Symantic.Transforming.Trans
  30
  31 -- * Class 'Sym_Monoid'
  32 class Sym_Monoid term where
  33         mempty  :: Monoid a => term a
  34         mappend :: Monoid a => term a -> term a -> term a
  35         default mempty  :: (Trans t term, Monoid a) => t term a
  36         default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
  37         mempty  = trans_lift mempty
  38         mappend = trans_map2 mappend
  39
  40 type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
  41 type instance Consts_of_Iface (Proxy Monoid) = Proxy Monoid ': Consts_imported_by Monoid
  42 type instance Consts_imported_by Monoid = '[]
  43
  44 instance Sym_Monoid HostI where
  45         mempty  = HostI Monoid.mempty
  46         mappend = liftM2 Monoid.mappend
  47 instance Sym_Monoid TextI where
  48         mempty  = textI_app0 "mempty"
  49         mappend = textI_app2 "mappend"
  50 instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
  51         mempty  = dupI0 sym_Monoid mempty
  52         mappend = dupI2 sym_Monoid mappend
  53
  54 -- | 'mappend' alias.
  55 (<>) ::
  56  ( Sym_Monoid term
  57  , Monoid a )
  58  => term a -> term a -> term a
  59 (<>) = mappend
  60 infixr 6 <>
  61
  62 instance Const_from Text cs => Const_from Text (Proxy Monoid ': cs) where
  63         const_from "Monoid" k = k (ConstZ kind)
  64         const_from s k = const_from s $ k . ConstS
  65 instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
  66         show_const ConstZ{} = "Monoid"
  67         show_const (ConstS c) = show_const c
  68
  69 instance -- Proj_ConC
  70  Proj_ConC cs (Proxy Monoid)
  71 instance -- Term_fromI
  72  ( AST ast
  73  , Lexem ast ~ LamVarName
  74  , Const_from (Lexem ast) (Consts_of_Ifaces is)
  75  , Inj_Const  (Consts_of_Ifaces is) Monoid
  76  , Inj_Const  (Consts_of_Ifaces is) (->)
  77  , Proj_Con   (Consts_of_Ifaces is)
  78  , Term_from is ast
  79  ) => Term_fromI is (Proxy Monoid) ast where
  80         term_fromI ast ctx k =
  81                 case ast_lexem ast of
  82                  "mempty"  -> mempty_from
  83                  "mappend" -> mappend_from
  84                  "<>"      -> mappend_from
  85                  _ -> Left $ Error_Term_unsupported
  86                 where
  87                 mempty_from =
  88                  -- mempty :: Monoid a => a
  89                         from_ast1 ast $ \ast_ty_x ->
  90                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
  91                         type_from ast_ty_x $ \ty_x -> Right $
  92                         check_kind ast SKiType (At (Just ast_ty_x) ty_x) $ \Refl ->
  93                         check_constraint (At (Just ast_ty_x) (tyMonoid :$ ty_x)) $ \Con ->
  94                         k ty_x $ TermLC $
  95                         Fun.const mempty
  96                 mappend_from =
  97                  -- mappend :: Monoid a => a -> a -> a
  98                         case ast_nodes ast of
  99                          [] -> Left $ Error_Term_Syntax $
 100                                 Error_Syntax_more_arguments_needed $ At (Just ast) 1
 101                          [ast_x] ->
 102                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 103                                 check_constraint (At (Just ast_x) (tyMonoid :$ ty_x)) $ \Con ->
 104                                 k (ty_x ~> ty_x) $ TermLC $
 105                                  \c -> lam $ \y -> mappend (x c) y
 106                          [ast_x, ast_y] ->
 107                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 108                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 109                                 check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
 110                                 check_constraint (At (Just ast_x) (tyMonoid :$ ty_x)) $ \Con ->
 111                                 k ty_x $ TermLC $
 112                                  \c -> mappend (x c) (y c)
 113                          _ -> Left $ Error_Term_Syntax $
 114                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 115
 116 -- | The 'Monoid' 'Type'
 117 tyMonoid :: Inj_Const cs Monoid => Type cs Monoid
 118 tyMonoid = TyConst inj_const
 119
 120 sym_Monoid :: Proxy Sym_Monoid
 121 sym_Monoid = Proxy
 122
 123 syMonoid :: IsString a => [Syntax a] -> Syntax a
 124 syMonoid = Syntax "Monoid"