]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Either.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / 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.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.Lambda
19
20 -- * Class 'Sym_Tuple'
21 class Sym_Either term where
22 _Left :: term l -> term (Either l r)
23 _Right :: term r -> term (Either l r)
24 either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
25 default _Left :: Trans t term => t term l -> t term (Either l r)
26 default _Right :: Trans t term => t term r -> t term (Either l r)
27 default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
28 _Left = trans_map1 _Left
29 _Right = trans_map1 _Right
30 either = trans_map3 either
31
32 type instance Sym_of_Iface (Proxy Either) = Sym_Either
33 type instance TyConsts_of_Iface (Proxy Either) = Proxy Either ': TyConsts_imported_by Either
34 type instance TyConsts_imported_by Either =
35 [ Proxy (->)
36 , Proxy Applicative
37 , Proxy Eq
38 , Proxy Foldable
39 , Proxy Functor
40 , Proxy Monad
41 , Proxy Ord
42 , Proxy Show
43 , Proxy Traversable
44 ]
45
46 instance Sym_Either HostI where
47 _Right = liftM Right
48 _Left = liftM Left
49 either = liftM3 Either.either
50 instance Sym_Either TextI where
51 _Right = textI1 "Right"
52 _Left = textI1 "Left"
53 either = textI3 "either"
54 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
55 _Left = dupI1 @Sym_Either _Left
56 _Right = dupI1 @Sym_Either _Right
57 either = dupI3 @Sym_Either either
58
59 instance
60 ( Read_TyNameR TyName cs rs
61 , Inj_TyConst cs Either
62 ) => Read_TyNameR TyName cs (Proxy Either ': rs) where
63 read_TyNameR _cs (TyName "Either") k = k (ty @Either)
64 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
65 instance Show_TyConst cs => Show_TyConst (Proxy Either ': cs) where
66 show_TyConst TyConstZ{} = "Either"
67 show_TyConst (TyConstS c) = show_TyConst c
68 instance -- Proj_TyConC
69 ( Proj_TyConst cs Either
70 , Proj_TyConsts cs (TyConsts_imported_by Either)
71 , Proj_TyCon cs
72 ) => Proj_TyConC cs (Proxy Either) where
73 proj_TyConC _ (TyConst q :$ (TyConst c :$ _l))
74 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
75 , Just Refl <- proj_TyConst c (Proxy @Either)
76 = case () of
77 _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
78 | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
79 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
80 | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
81 | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
82 _ -> Nothing
83 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
84 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
85 , Just Refl <- proj_TyConst c (Proxy @Either)
86 = case () of
87 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
88 , Just TyCon <- proj_TyCon (t :$ l)
89 , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
90 | Just Refl <- proj_TyConst q (Proxy @Ord)
91 , Just TyCon <- proj_TyCon (t :$ l)
92 , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
93 | Just Refl <- proj_TyConst q (Proxy @Show)
94 , Just TyCon <- proj_TyCon (t :$ l)
95 , Just TyCon <- proj_TyCon (t :$ r) -> Just TyCon
96 _ -> Nothing
97 proj_TyConC _c _q = Nothing
98 data instance TokenT meta (ts::[*]) (Proxy Either)
99 = Token_Term_Either_Left (EToken meta '[Proxy Token_Type]) (EToken meta ts)
100 | Token_Term_Either_Right (EToken meta '[Proxy Token_Type]) (EToken meta ts)
101 | Token_Term_Either_either (EToken meta ts) (EToken meta ts)
102 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
103 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
104 instance -- CompileI
105 ( Read_TyName TyName (TyConsts_of_Ifaces is)
106 , Inj_TyConst (TyConsts_of_Ifaces is) Either
107 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
108 -- , Proj_Token is Token_Type
109 , Compile is
110 ) => CompileI is (Proxy Either) where
111 compileI tok ctx k =
112 case tok of
113 Token_Term_Either_Left tok_ty_r tok_l ->
114 -- Left :: l -> Either l r
115 compile_Type tok_ty_r $ \(ty_r::Type (TyConsts_of_Ifaces is) r) ->
116 check_Kind
117 (At Nothing SKiType)
118 (At (Just tok_ty_r) $ kind_of ty_r) $ \Refl ->
119 compileO tok_l ctx $ \ty_l (TermO l) ->
120 k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
121 \c -> _Left (l c)
122 Token_Term_Either_Right tok_ty_l tok_r ->
123 -- Right :: r -> Either l r
124 compile_Type tok_ty_l $ \(ty_l::Type (TyConsts_of_Ifaces is) l) ->
125 check_Kind
126 (At Nothing SKiType)
127 (At (Just tok_ty_l) $ kind_of ty_l) $ \Refl ->
128 compileO tok_r ctx $ \ty_r (TermO r) ->
129 k ((ty @Either :$ ty_l) :$ ty_r) $ TermO $
130 \c -> _Right (r c)
131 Token_Term_Either_either tok_l2a tok_r2a ->
132 -- either :: (l -> a) -> (r -> a) -> Either l r -> a
133 compileO tok_l2a ctx $ \ty_l2a (TermO l2a) ->
134 compileO tok_r2a ctx $ \ty_r2a (TermO r2a) ->
135 check_TyEq2 (ty @(->)) (At (Just tok_l2a) ty_l2a) $ \Refl ty_l2a_l ty_l2a_a ->
136 check_TyEq2 (ty @(->)) (At (Just tok_r2a) ty_r2a) $ \Refl ty_r2a_r ty_r2a_a ->
137 check_TyEq (At (Just tok_l2a) ty_l2a_a) (At (Just tok_r2a) ty_r2a_a) $ \Refl ->
138 k ((ty @Either :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermO $
139 \c -> lam $ either (l2a c) (r2a c)
140 instance -- TokenizeT
141 Inj_Token meta ts Either =>
142 TokenizeT meta ts (Proxy Either) where
143 tokenizeT _t = mempty
144 { tokenizers_infix = tokenizeTMod []
145 [ (Term_Name "Left",) Term_ProTok
146 { term_protok = \meta -> ProTokLam $ \l -> ProTokPi $ \r ->
147 ProTok $ inj_EToken meta $ Token_Term_Either_Left r l
148 , term_fixity = infixN5 }
149 , (Term_Name "Right",) Term_ProTok
150 { term_protok = \meta -> ProTokPi $ \l -> ProTokLam $ \r ->
151 ProTok $ inj_EToken meta $ Token_Term_Either_Right l r
152 , term_fixity = infixN5 }
153 , tokenize2 "either" infixN5 Token_Term_Either_either
154 ]
155 }
156 instance Gram_Term_AtomsT meta ts (Proxy Either) g