]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Monoid.hs
Add Typing.Family and Compiling.MonoFunctor.
[haskell/symantic.git] / 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 as ->
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 as ty_x $ TermLC $ Fun.const mempty
95 mappend_from =
96 -- mappend :: Monoid a => a -> a -> a
97 from_ast1 ast $ \ast_x as ->
98 term_from ast_x ctx $ \ty_x (TermLC x) ->
99 check_constraint (At (Just ast_x) (tyMonoid :$ ty_x)) $ \Con ->
100 k as (ty_x ~> ty_x) $ TermLC $
101 \c -> lam $ \y -> mappend (x c) y
102
103 -- | The 'Monoid' 'Type'
104 tyMonoid :: Inj_Const cs Monoid => Type cs Monoid
105 tyMonoid = TyConst inj_const
106
107 sym_Monoid :: Proxy Sym_Monoid
108 sym_Monoid = Proxy
109
110 syMonoid :: IsString a => [Syntax a] -> Syntax a
111 syMonoid = Syntax "Monoid"