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