]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/NonNull.hs
Integrate types to the module system.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / NonNull.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'NonNull'.
4 module Language.Symantic.Lib.NonNull where
5
6 import Data.MonoTraversable (MonoFoldable)
7 import Data.NonNull (NonNull)
8 import Data.Sequences (IsSequence, SemiSequence)
9 import Prelude hiding (head, init, last, tail)
10 import qualified Data.MonoTraversable as MT
11 import qualified Data.NonNull as NonNull
12
13 import Language.Symantic
14 import Language.Symantic.Lib.Bool (tyBool)
15 import Language.Symantic.Lib.Maybe (tyMaybe)
16 import Language.Symantic.Lib.MonoFoldable (tyMonoFoldable)
17 import Language.Symantic.Lib.MonoFunctor (Element, famElement, o0, e1)
18 import Language.Symantic.Lib.Sequences (tySemiSequence, tyIsSequence, s0)
19 import Language.Symantic.Lib.Tuple2 (tyTuple2)
20
21 -- * Class 'Sym_NonNull'
22 type instance Sym NonNull = Sym_NonNull
23 class Sym_NonNull term where
24 fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
25 toNullable :: MonoFoldable o => term (NonNull o) -> term o
26 ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
27 nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
28 head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
29 last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
30 tail :: IsSequence s => term (NonNull s) -> term s
31 init :: IsSequence s => term (NonNull s) -> term s
32 nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
33 default fromNullable :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term o -> term (Maybe (NonNull o))
34 default toNullable :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term o
35 default ncons :: Sym_NonNull (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
36 default nuncons :: Sym_NonNull (UnT term) => Trans term => IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
37 default head :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
38 default last :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
39 default tail :: Sym_NonNull (UnT term) => Trans term => IsSequence s => term (NonNull s) -> term s
40 default init :: Sym_NonNull (UnT term) => Trans term => IsSequence s => term (NonNull s) -> term s
41 default nfilter :: Sym_NonNull (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
42 fromNullable = trans1 fromNullable
43 toNullable = trans1 toNullable
44 ncons = trans2 ncons
45 nuncons = trans1 nuncons
46 head = trans1 head
47 last = trans1 last
48 tail = trans1 tail
49 init = trans1 init
50 nfilter = trans2 nfilter
51
52 -- Interpreting
53 instance Sym_NonNull Eval where
54 fromNullable = eval1 NonNull.fromNullable
55 toNullable = eval1 NonNull.toNullable
56 ncons = eval2 NonNull.ncons
57 nuncons = eval1 NonNull.nuncons
58 head = eval1 NonNull.head
59 last = eval1 NonNull.last
60 tail = eval1 NonNull.tail
61 init = eval1 NonNull.init
62 nfilter = eval2 NonNull.nfilter
63 instance Sym_NonNull View where
64 fromNullable = view1 "fromNullable"
65 toNullable = view1 "toNullable"
66 ncons = view2 "ncons"
67 nuncons = view1 "nuncons"
68 head = view1 "head"
69 last = view1 "last"
70 tail = view1 "tail"
71 init = view1 "init"
72 nfilter = view2 "nfilter"
73 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (Dup r1 r2) where
74 fromNullable = dup1 @Sym_NonNull fromNullable
75 toNullable = dup1 @Sym_NonNull toNullable
76 ncons = dup2 @Sym_NonNull ncons
77 nuncons = dup1 @Sym_NonNull nuncons
78 head = dup1 @Sym_NonNull head
79 last = dup1 @Sym_NonNull last
80 tail = dup1 @Sym_NonNull tail
81 init = dup1 @Sym_NonNull init
82 nfilter = dup2 @Sym_NonNull nfilter
83
84 -- Transforming
85 instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
86
87 -- Typing
88 instance NameTyOf NonNull where
89 nameTyOf _c = ["NonNull"] `Mod` "NonNull"
90 instance FixityOf NonNull
91 instance TypeInstancesFor NonNull where
92 expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
93 | Just HRefl <- proj_ConstKi @_ @Element f
94 , Just HRefl <- proj_ConstKiTy @_ @NonNull z
95 = expandFamFor c len f (o `TypesS` TypesZ)
96 expandFamFor _c _len _fam _as = Nothing
97 instance ClassInstancesFor NonNull where
98 proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
99 | Just HRefl <- proj_ConstKiTy @_ @NonNull c
100 = case () of
101 _ | Just Refl <- proj_Const @Eq q
102 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
103 | Just Refl <- proj_Const @MT.MonoFoldable q
104 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
105 | Just Refl <- proj_Const @MT.MonoFunctor q
106 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
107 | Just Refl <- proj_Const @Ord q
108 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
109 | Just Refl <- proj_Const @SemiSequence q
110 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
111 | Just Refl <- proj_Const @Show q
112 , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
113 _ -> Nothing
114 proveConstraintFor _c _q = Nothing
115
116 -- Compiling
117 instance Gram_Term_AtomsFor src ss g NonNull
118 instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
119 moduleFor = ["NonNull"] `moduleWhere`
120 [ "fromNullable" := teNonNull_fromNullable
121 , "toNullable" := teNonNull_toNullable
122 , "ncons" := teNonNull_ncons
123 , "nuncons" := teNonNull_nuncons
124 , "head" := teNonNull_head
125 , "last" := teNonNull_last
126 , "tail" := teNonNull_tail
127 , "init" := teNonNull_init
128 , "nfilter" := teNonNull_nfilter
129 ]
130
131 -- ** 'Type's
132 tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)
133 tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a
134
135 -- ** 'Term's
136 teNonNull_fromNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (o -> Maybe (NonNull o)))
137 teNonNull_fromNullable = Term (tyMonoFoldable o0) (o0 ~> tyMaybe (tyNonNull o0)) $ teSym @NonNull $ lam1 fromNullable
138
139 teNonNull_toNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (NonNull o -> o))
140 teNonNull_toNullable = Term (tyMonoFoldable o0) (tyNonNull o0 ~> o0) $ teSym @NonNull $ lam1 toNullable
141
142 teNonNull_ncons :: TermDef NonNull '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> NonNull s))
143 teNonNull_ncons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> tyNonNull s0) $ teSym @NonNull $ lam2 ncons
144
145 teNonNull_nuncons :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> (NonNull s -> (e, Maybe (NonNull s))))
146 teNonNull_nuncons = Term (tyIsSequence s0 # e1 #~ famElement s0) (tyNonNull s0 ~> e1 `tyTuple2` tyMaybe (tyNonNull s0)) $ teSym @NonNull $ lam1 nuncons
147
148 teNonNull_nfilter :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> NonNull s -> s))
149 teNonNull_nfilter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> tyNonNull s0 ~> s0) $ teSym @NonNull $ lam2 nfilter
150
151 teNonNull_head, teNonNull_last :: TermDef NonNull '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (NonNull o -> e))
152 teNonNull_head = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
153 teNonNull_last = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
154
155 teNonNull_tail, teNonNull_init :: TermDef NonNull '[Proxy s] (IsSequence s #> (NonNull s -> s))
156 teNonNull_tail = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 tail
157 teNonNull_init = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 init