]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Maybe.hs
Add Parsing.Grammar.
[haskell/symantic.git] / Language / Symantic / Compiling / 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.Compiling.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.Text (Text)
12 import Data.Type.Equality ((:~:)(Refl))
13 import Prelude hiding (maybe)
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling.Term
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming.Trans
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 Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
37 type instance Consts_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 (Proxy @Sym_Maybe) _Nothing
58 _Just = dupI1 (Proxy @Sym_Maybe) _Just
59 maybe = dupI3 (Proxy @Sym_Maybe) maybe
60
61 instance
62 ( Read_TypeNameR Text cs rs
63 , Inj_Const cs Maybe
64 ) => Read_TypeNameR Text cs (Proxy Maybe ': rs) where
65 read_typenameR _cs "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
70
71 instance -- Proj_ConC
72 ( Proj_Const cs Maybe
73 , Proj_Consts cs (Consts_imported_by Maybe)
74 , Proj_Con cs
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::Proxy Maybe)
79 = case () of
80 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
81 | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con
82 | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
83 | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con
84 | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
85 _ -> Nothing
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::Proxy Maybe)
89 = case () of
90 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
91 , Just Con <- proj_con (t :$ a) -> Just Con
92 | Just Refl <- proj_const q (Proxy::Proxy Monoid)
93 , Just Con <- proj_con (t :$ a) -> Just Con
94 | Just Refl <- proj_const q (Proxy::Proxy Show)
95 , Just Con <- proj_con (t :$ a) -> Just Con
96 _ -> Nothing
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))
104 instance -- CompileI
105 ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
106 , Inj_Const (Consts_of_Ifaces is) Maybe
107 , Inj_Const (Consts_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 (Consts_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_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
130 check_type
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)