]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Either.hs
Move libraries in Lib.
[haskell/symantic.git] / Language / Symantic / Lib / Either.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
4 -- | Symantic for 'Either'.
5 module Language.Symantic.Lib.Either where
6
7 import Control.Monad (liftM, liftM3)
8 import qualified Data.Either as Either
9 import Data.Proxy
10 import Data.Type.Equality ((:~:)(Refl))
11 import Prelude hiding (either)
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Parsing.Grammar
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling
17 import Language.Symantic.Interpreting
18 import Language.Symantic.Transforming.Trans
19 import Language.Symantic.Lib.Lambda
20
21 -- * Class 'Sym_Tuple'
22 class Sym_Either term where
23 _Left :: term l -> term (Either l r)
24 _Right :: term r -> term (Either l r)
25 either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
26 default _Left :: Trans t term => t term l -> t term (Either l r)
27 default _Right :: Trans t term => t term r -> t term (Either l r)
28 default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
29 _Left = trans_map1 _Left
30 _Right = trans_map1 _Right
31 either = trans_map3 either
32
33 type instance Sym_of_Iface (Proxy Either) = Sym_Either
34 type instance Consts_of_Iface (Proxy Either) = Proxy Either ': Consts_imported_by Either
35 type instance Consts_imported_by Either =
36 [ Proxy (->)
37 , Proxy Applicative
38 , Proxy Eq
39 , Proxy Foldable
40 , Proxy Functor
41 , Proxy Monad
42 , Proxy Ord
43 , Proxy Show
44 , Proxy Traversable
45 ]
46
47 instance Sym_Either HostI where
48 _Right = liftM Right
49 _Left = liftM Left
50 either = liftM3 Either.either
51 instance Sym_Either TextI where
52 _Right = textI1 "Right"
53 _Left = textI1 "Left"
54 either = textI3 "either"
55 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
56 _Left = dupI1 (Proxy @Sym_Either) _Left
57 _Right = dupI1 (Proxy @Sym_Either) _Right
58 either = dupI3 (Proxy @Sym_Either) either
59
60 instance
61 ( Read_TypeNameR Type_Name cs rs
62 , Inj_Const cs Either
63 ) => Read_TypeNameR Type_Name cs (Proxy Either ': rs) where
64 read_typenameR _cs (Type_Name "Either") k = k (ty @Either)
65 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
66 instance Show_Const cs => Show_Const (Proxy Either ': cs) where
67 show_const ConstZ{} = "Either"
68 show_const (ConstS c) = show_const c
69 instance -- Proj_ConC
70 ( Proj_Const cs Either
71 , Proj_Consts cs (Consts_imported_by Either)
72 , Proj_Con cs
73 ) => Proj_ConC cs (Proxy Either) where
74 proj_conC _ (TyConst q :$ (TyConst c :$ _l))
75 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
76 , Just Refl <- proj_const c (Proxy @Either)
77 = case () of
78 _ | Just Refl <- proj_const q (Proxy @Functor) -> Just Con
79 | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
80 | Just Refl <- proj_const q (Proxy @Monad) -> Just Con
81 | Just Refl <- proj_const q (Proxy @Foldable) -> Just Con
82 | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
83 _ -> Nothing
84 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
85 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
86 , Just Refl <- proj_const c (Proxy @Either)
87 = case () of
88 _ | Just Refl <- proj_const q (Proxy @Eq)
89 , Just Con <- proj_con (t :$ l)
90 , Just Con <- proj_con (t :$ r) -> Just Con
91 | Just Refl <- proj_const q (Proxy @Ord)
92 , Just Con <- proj_con (t :$ l)
93 , Just Con <- proj_con (t :$ r) -> Just Con
94 | Just Refl <- proj_const q (Proxy @Show)
95 , Just Con <- proj_con (t :$ l)
96 , Just Con <- proj_con (t :$ r) -> Just Con
97 _ -> Nothing
98 proj_conC _c _q = Nothing
99 data instance TokenT meta (ts::[*]) (Proxy Either)
100 = Token_Term_Either_Left (EToken meta '[Proxy Token_Type]) (EToken meta ts)
101 | Token_Term_Either_Right (EToken meta '[Proxy Token_Type]) (EToken meta ts)
102 | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
103 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
104 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
105 instance -- CompileI
106 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
107 , Inj_Const (Consts_of_Ifaces is) Either
108 , Inj_Const (Consts_of_Ifaces is) (->)
109 -- , Proj_Token is Token_Type
110 , Compile is
111 ) => CompileI is (Proxy Either) where
112 compileI tok ctx k =
113 case tok of
114 Token_Term_Either_Left tok_ty_r tok_l ->
115 -- Left :: l -> Either l r
116 compile_type tok_ty_r $ \(ty_r::Type (Consts_of_Ifaces is) r) ->
117 check_kind
118 (At Nothing SKiType)
119 (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
120 compileO tok_l ctx $ \ty_l (TermO l) ->
121 k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
122 \c -> _Left (l c)
123 Token_Term_Either_Right tok_ty_l tok_r ->
124 -- Right :: r -> Either l r
125 compile_type tok_ty_l $ \(ty_l::Type (Consts_of_Ifaces is) l) ->
126 check_kind
127 (At Nothing SKiType)
128 (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
129 compileO tok_r ctx $ \ty_r (TermO r) ->
130 k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
131 \c -> _Right (r c)
132 Token_Term_Either_either tok_l2a tok_r2a ->
133 -- either :: (l -> a) -> (r -> a) -> Either l r -> a
134 compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
135 compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
136 check_type2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
137 check_type2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
138 check_type (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
139 k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
140 \c -> lam $ either (l2a c) (r2a c)
141 instance -- TokenizeT
142 Inj_Token meta ts Either =>
143 TokenizeT meta ts (Proxy Either) where
144 tokenizeT _t = mempty
145 { tokenizers_infix = tokenizeTMod []
146 [ (Term_Name "Left",) Term_ProTok
147 { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
148 ProTok $ inj_etoken meta $ Token_Term_Either_Left r l
149 , term_fixity = infixN5 }
150 , (Term_Name "Right",) Term_ProTok
151 { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
152 ProTok $ inj_etoken meta $ Token_Term_Either_Right l r
153 , term_fixity = infixN5 }
154 , tokenize2 "either" infixN5 Token_Term_Either_either
155 ]
156 }
157 instance Gram_Term_AtomsT meta ts (Proxy Either) g