git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/DeepSeq.hs
117 lines 4.8 kB history raw
1module Idris.Core.DeepSeq where
3import Idris.Core.TT
4import Idris.Core.CaseTree
6import Control.DeepSeq
8instance NFData Name where
9 rnf (UN x1) = rnf x1 `seq` ()
10 rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
11 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
12 rnf NErased = ()
13 rnf (SN x1) = rnf x1 `seq` ()
15instance NFData SpecialName where
16 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
17 rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
18 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
19 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
20 rnf (MethodN x1) = rnf x1 `seq` ()
21 rnf (CaseN x1) = rnf x1 `seq` ()
22 rnf (ElimN x1) = rnf x1 `seq` ()
23 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
25instance NFData Raw where
26 rnf (Var x1) = rnf x1 `seq` ()
27 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
28 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
29 rnf RType = ()
30 rnf (RForce x1) = rnf x1 `seq` ()
31 rnf (RConstant x1) = x1 `seq` ()
33instance NFData FC where
34 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
36instance NFData Err where
37 rnf (Msg x1) = rnf x1 `seq` ()
38 rnf (InternalMsg x1) = rnf x1 `seq` ()
39 rnf (CantUnify x1 x2 x3 x4 x5 x6)
40 = rnf x1 `seq`
41 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
42 rnf (InfiniteUnify x1 x2 x3)
43 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
44 rnf (CantConvert x1 x2 x3)
45 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
46 rnf (UnifyScope x1 x2 x3 x4)
47 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
48 rnf (CantInferType x1) = rnf x1 `seq` ()
49 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
50 rnf (CantIntroduce x1) = rnf x1 `seq` ()
51 rnf (NoSuchVariable x1) = rnf x1 `seq` ()
52 rnf (NoTypeDecl x1) = rnf x1 `seq` ()
53 rnf (NotInjective x1 x2 x3)
54 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
55 rnf (CantResolve x1) = rnf x1 `seq` ()
56 rnf (CantResolveAlts x1) = rnf x1 `seq` ()
57 rnf (IncompleteTerm x1) = rnf x1 `seq` ()
58 rnf UniverseError = ()
59 rnf ProgramLineComment = ()
60 rnf (Inaccessible x1) = rnf x1 `seq` ()
61 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()
62 rnf (AlreadyDefined x1) = rnf x1 `seq` ()
63 rnf (ProofSearchFail x1) = rnf x1 `seq` ()
64 rnf (NoRewriting x1) = rnf x1 `seq` ()
65 rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
66 rnf (Elaborating x1 x2 x3)
67 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
68 rnf (ProviderError x1) = rnf x1 `seq` ()
69 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
71instance (NFData b) => NFData (Binder b) where
72 rnf (Lam x1) = rnf x1 `seq` ()
73 rnf (Pi x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
74 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
75 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
76 rnf (Hole x1) = rnf x1 `seq` ()
77 rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
78 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
79 rnf (PVar x1) = rnf x1 `seq` ()
80 rnf (PVTy x1) = rnf x1 `seq` ()
82instance NFData UExp where
83 rnf (UVar x1) = rnf x1 `seq` ()
84 rnf (UVal x1) = rnf x1 `seq` ()
86instance NFData NameType where
87 rnf Bound = ()
88 rnf Ref = ()
89 rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
90 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
92instance (NFData n) => NFData (TT n) where
93 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
94 rnf (V x1) = rnf x1 `seq` ()
95 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
96 rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
97 rnf (Constant x1) = x1 `seq` ()
98 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
99 rnf Erased = ()
100 rnf Impossible = ()
101 rnf (TType x1) = rnf x1 `seq` ()
102 rnf (UType _) = ()
104instance (NFData t) => NFData (SC' t) where
105 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
106 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
107 rnf (STerm x1) = rnf x1 `seq` ()
108 rnf (UnmatchedCase x1) = rnf x1 `seq` ()
109 rnf ImpossibleCase = ()
111instance (NFData t) => NFData (CaseAlt' t) where
112 rnf (ConCase x1 x2 x3 x4)
113 = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()
114 rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()
115 rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()
116 rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()
117 rnf (DefaultCase x1) = rnf x1 `seq` ()