git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/DeepSeq.hs
363 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 = ()
122 rnf AutoHint = ()
124instance NFData DataOpt where
125 rnf Codata = ()
126 rnf DefaultEliminator = ()
127 rnf DefaultCaseFun = ()
128 rnf DataErrRev = ()
130instance (NFData t) => NFData (PDecl' t) where
131 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
132 rnf (PTy x1 x2 x3 x4 x5 x6 x7)
133 = rnf x1 `seq`
134 rnf x2 `seq`
135 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
136 rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)
137 = rnf x1 `seq`
138 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
139 rnf (PClauses x1 x2 x3 x4)
140 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
141 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
142 rnf (PData x1 x2 x3 x4 x5 x6)
143 = rnf x1 `seq`
144 rnf x2 `seq`
145 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
146 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
147 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
148 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)
149 = rnf x1 `seq`
150 rnf x2 `seq`
151 rnf x3 `seq`
152 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()
153 rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)
154 = rnf x1 `seq`
155 rnf x2 `seq`
156 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()
157 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
158 = rnf x1 `seq`
159 rnf x2 `seq`
160 rnf x3 `seq`
161 rnf x4 `seq`
162 rnf x5 `seq`
163 rnf x6 `seq`
164 rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
165 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
166 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
167 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
168 rnf (PDirective x1) = ()
169 rnf (PProvider x1 x2 x3 x4 x5)
170 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
171 rnf (PTransform x1 x2 x3 x4)
172 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
174instance NFData t => NFData (ProvideWhat' t) where
175 rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()
176 rnf (ProvPostulate tm) = rnf tm `seq` ()
178instance NFData PunInfo where
179 rnf x = x `seq` ()
181instance (NFData t) => NFData (PClause' t) where
182 rnf (PClause x1 x2 x3 x4 x5 x6)
183 = rnf x1 `seq`
184 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
185 rnf (PWith x1 x2 x3 x4 x5 x6 x7)
186 = rnf x1 `seq`
187 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
188 rnf (PClauseR x1 x2 x3 x4)
189 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
190 rnf (PWithR x1 x2 x3 x4 x5)
191 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
193instance (NFData t) => NFData (PData' t) where
194 rnf (PDatadecl x1 x2 x3)
195 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
196 rnf (PLaterdecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
198instance NFData PTerm where
199 rnf (PQuote x1) = rnf x1 `seq` ()
200 rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
201 rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
202 rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
203 rnf (PLam _ x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
204 rnf (PPi x1 x2 x3 x4)
205 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
206 rnf (PLet _ x1 x2 x3 x4)
207 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
208 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
209 rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
210 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
211 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
212 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
213 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
214 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
215 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
216 rnf (PResolveTC x1) = rnf x1 `seq` ()
217 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
218 rnf (PRewrite x1 x2 x3 x4)
219 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
220 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
221 rnf (PDPair x1 x2 x3 x4 x5)
222 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
223 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
224 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
225 rnf (PHidden x1) = rnf x1 `seq` ()
226 rnf PType = ()
227 rnf (PUniverse _) = ()
228 rnf (PGoal x1 x2 x3 x4)
229 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
230 rnf (PConstant x1) = x1 `seq` ()
231 rnf Placeholder = ()
232 rnf (PDoBlock x1) = rnf x1 `seq` ()
233 rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
234 rnf (PReturn x1) = rnf x1 `seq` ()
235 rnf (PMetavar x1) = rnf x1 `seq` ()
236 rnf (PProof x1) = rnf x1 `seq` ()
237 rnf (PTactics x1) = rnf x1 `seq` ()
238 rnf (PElabError x1) = rnf x1 `seq` ()
239 rnf PImpossible = ()
240 rnf (PCoerced x1) = rnf x1 `seq` ()
241 rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
242 rnf (PUnifyLog x1) = rnf x1 `seq` ()
243 rnf (PNoImplicits x1) = rnf x1 `seq` ()
244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
245 rnf (PUnquote x1) = rnf x1 `seq` ()
246 rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
248instance (NFData t) => NFData (PTactic' t) where
249 rnf (Intro x1) = rnf x1 `seq` ()
250 rnf Intros = ()
251 rnf (Focus x1) = rnf x1 `seq` ()
252 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
253 rnf (Rewrite x1) = rnf x1 `seq` ()
254 rnf DoUnify = ()
255 rnf (Induction x1) = rnf x1 `seq` ()
256 rnf (CaseTac x1) = rnf x1 `seq` ()
257 rnf (Equiv x1) = rnf x1 `seq` ()
258 rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
259 rnf (MatchRefine x1) = rnf x1 `seq` ()
260 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
261 rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
262 rnf (Exact x1) = rnf x1 `seq` ()
263 rnf Compute = ()
264 rnf Trivial = ()
265 rnf TCInstance = ()
266 rnf (ProofSearch r r1 r2 x1 x2)
267 = rnf x1 `seq` rnf x2 `seq` ()
268 rnf Solve = ()
269 rnf Attack = ()
270 rnf ProofState = ()
271 rnf ProofTerm = ()
272 rnf Undo = ()
273 rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
274 rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
275 rnf (ApplyTactic x1) = rnf x1 `seq` ()
276 rnf (ByReflection x1) = rnf x1 `seq` ()
277 rnf (Reflect x1) = rnf x1 `seq` ()
278 rnf (Fill x1) = rnf x1 `seq` ()
279 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
280 rnf Qed = ()
281 rnf Abandon = ()
282 rnf (TCheck x1) = rnf x1 `seq` ()
283 rnf (TEval x1) = rnf x1 `seq` ()
284 rnf (TDocStr x1) = x1 `seq` ()
285 rnf (TSearch x1) = rnf x1 `seq` ()
286 rnf Skip = ()
287 rnf (TFail x1) = rnf x1 `seq` ()
288 rnf SourceFC = ()
289 rnf Unfocus = ()
291instance NFData ErrorReportPart where
292 rnf (TermPart x1) = rnf x1 `seq` ()
293 rnf (TextPart x1) = rnf x1 `seq` ()
294 rnf (NamePart x1) = rnf x1 `seq` ()
295 rnf (SubReport x1) = rnf x1 `seq` ()
297instance (NFData t) => NFData (PDo' t) where
298 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
299 rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
300 rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
301 rnf (DoLet x1 x2 x3 x4)
302 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
303 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
305instance (NFData t) => NFData (PArg' t) where
306 rnf (PImp x1 x2 x3 x4 x5)
307 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
308 rnf (PExp x1 x2 x3 x4)
309 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
310 rnf (PConstraint x1 x2 x3 x4)
311 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
312 rnf (PTacImplicit x1 x2 x3 x4 x5)
313 = rnf x1 `seq`
314 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
316instance NFData ClassInfo where
317 rnf (CI x1 x2 x3 x4 x5 x6 x7)
318 = rnf x1 `seq`
319 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
321instance NFData OptInfo where
322 rnf (Optimise x1 x2)
323 = rnf x1 `seq` rnf x2 `seq` ()
325instance NFData TypeInfo where
326 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
328instance (NFData t) => NFData (DSL' t) where
329 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
330 = rnf x1 `seq`
331 rnf x2 `seq`
332 rnf x3 `seq`
333 rnf x4 `seq`
334 rnf x5 `seq`
335 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
337instance NFData SynContext where
338 rnf PatternSyntax = ()
339 rnf TermSyntax = ()
340 rnf AnySyntax = ()
342instance NFData Syntax where
343 rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
345instance NFData SSymbol where
346 rnf (Keyword x1) = rnf x1 `seq` ()
347 rnf (Symbol x1) = rnf x1 `seq` ()
348 rnf (Binding x1) = rnf x1 `seq` ()
349 rnf (Expr x1) = rnf x1 `seq` ()
350 rnf (SimpleExpr x1) = rnf x1 `seq` ()
352instance NFData Using where
353 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
354 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
356instance NFData SyntaxInfo where
357 rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
358 = rnf x1 `seq`
359 rnf x2 `seq`
360 rnf x3 `seq`
361 rnf x4 `seq`
362 rnf x5 `seq`
363 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()