git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Core/DeepSeq.hs
226 lines 8.4 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 = ()
138instance NFData ArithTy where
139 rnf (ATInt x1) = rnf x1 `seq` ()
140 rnf ATFloat = ()
142instance NFData Const where
143 rnf (I x1) = rnf x1 `seq` ()
144 rnf (BI x1) = rnf x1 `seq` ()
145 rnf (Fl x1) = rnf x1 `seq` ()
146 rnf (Ch x1) = rnf x1 `seq` ()
147 rnf (Str x1) = rnf x1 `seq` ()
148 rnf (B8 x1) = rnf x1 `seq` ()
149 rnf (B16 x1) = rnf x1 `seq` ()
150 rnf (B32 x1) = rnf x1 `seq` ()
151 rnf (B64 x1) = rnf x1 `seq` ()
152 rnf (AType x1) = rnf x1 `seq` ()
153 rnf WorldType = ()
154 rnf TheWorld = ()
155 rnf StrType = ()
156 rnf VoidType = ()
157 rnf Forgot = ()
159instance (NFData n) => NFData (TT n) where
160 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
161 rnf (V x1) = rnf x1 `seq` ()
162 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
163 rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
164 rnf (Constant x1) = rnf x1 `seq` ()
165 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
166 rnf Erased = ()
167 rnf Impossible = ()
168 rnf (TType x1) = rnf x1 `seq` ()
169 rnf (UType _) = ()
171instance NFData Accessibility where
172 rnf Public = ()
173 rnf Frozen = ()
174 rnf Hidden = ()
177instance NFData Totality where
178 rnf (Total x1) = rnf x1 `seq` ()
179 rnf Productive = ()
180 rnf (Partial x1) = rnf x1 `seq` ()
181 rnf Unchecked = ()
183instance NFData PReason where
184 rnf (Other x1) = rnf x1 `seq` ()
185 rnf Itself = ()
186 rnf NotCovering = ()
187 rnf NotPositive = ()
188 rnf (UseUndef x1) = rnf x1 `seq` ()
189 rnf ExternalIO = ()
190 rnf BelieveMe = ()
191 rnf (Mutual x1) = rnf x1 `seq` ()
192 rnf NotProductive = ()
194instance NFData MetaInformation where
195 rnf EmptyMI = ()
196 rnf (DataMI x1) = rnf x1 `seq` ()
198instance NFData Def where
199 rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
200 rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
201 rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
202 rnf (CaseOp x1 x2 x3 x4 x5 x6)
203 = rnf x1 `seq`
204 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
206instance NFData CaseInfo where
207 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
209instance NFData CaseDefs where
210 rnf (CaseDefs x1 x2 x3 x4)
211 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
213instance (NFData t) => NFData (SC' t) where
214 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
215 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
216 rnf (STerm x1) = rnf x1 `seq` ()
217 rnf (UnmatchedCase x1) = rnf x1 `seq` ()
218 rnf ImpossibleCase = ()
220instance (NFData t) => NFData (CaseAlt' t) where
221 rnf (ConCase x1 x2 x3 x4)
222 = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()
223 rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()
224 rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()
225 rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()
226 rnf (DefaultCase x1) = rnf x1 `seq` ()