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