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
8 import qualified Data.Function as Fun
9 import qualified Data.Maybe as Maybe
11 import Data.Type.Equality ((:~:)(Refl))
12 import Prelude hiding (maybe)
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
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
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
31 _Nothing = trans_lift _Nothing
32 _Just = trans_map1 _Just
33 maybe = trans_map3 maybe
35 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
36 type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
37 type instance Consts_imported_by Maybe =
48 instance Sym_Maybe HostI where
49 _Nothing = HostI Nothing
51 maybe = liftM3 Maybe.maybe
52 instance Sym_Maybe TextI where
53 _Nothing = textI0 "Nothing"
55 maybe = textI3 "maybe"
56 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
57 _Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
58 _Just = dupI1 (Proxy @Sym_Maybe) _Just
59 maybe = dupI3 (Proxy @Sym_Maybe) maybe
62 ( Read_TypeNameR Type_Name cs rs
64 ) => Read_TypeNameR Type_Name cs (Proxy Maybe ': rs) where
65 read_typenameR _cs (Type_Name "Maybe") k = k (ty @Maybe)
66 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
67 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
68 show_const ConstZ{} = "Maybe"
69 show_const (ConstS c) = show_const c
73 , Proj_Consts cs (Consts_imported_by Maybe)
75 ) => Proj_ConC cs (Proxy Maybe) where
76 proj_conC _ (TyConst q :$ TyConst c)
77 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
78 , Just Refl <- proj_const c (Proxy @Maybe)
80 _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
81 | Just Refl <- proj_const q (Proxy @Foldable) -> Just Con
82 | Just Refl <- proj_const q (Proxy @Functor) -> Just Con
83 | Just Refl <- proj_const q (Proxy @Monad) -> Just Con
84 | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
86 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
87 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
88 , Just Refl <- proj_const c (Proxy @Maybe)
90 _ | Just Refl <- proj_const q (Proxy @Eq)
91 , Just Con <- proj_con (t :$ a) -> Just Con
92 | Just Refl <- proj_const q (Proxy @Monoid)
93 , Just Con <- proj_con (t :$ a) -> Just Con
94 | Just Refl <- proj_const q (Proxy @Show)
95 , Just Con <- proj_con (t :$ a) -> Just Con
97 proj_conC _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))
105 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
106 , Inj_Const (Consts_of_Ifaces is) Maybe
107 , Inj_Const (Consts_of_Ifaces is) (->)
109 ) => CompileI is (Proxy Maybe) where
112 Token_Term_Maybe_Nothing tok_ty_a ->
113 -- Nothing :: Maybe a
114 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
117 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
118 k (ty @Maybe :$ ty_a) $ TermO $
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 $
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_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
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)
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
145 , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
148 instance Gram_Term_AtomsT meta ts (Proxy Maybe) g