git.iko.soy/Idris-dev
on 13ebfcf help sign in
Idris-dev/src/Idris/DeepSeq.hs
362 lines 14 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where
5import Idris.Core.DeepSeq
6import Idris.Docstrings
7import Idris.Core.TT
8import Idris.AbsSyntaxTree
10import Control.DeepSeq
12import qualified Cheapskate.Types as CT
13import qualified Idris.Docstrings as D
15instance NFData a => NFData (D.Docstring a) where
16 rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()
18instance NFData CT.Options where
19 rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
21instance NFData a => NFData (D.Block a) where
22 rnf (D.Para lines) = rnf lines `seq` ()
23 rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()
24 rnf (D.Blockquote bs) = rnf bs `seq` ()
25 rnf (D.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()
26 rnf (D.CodeBlock attr txt tm) = rnf attr `seq` rnf txt `seq` ()
27 rnf (D.HtmlBlock txt) = rnf txt `seq` ()
28 rnf D.HRule = ()
30instance NFData a => NFData (D.Inline a) where
31 rnf (D.Str txt) = rnf txt `seq` ()
32 rnf D.Space = ()
33 rnf D.SoftBreak = ()
34 rnf D.LineBreak = ()
35 rnf (D.Emph xs) = rnf xs `seq` ()
36 rnf (D.Strong xs) = rnf xs `seq` ()
37 rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()
38 rnf (D.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()
39 rnf (D.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()
40 rnf (D.Entity a) = rnf a `seq` ()
41 rnf (D.RawHtml x) = rnf x `seq` ()
43instance NFData CT.ListType where
44 rnf (CT.Bullet c) = rnf c `seq` ()
45 rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
47instance NFData CT.CodeAttr where
48 rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
50instance NFData CT.NumWrapper where
51 rnf CT.PeriodFollowing = ()
52 rnf CT.ParenFollowing = ()
54instance NFData DocTerm where
55 rnf Unchecked = ()
56 rnf (Checked x1) = rnf x1 `seq` ()
57 rnf (Example x1) = rnf x1 `seq` ()
58 rnf (Failing x1) = rnf x1 `seq` ()
60-- All generated by 'derive'
62instance NFData SizeChange where
63 rnf Smaller = ()
64 rnf Same = ()
65 rnf Bigger = ()
66 rnf Unknown = ()
68instance NFData FnInfo where
69 rnf (FnInfo x1) = rnf x1 `seq` ()
71instance NFData Codegen where
72 rnf (Via x1) = rnf x1 `seq` ()
73 rnf Bytecode = ()
75instance NFData CGInfo where
76 rnf (CGInfo x1 x2 x3 x4 x5)
77 = rnf x1 `seq`
78 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
80instance NFData Fixity where
81 rnf (Infixl x1) = rnf x1 `seq` ()
82 rnf (Infixr x1) = rnf x1 `seq` ()
83 rnf (InfixN x1) = rnf x1 `seq` ()
84 rnf (PrefixN x1) = rnf x1 `seq` ()
86instance NFData FixDecl where
87 rnf (Fix x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
89instance NFData Static where
90 rnf Static = ()
91 rnf Dynamic = ()
93instance NFData ArgOpt where
94 rnf _ = ()
96instance NFData Plicity where
97 rnf (Imp x1 x2 x3 x4)
98 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
99 rnf (Exp x1 x2 x3)
100 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
101 rnf (Constraint x1 x2)
102 = rnf x1 `seq` rnf x2 `seq` ()
103 rnf (TacImp x1 x2 x3)
104 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
106instance NFData FnOpt where
107 rnf Inlinable = ()
108 rnf TotalFn = ()
109 rnf PartialFn = ()
110 rnf CoveringFn = ()
111 rnf Coinductive = ()
112 rnf AssertTotal = ()
113 rnf Dictionary = ()
114 rnf Implicit = ()
115 rnf NoImplicit = ()
116 rnf (CExport x1) = rnf x1 `seq` ()
117 rnf ErrorHandler = ()
118 rnf ErrorReverse = ()
119 rnf Reflection = ()
120 rnf (Specialise x1) = rnf x1 `seq` ()
121 rnf Constructor = ()
123instance NFData DataOpt where
124 rnf Codata = ()
125 rnf DefaultEliminator = ()
126 rnf DefaultCaseFun = ()
127 rnf DataErrRev = ()
129instance (NFData t) => NFData (PDecl' t) where
130 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
131 rnf (PTy x1 x2 x3 x4 x5 x6 x7)
132 = rnf x1 `seq`
133 rnf x2 `seq`
134 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
135 rnf (PPostulate x1 x2 x3 x4 x5 x6)
136 = rnf x1 `seq`
137 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
138 rnf (PClauses x1 x2 x3 x4)
139 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
140 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
141 rnf (PData x1 x2 x3 x4 x5 x6)
142 = rnf x1 `seq`
143 rnf x2 `seq`
144 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
145 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
146 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
147 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)
148 = rnf x1 `seq`
149 rnf x2 `seq`
150 rnf x3 `seq`
151 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()
152 rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)
153 = rnf x1 `seq`
154 rnf x2 `seq`
155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()
156 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
157 = rnf x1 `seq`
158 rnf x2 `seq`
159 rnf x3 `seq`
160 rnf x4 `seq`
161 rnf x5 `seq`
162 rnf x6 `seq`
163 rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
164 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
167 rnf (PDirective x1) = ()
168 rnf (PProvider x1 x2 x3 x4 x5)
169 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
170 rnf (PTransform x1 x2 x3 x4)
171 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
173instance NFData t => NFData (ProvideWhat' t) where
174 rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()
175 rnf (ProvPostulate tm) = rnf tm `seq` ()
177instance NFData PunInfo where
178 rnf x = x `seq` ()
180instance (NFData t) => NFData (PClause' t) where
181 rnf (PClause x1 x2 x3 x4 x5 x6)
182 = rnf x1 `seq`
183 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
184 rnf (PWith x1 x2 x3 x4 x5 x6 x7)
185 = rnf x1 `seq`
186 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
187 rnf (PClauseR x1 x2 x3 x4)
188 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
189 rnf (PWithR x1 x2 x3 x4 x5)
190 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
192instance (NFData t) => NFData (PData' t) where
193 rnf (PDatadecl x1 x2 x3)
194 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
195 rnf (PLaterdecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
197instance NFData PTerm where
198 rnf (PQuote x1) = rnf x1 `seq` ()
199 rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
200 rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
201 rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
202 rnf (PLam _ x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
203 rnf (PPi x1 x2 x3 x4)
204 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
205 rnf (PLet _ x1 x2 x3 x4)
206 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
207 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
208 rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
209 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
210 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
211 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
212 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
213 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
214 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
215 rnf (PResolveTC x1) = rnf x1 `seq` ()
216 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
217 rnf (PRewrite x1 x2 x3 x4)
218 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
219 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
220 rnf (PDPair x1 x2 x3 x4 x5)
221 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
222 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
223 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
224 rnf (PHidden x1) = rnf x1 `seq` ()
225 rnf PType = ()
226 rnf (PUniverse _) = ()
227 rnf (PGoal x1 x2 x3 x4)
228 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
229 rnf (PConstant x1) = x1 `seq` ()
230 rnf Placeholder = ()
231 rnf (PDoBlock x1) = rnf x1 `seq` ()
232 rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
233 rnf (PReturn x1) = rnf x1 `seq` ()
234 rnf (PMetavar x1) = rnf x1 `seq` ()
235 rnf (PProof x1) = rnf x1 `seq` ()
236 rnf (PTactics x1) = rnf x1 `seq` ()
237 rnf (PElabError x1) = rnf x1 `seq` ()
238 rnf PImpossible = ()
239 rnf (PCoerced x1) = rnf x1 `seq` ()
240 rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
241 rnf (PUnifyLog x1) = rnf x1 `seq` ()
242 rnf (PNoImplicits x1) = rnf x1 `seq` ()
243 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
244 rnf (PUnquote x1) = rnf x1 `seq` ()
245 rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
247instance (NFData t) => NFData (PTactic' t) where
248 rnf (Intro x1) = rnf x1 `seq` ()
249 rnf Intros = ()
250 rnf (Focus x1) = rnf x1 `seq` ()
251 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
252 rnf (Rewrite x1) = rnf x1 `seq` ()
253 rnf DoUnify = ()
254 rnf (Induction x1) = rnf x1 `seq` ()
255 rnf (CaseTac x1) = rnf x1 `seq` ()
256 rnf (Equiv x1) = rnf x1 `seq` ()
257 rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
258 rnf (MatchRefine x1) = rnf x1 `seq` ()
259 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
260 rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
261 rnf (Exact x1) = rnf x1 `seq` ()
262 rnf Compute = ()
263 rnf Trivial = ()
264 rnf TCInstance = ()
265 rnf (ProofSearch r r1 r2 x1 x2)
266 = rnf x1 `seq` rnf x2 `seq` ()
267 rnf Solve = ()
268 rnf Attack = ()
269 rnf ProofState = ()
270 rnf ProofTerm = ()
271 rnf Undo = ()
272 rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
273 rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
274 rnf (ApplyTactic x1) = rnf x1 `seq` ()
275 rnf (ByReflection x1) = rnf x1 `seq` ()
276 rnf (Reflect x1) = rnf x1 `seq` ()
277 rnf (Fill x1) = rnf x1 `seq` ()
278 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
279 rnf Qed = ()
280 rnf Abandon = ()
281 rnf (TCheck x1) = rnf x1 `seq` ()
282 rnf (TEval x1) = rnf x1 `seq` ()
283 rnf (TDocStr x1) = x1 `seq` ()
284 rnf (TSearch x1) = rnf x1 `seq` ()
285 rnf Skip = ()
286 rnf (TFail x1) = rnf x1 `seq` ()
287 rnf SourceFC = ()
288 rnf Unfocus = ()
290instance NFData ErrorReportPart where
291 rnf (TermPart x1) = rnf x1 `seq` ()
292 rnf (TextPart x1) = rnf x1 `seq` ()
293 rnf (NamePart x1) = rnf x1 `seq` ()
294 rnf (SubReport x1) = rnf x1 `seq` ()
296instance (NFData t) => NFData (PDo' t) where
297 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
298 rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
299 rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
300 rnf (DoLet x1 x2 x3 x4)
301 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
302 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
304instance (NFData t) => NFData (PArg' t) where
305 rnf (PImp x1 x2 x3 x4 x5)
306 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
307 rnf (PExp x1 x2 x3 x4)
308 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
309 rnf (PConstraint x1 x2 x3 x4)
310 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
311 rnf (PTacImplicit x1 x2 x3 x4 x5)
312 = rnf x1 `seq`
313 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
315instance NFData ClassInfo where
316 rnf (CI x1 x2 x3 x4 x5 x6)
317 = rnf x1 `seq`
318 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
320instance NFData OptInfo where
321 rnf (Optimise x1 x2)
322 = rnf x1 `seq` rnf x2 `seq` ()
324instance NFData TypeInfo where
325 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
327instance (NFData t) => NFData (DSL' t) where
328 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
329 = rnf x1 `seq`
330 rnf x2 `seq`
331 rnf x3 `seq`
332 rnf x4 `seq`
333 rnf x5 `seq`
334 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
336instance NFData SynContext where
337 rnf PatternSyntax = ()
338 rnf TermSyntax = ()
339 rnf AnySyntax = ()
341instance NFData Syntax where
342 rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
344instance NFData SSymbol where
345 rnf (Keyword x1) = rnf x1 `seq` ()
346 rnf (Symbol x1) = rnf x1 `seq` ()
347 rnf (Binding x1) = rnf x1 `seq` ()
348 rnf (Expr x1) = rnf x1 `seq` ()
349 rnf (SimpleExpr x1) = rnf x1 `seq` ()
351instance NFData Using where
352 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
353 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
355instance NFData SyntaxInfo where
356 rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
357 = rnf x1 `seq`
358 rnf x2 `seq`
359 rnf x3 `seq`
360 rnf x4 `seq`
361 rnf x5 `seq`
362 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()