git.iko.soy/Idris-dev
on master help sign in
Do more forcing in IBC
2ec25c2Edwin Brady
src/Idris/AbsSyntax.hs+1
compare with master
unifiedsplit
@@ -379,6 +379,7 @@ resetNameIdx = do i <- getIState
379addNameIdx :: Name -> Idris (Int, Name)
379addNameIdx :: Name -> Idris (Int, Name)
380addNameIdx n = do i <- getIState
380addNameIdx n = do i <- getIState
381 let (i', x) = addNameIdx' i n
381 let (i', x) = addNameIdx' i n
382+ putIState i'
382 return x
383 return x
383
384
384addNameIdx' :: IState -> Name -> (IState, (Int, Name))
385addNameIdx' :: IState -> Name -> (IState, (Int, Name))
src/Idris/AbsSyntaxTree.hs+4
@@ -313,6 +313,9 @@ data Codegen = Via String
313-- | ViaLLVM
313-- | ViaLLVM
314 | Bytecode
314 | Bytecode
315 deriving (Show, Eq)
315 deriving (Show, Eq)
316+{-!
317+deriving instance NFData Codegen
318+!-}
316
319
317-- | REPL commands
320-- | REPL commands
318data Command = Quit
321data Command = Quit
@@ -944,6 +947,7 @@ data FnInfo = FnInfo { fn_params :: [Int] }
944 deriving Show
947 deriving Show
945{-!
948{-!
946deriving instance Binary FnInfo
949deriving instance Binary FnInfo
950+deriving instance NFData FnInfo
947!-}
951!-}
948
952
949data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
953data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
src/Idris/Core/DeepSeq.hs+103−1
@@ -1,7 +1,10 @@
1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
2+
1module Idris.Core.DeepSeq where
3module Idris.Core.DeepSeq where
2
4
3import Idris.Core.TT
5import Idris.Core.TT
4import Idris.Core.CaseTree
6import Idris.Core.CaseTree
7+import Idris.Core.Evaluate
5
8
6import Control.DeepSeq
9import Control.DeepSeq
7
10
@@ -11,6 +14,7 @@ instance NFData Name where
11 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
14 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
12 rnf NErased = ()
15 rnf NErased = ()
13 rnf (SN x1) = rnf x1 `seq` ()
16 rnf (SN x1) = rnf x1 `seq` ()
17+ rnf (SymRef x1) = rnf x1 `seq` ()
14
18
15instance NFData SpecialName where
19instance NFData SpecialName where
16 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
20 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
@@ -22,11 +26,17 @@ instance NFData SpecialName where
22 rnf (ElimN x1) = rnf x1 `seq` ()
26 rnf (ElimN x1) = rnf x1 `seq` ()
23 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
27 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
24
28
29+instance NFData Universe where
30+ rnf NullType = ()
31+ rnf UniqueType = ()
32+ rnf AllTypes = ()
33+
25instance NFData Raw where
34instance NFData Raw where
26 rnf (Var x1) = rnf x1 `seq` ()
35 rnf (Var x1) = rnf x1 `seq` ()
27 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
36 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` ()
37 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
29 rnf RType = ()
38 rnf RType = ()
39+ rnf (RUType x1) = rnf x1 `seq` ()
30 rnf (RForce x1) = rnf x1 `seq` ()
40 rnf (RForce x1) = rnf x1 `seq` ()
31 rnf (RConstant x1) = x1 `seq` ()
41 rnf (RConstant x1) = x1 `seq` ()
32
42
@@ -45,9 +55,20 @@ instance NFData Err where
45 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
55 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
46 rnf (UnifyScope x1 x2 x3 x4)
56 rnf (UnifyScope x1 x2 x3 x4)
47 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
57 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
58+ rnf (ElaboratingArg x1 x2 x3 x4)
59+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
48 rnf (CantInferType x1) = rnf x1 `seq` ()
60 rnf (CantInferType x1) = rnf x1 `seq` ()
61+ rnf (CantMatch x1) = rnf x1 `seq` ()
62+ rnf (ReflectionError x1 x2) = x1 `seq` rnf x2 `seq` ()
63+ rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
64+ rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
65+ rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
66+ rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
67+ rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
49 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
68 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
50 rnf (CantIntroduce x1) = rnf x1 `seq` ()
69 rnf (CantIntroduce x1) = rnf x1 `seq` ()
70+ rnf (TooManyArguments x1) = rnf x1 `seq` ()
71+ rnf (WithFnType x1) = rnf x1 `seq` ()
51 rnf (NoSuchVariable x1) = rnf x1 `seq` ()
72 rnf (NoSuchVariable x1) = rnf x1 `seq` ()
52 rnf (NoTypeDecl x1) = rnf x1 `seq` ()
73 rnf (NoTypeDecl x1) = rnf x1 `seq` ()
53 rnf (NotInjective x1 x2 x3)
74 rnf (NotInjective x1 x2 x3)
@@ -89,18 +110,99 @@ instance NFData NameType where
89 rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
110 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` ()
111 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
91
112
113+instance NFData NativeTy where
114+ rnf IT8 = ()
115+ rnf IT16 = ()
116+ rnf IT32 = ()
117+ rnf IT64 = ()
118+
119+instance NFData IntTy where
120+ rnf (ITFixed x1) = rnf x1 `seq` ()
121+ rnf ITNative = ()
122+ rnf ITBig = ()
123+ rnf ITChar = ()
124+ rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
125+
126+instance NFData ArithTy where
127+ rnf (ATInt x1) = rnf x1 `seq` ()
128+ rnf ATFloat = ()
129+
130+instance NFData Const where
131+ rnf (I x1) = rnf x1 `seq` ()
132+ rnf (BI x1) = rnf x1 `seq` ()
133+ rnf (Fl x1) = rnf x1 `seq` ()
134+ rnf (Ch x1) = rnf x1 `seq` ()
135+ rnf (Str x1) = rnf x1 `seq` ()
136+ rnf (B8 x1) = rnf x1 `seq` ()
137+ rnf (B16 x1) = rnf x1 `seq` ()
138+ rnf (B32 x1) = rnf x1 `seq` ()
139+ rnf (B64 x1) = rnf x1 `seq` ()
140+ rnf (B8V x1) = rnf x1 `seq` ()
141+ rnf (B16V x1) = rnf x1 `seq` ()
142+ rnf (B32V x1) = rnf x1 `seq` ()
143+ rnf (B64V x1) = rnf x1 `seq` ()
144+ rnf (AType x1) = rnf x1 `seq` ()
145+ rnf StrType = ()
146+ rnf PtrType = ()
147+ rnf ManagedPtrType = ()
148+ rnf BufferType = ()
149+ rnf VoidType = ()
150+ rnf Forgot = ()
151+
92instance (NFData n) => NFData (TT n) where
152instance (NFData n) => NFData (TT n) where
93 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
153 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
94 rnf (V x1) = rnf x1 `seq` ()
154 rnf (V x1) = rnf x1 `seq` ()
95 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
155 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` ()
156 rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
97− rnf (Constant x1) = x1 `seq` ()
157+ rnf (Constant x1) = rnf x1 `seq` ()
98 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
158 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
99 rnf Erased = ()
159 rnf Erased = ()
100 rnf Impossible = ()
160 rnf Impossible = ()
101 rnf (TType x1) = rnf x1 `seq` ()
161 rnf (TType x1) = rnf x1 `seq` ()
102 rnf (UType _) = ()
162 rnf (UType _) = ()
103
163
164+instance NFData Accessibility where
165+ rnf Public = ()
166+ rnf Frozen = ()
167+ rnf Hidden = ()
168+
169+
170+instance NFData Totality where
171+ rnf (Total x1) = rnf x1 `seq` ()
172+ rnf Productive = ()
173+ rnf (Partial x1) = rnf x1 `seq` ()
174+ rnf Unchecked = ()
175+
176+instance NFData PReason where
177+ rnf (Other x1) = rnf x1 `seq` ()
178+ rnf Itself = ()
179+ rnf NotCovering = ()
180+ rnf NotPositive = ()
181+ rnf (UseUndef x1) = rnf x1 `seq` ()
182+ rnf ExternalIO = ()
183+ rnf BelieveMe = ()
184+ rnf (Mutual x1) = rnf x1 `seq` ()
185+ rnf NotProductive = ()
186+
187+instance NFData MetaInformation where
188+ rnf EmptyMI = ()
189+ rnf (DataMI x1) = rnf x1 `seq` ()
190+
191+instance NFData Def where
192+ rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
193+ rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
194+ rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
195+ rnf (CaseOp x1 x2 x3 x4 x5 x6)
196+ = rnf x1 `seq`
197+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
198+
199+instance NFData CaseInfo where
200+ rnf (CaseInfo x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
201+
202+instance NFData CaseDefs where
203+ rnf (CaseDefs x1 x2 x3 x4)
204+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
205+
104instance (NFData t) => NFData (SC' t) where
206instance (NFData t) => NFData (SC' t) where
105 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
207 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
106 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
208 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
src/Idris/Core/Evaluate.hs+18
@@ -692,6 +692,15 @@ deriving instance Binary CaseInfo
692{-!
692{-!
693deriving instance Binary CaseDefs
693deriving instance Binary CaseDefs
694!-}
694!-}
695+{-!
696+deriving instance NFData Def
697+!-}
698+{-!
699+deriving instance NFData CaseInfo
700+!-}
701+{-!
702+deriving instance NFData CaseDefs
703+!-}
695
704
696instance Show Def where
705instance Show Def where
697 show (Function ty tm) = "Function: " ++ show (ty, tm)
706 show (Function ty tm) = "Function: " ++ show (ty, tm)
@@ -717,6 +726,9 @@ instance Show Def where
717
726
718data Accessibility = Public | Frozen | Hidden
727data Accessibility = Public | Frozen | Hidden
719 deriving (Show, Eq)
728 deriving (Show, Eq)
729+{-!
730+deriving instance NFData Accessibility
731+!-}
720
732
721-- | The result of totality checking
733-- | The result of totality checking
722data Totality = Total [Int] -- ^ well-founded arguments
734data Totality = Total [Int] -- ^ well-founded arguments
@@ -724,11 +736,17 @@ data Totality = Total [Int] -- ^ well-founded arguments
724 | Partial PReason
736 | Partial PReason
725 | Unchecked
737 | Unchecked
726 deriving Eq
738 deriving Eq
739+{-!
740+deriving instance NFData Totality
741+!-}
727
742
728-- | Reasons why a function may not be total
743-- | Reasons why a function may not be total
729data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
744data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
730 | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
745 | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
731 deriving (Show, Eq)
746 deriving (Show, Eq)
747+{-!
748+deriving instance NFData PReason
749+!-}
732
750
733instance Show Totality where
751instance Show Totality where
734 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
752 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
src/Idris/Core/TT.hs+1−1
@@ -241,7 +241,7 @@ score _ = 0
241instance Show Err where
241instance Show Err where
242 show (Msg s) = s
242 show (Msg s) = s
243 show (InternalMsg s) = "Internal error: " ++ show s
243 show (InternalMsg s) = "Internal error: " ++ show s
244− show (CantUnify rec l r e sc i) = "CantUnify " ++ show rec ++ " " ++
244+ show (CantUnify rcv l r e sc i) = "CantUnify " ++ show rcv ++ " " ++
245 show l ++ " " ++ show r ++ " " ++
245 show l ++ " " ++ show r ++ " " ++
246 show e ++ " in " ++ show sc ++ " " ++ show i
246 show e ++ " in " ++ show sc ++ " " ++ show i
247 show (CantSolveGoal g _) = "CantSolve " ++ show g
247 show (CantSolveGoal g _) = "CantSolve " ++ show g
src/Idris/DeepSeq.hs+33−17
@@ -1,6 +1,9 @@
1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
2+
1module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where
3module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where
2
4
3import Idris.Core.DeepSeq
5import Idris.Core.DeepSeq
6+import Idris.Docstrings
4import Idris.Core.TT
7import Idris.Core.TT
5import Idris.AbsSyntaxTree
8import Idris.AbsSyntaxTree
6
9
@@ -48,24 +51,13 @@ instance NFData CT.NumWrapper where
48 rnf CT.PeriodFollowing = ()
51 rnf CT.PeriodFollowing = ()
49 rnf CT.ParenFollowing = ()
52 rnf CT.ParenFollowing = ()
50
53
51−-- All generated by 'derive'
54+instance 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` ()
52
59
53−instance NFData IntTy where
60+-- All generated by 'derive'
54− rnf (ITFixed x1) = rnf x1 `seq` ()
55− rnf ITNative = ()
56− rnf ITBig = ()
57− rnf ITChar = ()
58− rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
59−
60−instance NFData NativeTy where
61− rnf IT8 = ()
62− rnf IT16 = ()
63− rnf IT32 = ()
64− rnf IT64 = ()
65−
66−instance NFData ArithTy where
67− rnf (ATInt x1) = rnf x1 `seq` ()
68− rnf ATFloat = ()
69
61
70instance NFData SizeChange where
62instance NFData SizeChange where
71 rnf Smaller = ()
63 rnf Smaller = ()
@@ -73,6 +65,13 @@ instance NFData SizeChange where
73 rnf Bigger = ()
65 rnf Bigger = ()
74 rnf Unknown = ()
66 rnf Unknown = ()
75
67
68+instance NFData FnInfo where
69+ rnf (FnInfo x1) = rnf x1 `seq` ()
70+
71+instance NFData Codegen where
72+ rnf (Via x1) = rnf x1 `seq` ()
73+ rnf Bytecode = ()
74+
76instance NFData CGInfo where
75instance NFData CGInfo where
77 rnf (CGInfo x1 x2 x3 x4 x5)
76 rnf (CGInfo x1 x2 x3 x4 x5)
78 = rnf x1 `seq`
77 = rnf x1 `seq`
@@ -108,18 +107,24 @@ instance NFData FnOpt where
108 rnf Inlinable = ()
107 rnf Inlinable = ()
109 rnf TotalFn = ()
108 rnf TotalFn = ()
110 rnf PartialFn = ()
109 rnf PartialFn = ()
110+ rnf CoveringFn = ()
111 rnf Coinductive = ()
111 rnf Coinductive = ()
112 rnf AssertTotal = ()
112 rnf AssertTotal = ()
113 rnf Dictionary = ()
113 rnf Dictionary = ()
114 rnf Implicit = ()
114 rnf Implicit = ()
115+ rnf NoImplicit = ()
115 rnf (CExport x1) = rnf x1 `seq` ()
116 rnf (CExport x1) = rnf x1 `seq` ()
117+ rnf ErrorHandler = ()
118+ rnf ErrorReverse = ()
116 rnf Reflection = ()
119 rnf Reflection = ()
117 rnf (Specialise x1) = rnf x1 `seq` ()
120 rnf (Specialise x1) = rnf x1 `seq` ()
121+ rnf Constructor = ()
118
122
119instance NFData DataOpt where
123instance NFData DataOpt where
120 rnf Codata = ()
124 rnf Codata = ()
121 rnf DefaultEliminator = ()
125 rnf DefaultEliminator = ()
122 rnf DefaultCaseFun = ()
126 rnf DefaultCaseFun = ()
127+ rnf DataErrRev = ()
123
128
124instance (NFData t) => NFData (PDecl' t) where
129instance (NFData t) => NFData (PDecl' t) where
125 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
130 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
@@ -210,6 +215,7 @@ instance NFData PTerm where
210 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
215 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
211 rnf (PDPair x1 x2 x3 x4 x5)
216 rnf (PDPair x1 x2 x3 x4 x5)
212 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
217 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
218+ rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
213 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
219 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
214 rnf (PHidden x1) = rnf x1 `seq` ()
220 rnf (PHidden x1) = rnf x1 `seq` ()
215 rnf PType = ()
221 rnf PType = ()
@@ -227,8 +233,11 @@ instance NFData PTerm where
227 rnf (PElabError x1) = rnf x1 `seq` ()
233 rnf (PElabError x1) = rnf x1 `seq` ()
228 rnf PImpossible = ()
234 rnf PImpossible = ()
229 rnf (PCoerced x1) = rnf x1 `seq` ()
235 rnf (PCoerced x1) = rnf x1 `seq` ()
236+ rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
230 rnf (PUnifyLog x1) = rnf x1 `seq` ()
237 rnf (PUnifyLog x1) = rnf x1 `seq` ()
231 rnf (PNoImplicits x1) = rnf x1 `seq` ()
238 rnf (PNoImplicits x1) = rnf x1 `seq` ()
239+ rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
240+ rnf (PUnquote x1) = rnf x1 `seq` ()
232
241
233instance (NFData t) => NFData (PTactic' t) where
242instance (NFData t) => NFData (PTactic' t) where
234 rnf (Intro x1) = rnf x1 `seq` ()
243 rnf (Intro x1) = rnf x1 `seq` ()
@@ -236,6 +245,7 @@ instance (NFData t) => NFData (PTactic' t) where
236 rnf (Focus x1) = rnf x1 `seq` ()
245 rnf (Focus x1) = rnf x1 `seq` ()
237 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
246 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
238 rnf (Rewrite x1) = rnf x1 `seq` ()
247 rnf (Rewrite x1) = rnf x1 `seq` ()
248+ rnf DoUnify = ()
239 rnf (Induction x1) = rnf x1 `seq` ()
249 rnf (Induction x1) = rnf x1 `seq` ()
240 rnf (CaseTac x1) = rnf x1 `seq` ()
250 rnf (CaseTac x1) = rnf x1 `seq` ()
241 rnf (Equiv x1) = rnf x1 `seq` ()
251 rnf (Equiv x1) = rnf x1 `seq` ()
@@ -245,6 +255,7 @@ instance (NFData t) => NFData (PTactic' t) where
245 rnf (Exact x1) = rnf x1 `seq` ()
255 rnf (Exact x1) = rnf x1 `seq` ()
246 rnf Compute = ()
256 rnf Compute = ()
247 rnf Trivial = ()
257 rnf Trivial = ()
258+ rnf TCInstance = ()
248 rnf (ProofSearch r r1 r2 x1 x2)
259 rnf (ProofSearch r r1 r2 x1 x2)
249 = rnf x1 `seq` rnf x2 `seq` ()
260 = rnf x1 `seq` rnf x2 `seq` ()
250 rnf Solve = ()
261 rnf Solve = ()
@@ -255,11 +266,16 @@ instance (NFData t) => NFData (PTactic' t) where
255 rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
266 rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
256 rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
267 rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
257 rnf (ApplyTactic x1) = rnf x1 `seq` ()
268 rnf (ApplyTactic x1) = rnf x1 `seq` ()
269+ rnf (ByReflection x1) = rnf x1 `seq` ()
258 rnf (Reflect x1) = rnf x1 `seq` ()
270 rnf (Reflect x1) = rnf x1 `seq` ()
259 rnf (Fill x1) = rnf x1 `seq` ()
271 rnf (Fill x1) = rnf x1 `seq` ()
260 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
272 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
261 rnf Qed = ()
273 rnf Qed = ()
262 rnf Abandon = ()
274 rnf Abandon = ()
275+ rnf (TCheck x1) = rnf x1 `seq` ()
276+ rnf (TEval x1) = rnf x1 `seq` ()
277+ rnf (TDocStr x1) = x1 `seq` ()
278+ rnf (TSearch x1) = rnf x1 `seq` ()
263 rnf Skip = ()
279 rnf Skip = ()
264 rnf (TFail x1) = rnf x1 `seq` ()
280 rnf (TFail x1) = rnf x1 `seq` ()
265 rnf SourceFC = ()
281 rnf SourceFC = ()
src/Idris/IBC.hs+82−80
@@ -9,6 +9,7 @@ import Idris.Core.CaseTree
9import Idris.AbsSyntax
9import Idris.AbsSyntax
10import Idris.Imports
10import Idris.Imports
11import Idris.Error
11import Idris.Error
12+import Idris.DeepSeq
12import Idris.Delaborate
13import Idris.Delaborate
13import qualified Idris.Docstrings as D
14import qualified Idris.Docstrings as D
14import Idris.Docstrings (Docstring)
15import Idris.Docstrings (Docstring)
@@ -25,6 +26,7 @@ import qualified Data.Text as T
25import qualified Data.Set as S
26import qualified Data.Set as S
26
27
27import Control.Monad
28import Control.Monad
29+import Control.DeepSeq
28import Control.Monad.State.Strict hiding (get, put)
30import Control.Monad.State.Strict hiding (get, put)
29import qualified Control.Monad.State.Strict as ST
31import qualified Control.Monad.State.Strict as ST
30import System.FilePath
32import System.FilePath
@@ -37,44 +39,44 @@ ibcVersion = 90
37
39
38data IBCFile = IBCFile { ver :: Word8,
40data IBCFile = IBCFile { ver :: Word8,
39 sourcefile :: FilePath,
41 sourcefile :: FilePath,
40− symbols :: [Name],
42+ symbols :: ![Name],
41− ibc_imports :: [(Bool, FilePath)],
43+ ibc_imports :: ![(Bool, FilePath)],
42− ibc_importdirs :: [FilePath],
44+ ibc_importdirs :: ![FilePath],
43− ibc_implicits :: [(Name, [PArg])],
45+ ibc_implicits :: ![(Name, [PArg])],
44− ibc_fixes :: [FixDecl],
46+ ibc_fixes :: ![FixDecl],
45− ibc_statics :: [(Name, [Bool])],
47+ ibc_statics :: ![(Name, [Bool])],
46− ibc_classes :: [(Name, ClassInfo)],
48+ ibc_classes :: ![(Name, ClassInfo)],
47− ibc_instances :: [(Bool, Name, Name)],
49+ ibc_instances :: ![(Bool, Name, Name)],
48− ibc_dsls :: [(Name, DSL)],
50+ ibc_dsls :: ![(Name, DSL)],
49− ibc_datatypes :: [(Name, TypeInfo)],
51+ ibc_datatypes :: ![(Name, TypeInfo)],
50− ibc_optimise :: [(Name, OptInfo)],
52+ ibc_optimise :: ![(Name, OptInfo)],
51− ibc_syntax :: [Syntax],
53+ ibc_syntax :: ![Syntax],
52− ibc_keywords :: [String],
54+ ibc_keywords :: ![String],
53− ibc_objs :: [(Codegen, FilePath)],
55+ ibc_objs :: ![(Codegen, FilePath)],
54− ibc_libs :: [(Codegen, String)],
56+ ibc_libs :: ![(Codegen, String)],
55− ibc_cgflags :: [(Codegen, String)],
57+ ibc_cgflags :: ![(Codegen, String)],
56− ibc_dynamic_libs :: [String],
58+ ibc_dynamic_libs :: ![String],
57− ibc_hdrs :: [(Codegen, String)],
59+ ibc_hdrs :: ![(Codegen, String)],
58− ibc_access :: [(Name, Accessibility)],
60+ ibc_access :: ![(Name, Accessibility)],
59− ibc_total :: [(Name, Totality)],
61+ ibc_total :: ![(Name, Totality)],
60− ibc_totcheckfail :: [(FC, String)],
62+ ibc_totcheckfail :: ![(FC, String)],
61− ibc_flags :: [(Name, [FnOpt])],
63+ ibc_flags :: ![(Name, [FnOpt])],
62− ibc_fninfo :: [(Name, FnInfo)],
64+ ibc_fninfo :: ![(Name, FnInfo)],
63− ibc_cg :: [(Name, CGInfo)],
65+ ibc_cg :: ![(Name, CGInfo)],
64− ibc_defs :: [(Name, Def)],
66+ ibc_defs :: ![(Name, Def)],
65− ibc_docstrings :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],
67+ ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],
66− ibc_transforms :: [(Name, (Term, Term))],
68+ ibc_transforms :: ![(Name, (Term, Term))],
67− ibc_errRev :: [(Term, Term)],
69+ ibc_errRev :: ![(Term, Term)],
68− ibc_coercions :: [Name],
70+ ibc_coercions :: ![Name],
69− ibc_lineapps :: [(FilePath, Int, PTerm)],
71+ ibc_lineapps :: ![(FilePath, Int, PTerm)],
70− ibc_namehints :: [(Name, Name)],
72+ ibc_namehints :: ![(Name, Name)],
71− ibc_metainformation :: [(Name, MetaInformation)],
73+ ibc_metainformation :: ![(Name, MetaInformation)],
72− ibc_errorhandlers :: [Name],
74+ ibc_errorhandlers :: ![Name],
73− ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler
75+ ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
74− ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],
76+ ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],
75− ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],
77+ ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
76− ibc_postulates :: [Name],
78+ ibc_postulates :: ![Name],
77− ibc_parsedSpan :: Maybe FC
79+ ibc_parsedSpan :: !(Maybe FC)
78 }
80 }
79 deriving Show
81 deriving Show
80{-!
82{-!
@@ -189,11 +191,11 @@ ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
189ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
191ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
190ibc i (IBCDef n) f
192ibc i (IBCDef n) f
191 = do f' <- case lookupDefExact n (tt_ctxt i) of
193 = do f' <- case lookupDefExact n (tt_ctxt i) of
192− Just v -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
194+ Just v -> do -- (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
193− return f' { ibc_defs = (n,v) : ibc_defs f' }
195+ return f { ibc_defs = (n,v) : ibc_defs f }
194 _ -> ifail "IBC write failed"
196 _ -> ifail "IBC write failed"
195 case lookupCtxtExact n (idris_patdefs i) of
197 case lookupCtxtExact n (idris_patdefs i) of
196− Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f' }
198+ Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }
197 _ -> return f' -- Not a pattern definition
199 _ -> return f' -- Not a pattern definition
198 where
200 where
199 updateDef :: Def -> StateT (IBCFile, Int) Idris Def
201 updateDef :: Def -> StateT (IBCFile, Int) Idris Def
@@ -296,43 +298,43 @@ process reexp i fn
296 v <- verbose
298 v <- verbose
297 quiet <- getQuiet
299 quiet <- getQuiet
298-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
300-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
299− pImportDirs (ibc_importdirs i)
301+ pImportDirs $ force (ibc_importdirs i)
300− pImports (ibc_imports i)
302+ pImports $ force (ibc_imports i)
301− pImps (ibc_implicits i)
303+ pImps $ force (ibc_implicits i)
302− pFixes (ibc_fixes i)
304+ pFixes $ force (ibc_fixes i)
303− pStatics (ibc_statics i)
305+ pStatics $ force (ibc_statics i)
304− pClasses (ibc_classes i)
306+ pClasses $ force (ibc_classes i)
305− pInstances (ibc_instances i)
307+ pInstances $ force (ibc_instances i)
306− pDSLs (ibc_dsls i)
308+ pDSLs $ force (ibc_dsls i)
307− pDatatypes (ibc_datatypes i)
309+ pDatatypes $ force (ibc_datatypes i)
308− pOptimise (ibc_optimise i)
310+ pOptimise $ force (ibc_optimise i)
309− pSyntax (ibc_syntax i)
311+ pSyntax $ force (ibc_syntax i)
310− pKeywords (ibc_keywords i)
312+ pKeywords $ force (ibc_keywords i)
311− pObjs (ibc_objs i)
313+ pObjs $ force (ibc_objs i)
312− pLibs (ibc_libs i)
314+ pLibs $ force (ibc_libs i)
313− pCGFlags (ibc_cgflags i)
315+ pCGFlags $ force (ibc_cgflags i)
314− pDyLibs (ibc_dynamic_libs i)
316+ pDyLibs $ force (ibc_dynamic_libs i)
315− pHdrs (ibc_hdrs i)
317+ pHdrs $ force (ibc_hdrs i)
316− pDefs reexp (symbols i) (ibc_defs i)
318+ pDefs reexp (symbols i) $ force (ibc_defs i)
317− pPatdefs (ibc_patdefs i)
319+ pPatdefs $ force (ibc_patdefs i)
318− pAccess reexp (ibc_access i)
320+ pAccess reexp $ force (ibc_access i)
319− pFlags (ibc_flags i)
321+ pFlags $ force (ibc_flags i)
320− pFnInfo (ibc_fninfo i)
322+ pFnInfo $ force (ibc_fninfo i)
321− pTotal (ibc_total i)
323+ pTotal $ force (ibc_total i)
322− pTotCheckErr (ibc_totcheckfail i)
324+ pTotCheckErr $ force (ibc_totcheckfail i)
323− pCG (ibc_cg i)
325+ pCG $ force (ibc_cg i)
324− pDocs (ibc_docstrings i)
326+ pDocs $ force (ibc_docstrings i)
325− pCoercions (ibc_coercions i)
327+ pCoercions $ force (ibc_coercions i)
326− pTrans (ibc_transforms i)
328+ pTrans $ force (ibc_transforms i)
327− pErrRev (ibc_errRev i)
329+ pErrRev $ force (ibc_errRev i)
328− pLineApps (ibc_lineapps i)
330+ pLineApps $ force (ibc_lineapps i)
329− pNameHints (ibc_namehints i)
331+ pNameHints $ force (ibc_namehints i)
330− pMetaInformation (ibc_metainformation i)
332+ pMetaInformation $ force (ibc_metainformation i)
331− pErrorHandlers (ibc_errorhandlers i)
333+ pErrorHandlers $ force (ibc_errorhandlers i)
332− pFunctionErrorHandlers (ibc_function_errorhandlers i)
334+ pFunctionErrorHandlers $ force (ibc_function_errorhandlers i)
333− pMetavars (ibc_metavars i)
335+ pMetavars $ force (ibc_metavars i)
334− pPostulates (ibc_postulates i)
336+ pPostulates $ force (ibc_postulates i)
335− pParsedSpan (ibc_parsedSpan i)
337+ pParsedSpan $ force (ibc_parsedSpan i)
336
338
337timestampOlder :: FilePath -> FilePath -> Idris ()
339timestampOlder :: FilePath -> FilePath -> Idris ()
338timestampOlder src ibc = do srct <- runIO $ getModificationTime src
340timestampOlder src ibc = do srct <- runIO $ getModificationTime src
@@ -462,13 +464,13 @@ pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
462pPatdefs ds
464pPatdefs ds
463 = mapM_ (\ (n, d) ->
465 = mapM_ (\ (n, d) ->
464 do i <- getIState
466 do i <- getIState
465− putIState (i { idris_patdefs = addDef n d (idris_patdefs i) }))
467+ putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))
466 ds
468 ds
467
469
468pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
470pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
469pDefs reexp syms ds
471pDefs reexp syms ds
470 = mapM_ (\ (n, d) ->
472 = mapM_ (\ (n, d) ->
471− do let d' = updateDef d
473+ do let d' = force d -- (updateDef d)
472 case d' of
474 case d' of
473 TyDecl _ _ -> return ()
475 TyDecl _ _ -> return ()
474 _ -> do iLOG $ "SOLVING " ++ show n
476 _ -> do iLOG $ "SOLVING " ++ show n