git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/src/Idris/Core/DeepSeq.hs
234 lines 8.7 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` ()
29instance NFData Universe where
30 rnf NullType = ()
31 rnf UniqueType = ()
32 rnf AllTypes = ()
34instance NFData Raw where
35 rnf (Var x1) = rnf x1 `seq` ()
36 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
37 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
38 rnf RType = ()
39 rnf (RUType x1) = rnf x1 `seq` ()
40 rnf (RForce x1) = rnf x1 `seq` ()
41 rnf (RConstant x1) = x1 `seq` ()
43instance NFData FC where
44 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
46instance NFData Provenance where
47 rnf ExpectedType = ()
48 rnf InferredVal = ()
49 rnf GivenVal = ()
50 rnf (SourceTerm x1) = rnf x1 `seq` ()
51 rnf (TooManyArgs x1) = rnf x1 `seq` ()
53instance NFData Err where
54 rnf (Msg x1) = rnf x1 `seq` ()
55 rnf (InternalMsg x1) = rnf x1 `seq` ()
56 rnf (CantUnify x1 x2 x3 x4 x5 x6)
57 = rnf x1 `seq`
58 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
59 rnf (InfiniteUnify x1 x2 x3)
60 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
61 rnf (CantConvert x1 x2 x3)
62 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
63 rnf (UnifyScope x1 x2 x3 x4)
64 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
65 rnf (ElaboratingArg x1 x2 x3 x4)
66 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
67 rnf (CantInferType x1) = rnf x1 `seq` ()
68 rnf (CantMatch x1) = rnf x1 `seq` ()
69 rnf (ReflectionError x1 x2) = x1 `seq` rnf x2 `seq` ()
70 rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
71 rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
72 rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
73 rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
74 rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
75 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
76 rnf (CantIntroduce x1) = rnf x1 `seq` ()
77 rnf (TooManyArguments x1) = rnf x1 `seq` ()
78 rnf (WithFnType x1) = rnf x1 `seq` ()
79 rnf (NoSuchVariable x1) = rnf x1 `seq` ()
80 rnf (NoTypeDecl x1) = rnf x1 `seq` ()
81 rnf (NotInjective x1 x2 x3)
82 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
83 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
84 rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
85 rnf (CantResolveAlts x1) = rnf x1 `seq` ()
86 rnf (IncompleteTerm x1) = rnf x1 `seq` ()
87 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
88 rnf UniverseError = ()
89 rnf ProgramLineComment = ()
90 rnf (Inaccessible x1) = rnf x1 `seq` ()
91 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()
92 rnf (AlreadyDefined x1) = rnf x1 `seq` ()
93 rnf (ProofSearchFail x1) = rnf x1 `seq` ()
94 rnf (NoRewriting x1) = rnf x1 `seq` ()
95 rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
96 rnf (Elaborating x1 x2 x3)
97 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
98 rnf (ProviderError x1) = rnf x1 `seq` ()
99 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
100 rnf (ElabDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
102instance NFData ImplicitInfo where
103 rnf (Impl x1) = rnf x1 `seq` ()
105instance (NFData b) => NFData (Binder b) where
106 rnf (Lam x1) = rnf x1 `seq` ()
107 rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
108 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
109 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
110 rnf (Hole x1) = rnf x1 `seq` ()
111 rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
112 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
113 rnf (PVar x1) = rnf x1 `seq` ()
114 rnf (PVTy x1) = rnf x1 `seq` ()
116instance NFData UExp where
117 rnf (UVar x1) = rnf x1 `seq` ()
118 rnf (UVal x1) = rnf x1 `seq` ()
120instance NFData NameType where
121 rnf Bound = ()
122 rnf Ref = ()
123 rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
124 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
126instance NFData NativeTy where
127 rnf IT8 = ()
128 rnf IT16 = ()
129 rnf IT32 = ()
130 rnf IT64 = ()
132instance NFData IntTy where
133 rnf (ITFixed x1) = rnf x1 `seq` ()
134 rnf ITNative = ()
135 rnf ITBig = ()
136 rnf ITChar = ()
137 rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
139instance NFData ArithTy where
140 rnf (ATInt x1) = rnf x1 `seq` ()
141 rnf ATFloat = ()
143instance NFData Const where
144 rnf (I x1) = rnf x1 `seq` ()
145 rnf (BI x1) = rnf x1 `seq` ()
146 rnf (Fl x1) = rnf x1 `seq` ()
147 rnf (Ch x1) = rnf x1 `seq` ()
148 rnf (Str x1) = rnf x1 `seq` ()
149 rnf (B8 x1) = rnf x1 `seq` ()
150 rnf (B16 x1) = rnf x1 `seq` ()
151 rnf (B32 x1) = rnf x1 `seq` ()
152 rnf (B64 x1) = rnf x1 `seq` ()
153 rnf (B8V x1) = rnf x1 `seq` ()
154 rnf (B16V x1) = rnf x1 `seq` ()
155 rnf (B32V x1) = rnf x1 `seq` ()
156 rnf (B64V x1) = rnf x1 `seq` ()
157 rnf (AType x1) = rnf x1 `seq` ()
158 rnf WorldType = ()
159 rnf TheWorld = ()
160 rnf StrType = ()
161 rnf PtrType = ()
162 rnf ManagedPtrType = ()
163 rnf BufferType = ()
164 rnf VoidType = ()
165 rnf Forgot = ()
167instance (NFData n) => NFData (TT n) where
168 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
169 rnf (V x1) = rnf x1 `seq` ()
170 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
171 rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
172 rnf (Constant x1) = rnf x1 `seq` ()
173 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
174 rnf Erased = ()
175 rnf Impossible = ()
176 rnf (TType x1) = rnf x1 `seq` ()
177 rnf (UType _) = ()
179instance NFData Accessibility where
180 rnf Public = ()
181 rnf Frozen = ()
182 rnf Hidden = ()
185instance NFData Totality where
186 rnf (Total x1) = rnf x1 `seq` ()
187 rnf Productive = ()
188 rnf (Partial x1) = rnf x1 `seq` ()
189 rnf Unchecked = ()
191instance NFData PReason where
192 rnf (Other x1) = rnf x1 `seq` ()
193 rnf Itself = ()
194 rnf NotCovering = ()
195 rnf NotPositive = ()
196 rnf (UseUndef x1) = rnf x1 `seq` ()
197 rnf ExternalIO = ()
198 rnf BelieveMe = ()
199 rnf (Mutual x1) = rnf x1 `seq` ()
200 rnf NotProductive = ()
202instance NFData MetaInformation where
203 rnf EmptyMI = ()
204 rnf (DataMI x1) = rnf x1 `seq` ()
206instance NFData Def where
207 rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
208 rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
209 rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
210 rnf (CaseOp x1 x2 x3 x4 x5 x6)
211 = rnf x1 `seq`
212 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
214instance NFData CaseInfo where
215 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
217instance NFData CaseDefs where
218 rnf (CaseDefs x1 x2 x3 x4)
219 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
221instance (NFData t) => NFData (SC' t) where
222 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
223 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
224 rnf (STerm x1) = rnf x1 `seq` ()
225 rnf (UnmatchedCase x1) = rnf x1 `seq` ()
226 rnf ImpossibleCase = ()
228instance (NFData t) => NFData (CaseAlt' t) where
229 rnf (ConCase x1 x2 x3 x4)
230 = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()
231 rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()
232 rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()
233 rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()
234 rnf (DefaultCase x1) = rnf x1 `seq` ()