git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Core/DeepSeq.hs
247 lines 9.3 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Core.DeepSeq where
5import Idris.Core.TT
6import Idris.Core.CaseTree
7import Idris.Core.Evaluate
9import Control.DeepSeq
11instance NFData Name where
12 rnf (UN x1) = rnf x1 `seq` ()
13 rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
14 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
15 rnf NErased = ()
16 rnf (SN x1) = rnf x1 `seq` ()
17 rnf (SymRef x1) = rnf x1 `seq` ()
19instance NFData SpecialName where
20 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
21 rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
22 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
23 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
24 rnf (MethodN x1) = rnf x1 `seq` ()
25 rnf (CaseN x1) = rnf x1 `seq` ()
26 rnf (ElimN x1) = rnf x1 `seq` ()
27 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
28 rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
30instance NFData Universe where
31 rnf NullType = ()
32 rnf UniqueType = ()
33 rnf AllTypes = ()
35instance NFData Raw where
36 rnf (Var x1) = rnf x1 `seq` ()
37 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
38 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
39 rnf RType = ()
40 rnf (RUType x1) = rnf x1 `seq` ()
41 rnf (RForce x1) = rnf x1 `seq` ()
42 rnf (RConstant x1) = x1 `seq` ()
44instance NFData FC where
45 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
46 rnf NoFC = ()
47 rnf (FileFC f) = rnf f `seq` ()
49instance NFData Provenance where
50 rnf ExpectedType = ()
51 rnf InferredVal = ()
52 rnf GivenVal = ()
53 rnf (SourceTerm x1) = rnf x1 `seq` ()
54 rnf (TooManyArgs x1) = rnf x1 `seq` ()
56instance NFData UConstraint where
57 rnf (ULT x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
58 rnf (ULE x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
60instance NFData ConstraintFC where
61 rnf (ConstraintFC x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
63instance NFData Err where
64 rnf (Msg x1) = rnf x1 `seq` ()
65 rnf (InternalMsg x1) = rnf x1 `seq` ()
66 rnf (CantUnify x1 x2 x3 x4 x5 x6)
67 = rnf x1 `seq`
68 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
69 rnf (InfiniteUnify x1 x2 x3)
70 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
71 rnf (CantConvert x1 x2 x3)
72 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
73 rnf (UnifyScope x1 x2 x3 x4)
74 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
75 rnf (ElaboratingArg x1 x2 x3 x4)
76 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
77 rnf (CantInferType x1) = rnf x1 `seq` ()
78 rnf (CantMatch x1) = rnf x1 `seq` ()
79 rnf (ReflectionError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
80 rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
81 rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
82 rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
83 rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
84 rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
85 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
86 rnf (CantIntroduce x1) = rnf x1 `seq` ()
87 rnf (TooManyArguments x1) = rnf x1 `seq` ()
88 rnf (WithFnType x1) = rnf x1 `seq` ()
89 rnf (NoSuchVariable x1) = rnf x1 `seq` ()
90 rnf (NoTypeDecl x1) = rnf x1 `seq` ()
91 rnf (NotInjective x1 x2 x3)
92 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
93 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
94 rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
95 rnf (CantResolveAlts x1) = rnf x1 `seq` ()
96 rnf (NoValidAlts x1) = rnf x1 `seq` ()
97 rnf (IncompleteTerm x1) = rnf x1 `seq` ()
98 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
99 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
100 rnf ProgramLineComment = ()
101 rnf (Inaccessible x1) = rnf x1 `seq` ()
102 rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
103 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()
104 rnf (AlreadyDefined x1) = rnf x1 `seq` ()
105 rnf (ProofSearchFail x1) = rnf x1 `seq` ()
106 rnf (NoRewriting x1) = rnf x1 `seq` ()
107 rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
108 rnf (Elaborating x1 x2 x3)
109 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
110 rnf (ProviderError x1) = rnf x1 `seq` ()
111 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
112 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
113 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()
115instance NFData ErrorReportPart where
116 rnf (TextPart x1) = rnf x1 `seq` ()
117 rnf (TermPart x1) = rnf x1 `seq` ()
118 rnf (RawPart x1) = rnf x1 `seq` ()
119 rnf (NamePart x1) = rnf x1 `seq` ()
120 rnf (SubReport x1) = rnf x1 `seq` ()
122instance NFData ImplicitInfo where
123 rnf (Impl x1) = rnf x1 `seq` ()
125instance (NFData b) => NFData (Binder b) where
126 rnf (Lam x1) = rnf x1 `seq` ()
127 rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
128 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
129 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
130 rnf (Hole x1) = rnf x1 `seq` ()
131 rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
132 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
133 rnf (PVar x1) = rnf x1 `seq` ()
134 rnf (PVTy x1) = rnf x1 `seq` ()
136instance NFData UExp where
137 rnf (UVar x1) = rnf x1 `seq` ()
138 rnf (UVal x1) = rnf x1 `seq` ()
140instance NFData NameType where
141 rnf Bound = ()
142 rnf Ref = ()
143 rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
144 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
146instance NFData NativeTy where
147 rnf IT8 = ()
148 rnf IT16 = ()
149 rnf IT32 = ()
150 rnf IT64 = ()
152instance NFData IntTy where
153 rnf (ITFixed x1) = rnf x1 `seq` ()
154 rnf ITNative = ()
155 rnf ITBig = ()
156 rnf ITChar = ()
158instance NFData ArithTy where
159 rnf (ATInt x1) = rnf x1 `seq` ()
160 rnf ATFloat = ()
162instance NFData Const where
163 rnf (I x1) = rnf x1 `seq` ()
164 rnf (BI x1) = rnf x1 `seq` ()
165 rnf (Fl x1) = rnf x1 `seq` ()
166 rnf (Ch x1) = rnf x1 `seq` ()
167 rnf (Str x1) = rnf x1 `seq` ()
168 rnf (B8 x1) = rnf x1 `seq` ()
169 rnf (B16 x1) = rnf x1 `seq` ()
170 rnf (B32 x1) = rnf x1 `seq` ()
171 rnf (B64 x1) = rnf x1 `seq` ()
172 rnf (AType x1) = rnf x1 `seq` ()
173 rnf WorldType = ()
174 rnf TheWorld = ()
175 rnf StrType = ()
176 rnf VoidType = ()
177 rnf Forgot = ()
179instance (NFData n) => NFData (TT n) where
180 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
181 rnf (V x1) = rnf x1 `seq` ()
182 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
183 rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()
184 rnf (Constant x1) = rnf x1 `seq` ()
185 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
186 rnf Erased = ()
187 rnf Impossible = ()
188 rnf (TType x1) = rnf x1 `seq` ()
189 rnf (UType _) = ()
191instance NFData Accessibility where
192 rnf Public = ()
193 rnf Frozen = ()
194 rnf Hidden = ()
197instance NFData Totality where
198 rnf (Total x1) = rnf x1 `seq` ()
199 rnf Productive = ()
200 rnf (Partial x1) = rnf x1 `seq` ()
201 rnf Unchecked = ()
202 rnf Generated = ()
204instance NFData PReason where
205 rnf (Other x1) = rnf x1 `seq` ()
206 rnf Itself = ()
207 rnf NotCovering = ()
208 rnf NotPositive = ()
209 rnf (UseUndef x1) = rnf x1 `seq` ()
210 rnf ExternalIO = ()
211 rnf BelieveMe = ()
212 rnf (Mutual x1) = rnf x1 `seq` ()
213 rnf NotProductive = ()
215instance NFData MetaInformation where
216 rnf EmptyMI = ()
217 rnf (DataMI x1) = rnf x1 `seq` ()
219instance NFData Def where
220 rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
221 rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
222 rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
223 rnf (CaseOp x1 x2 x3 x4 x5 x6)
224 = rnf x1 `seq`
225 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
227instance NFData CaseInfo where
228 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
230instance NFData CaseDefs where
231 rnf (CaseDefs x1 x2 x3 x4)
232 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
234instance (NFData t) => NFData (SC' t) where
235 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
236 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
237 rnf (STerm x1) = rnf x1 `seq` ()
238 rnf (UnmatchedCase x1) = rnf x1 `seq` ()
239 rnf ImpossibleCase = ()
241instance (NFData t) => NFData (CaseAlt' t) where
242 rnf (ConCase x1 x2 x3 x4)
243 = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()
244 rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()
245 rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()
246 rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()
247 rnf (DefaultCase x1) = rnf x1 `seq` ()