2ec25c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Do more forcing in IBC

This seems to reduce memory leaks when reloading since some bits of laziness appeared to be retaining references to old states.

commit2ec25c2c3fdd73ae7b79ff8f0c71ccd8fe22d2ea authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 3 Jan 2015, 11:32 (12 years ago) parent0a8e3e3

7 files changed+242−99

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1 src/Idris/AbsSyntaxTree.hs+4 src/Idris/Core/DeepSeq.hs+103−1 src/Idris/Core/Evaluate.hs+18 src/Idris/Core/TT.hs+1−1 src/Idris/DeepSeq.hs+33−17 src/Idris/IBC.hs+82−80

src/Idris/AbsSyntax.hs+1

@@ -379,6 +379,7 @@ resetNameIdx = do i <- getIState

379379addNameIdx :: Name -> Idris (Int, Name)

380380addNameIdx n = do i <- getIState

381381 let (i', x) = addNameIdx' i n

382+ putIState i'

382383 return x

383384

384385addNameIdx' :: IState -> Name -> (IState, (Int, Name))

src/Idris/AbsSyntaxTree.hs+4

@@ -313,6 +313,9 @@ data Codegen = Via String

313313-- | ViaLLVM

314314 | Bytecode

315315 deriving (Show, Eq)

316+{-!

317+deriving instance NFData Codegen

318+!-}

316319

317320-- | REPL commands

318321data Command = Quit

@@ -944,6 +947,7 @@ data FnInfo = FnInfo { fn_params :: [Int] }

944947 deriving Show

945948{-!

946949deriving instance Binary FnInfo

950+deriving instance NFData FnInfo

947951!-}

948952

949953data 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 #-}

13module Idris.Core.DeepSeq where

35import Idris.Core.TT

46import Idris.Core.CaseTree

7+import Idris.Core.Evaluate

69import Control.DeepSeq

710

@@ -11,6 +14,7 @@ instance NFData Name where

1114 rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

1215 rnf NErased = ()

1316 rnf (SN x1) = rnf x1 `seq` ()

17+ rnf (SymRef x1) = rnf x1 `seq` ()

1418

1519instance NFData SpecialName where

1620 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -22,11 +26,17 @@ instance NFData SpecialName where

2226 rnf (ElimN x1) = rnf x1 `seq` ()

2327 rnf (InstanceCtorN x1) = rnf x1 `seq` ()

2428

29+instance NFData Universe where

30+ rnf NullType = ()

31+ rnf UniqueType = ()

32+ rnf AllTypes = ()

33+

2534instance NFData Raw where

2635 rnf (Var x1) = rnf x1 `seq` ()

2736 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

2837 rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

2938 rnf RType = ()

39+ rnf (RUType x1) = rnf x1 `seq` ()

3040 rnf (RForce x1) = rnf x1 `seq` ()

3141 rnf (RConstant x1) = x1 `seq` ()

3242

@@ -45,9 +55,20 @@ instance NFData Err where

4555 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

4656 rnf (UnifyScope x1 x2 x3 x4)

4757 = 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` ()

4860 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` ()

4968 rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

5069 rnf (CantIntroduce x1) = rnf x1 `seq` ()

70+ rnf (TooManyArguments x1) = rnf x1 `seq` ()

71+ rnf (WithFnType x1) = rnf x1 `seq` ()

5172 rnf (NoSuchVariable x1) = rnf x1 `seq` ()

5273 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

5374 rnf (NotInjective x1 x2 x3)

@@ -89,18 +110,99 @@ instance NFData NameType where

89110 rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

90111 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

91112

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+

92152instance (NFData n) => NFData (TT n) where

93153 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

94154 rnf (V x1) = rnf x1 `seq` ()

95155 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

96156 rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

97− rnf (Constant x1) = x1 `seq` ()

157+ rnf (Constant x1) = rnf x1 `seq` ()

98158 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

99159 rnf Erased = ()

100160 rnf Impossible = ()

101161 rnf (TType x1) = rnf x1 `seq` ()

102162 rnf (UType _) = ()

103163

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+

104206instance (NFData t) => NFData (SC' t) where

105207 rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

106208 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Core/Evaluate.hs+18

@@ -692,6 +692,15 @@ deriving instance Binary CaseInfo

692692{-!

693693deriving instance Binary CaseDefs

694694!-}

695+{-!

696+deriving instance NFData Def

697+!-}

698+{-!

699+deriving instance NFData CaseInfo

700+!-}

701+{-!

702+deriving instance NFData CaseDefs

703+!-}

695704

696705instance Show Def where

697706 show (Function ty tm) = "Function: " ++ show (ty, tm)

@@ -717,6 +726,9 @@ instance Show Def where

717726

718727data Accessibility = Public | Frozen | Hidden

719728 deriving (Show, Eq)

729+{-!

730+deriving instance NFData Accessibility

731+!-}

720732

721733-- | The result of totality checking

722734data Totality = Total [Int] -- ^ well-founded arguments

@@ -724,11 +736,17 @@ data Totality = Total [Int] -- ^ well-founded arguments

724736 | Partial PReason

725737 | Unchecked

726738 deriving Eq

739+{-!

740+deriving instance NFData Totality

741+!-}

727742

728743-- | Reasons why a function may not be total

729744data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

730745 | ExternalIO | BelieveMe | Mutual [Name] | NotProductive

731746 deriving (Show, Eq)

747+{-!

748+deriving instance NFData PReason

749+!-}

732750

733751instance Show Totality where

734752 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"

src/Idris/Core/TT.hs+1−1

@@ -241,7 +241,7 @@ score _ = 0

241241instance Show Err where

242242 show (Msg s) = s

243243 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 ++ " " ++

245245 show l ++ " " ++ show r ++ " " ++

246246 show e ++ " in " ++ show sc ++ " " ++ show i

247247 show (CantSolveGoal g _) = "CantSolve " ++ show g

src/Idris/DeepSeq.hs+33−17

@@ -1,6 +1,9 @@

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

13module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

35import Idris.Core.DeepSeq

6+import Idris.Docstrings

47import Idris.Core.TT

58import Idris.AbsSyntaxTree

@@ -48,24 +51,13 @@ instance NFData CT.NumWrapper where

4851 rnf CT.PeriodFollowing = ()

4952 rnf CT.ParenFollowing = ()

5053

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` ()

5259

53−instance NFData IntTy where

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 = ()

60+-- All generated by 'derive'

6961

7062instance NFData SizeChange where

7163 rnf Smaller = ()

@@ -73,6 +65,13 @@ instance NFData SizeChange where

7365 rnf Bigger = ()

7466 rnf Unknown = ()

7567

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+

7675instance NFData CGInfo where

7776 rnf (CGInfo x1 x2 x3 x4 x5)

7877 = rnf x1 `seq`

@@ -108,18 +107,24 @@ instance NFData FnOpt where

108107 rnf Inlinable = ()

109108 rnf TotalFn = ()

110109 rnf PartialFn = ()

110+ rnf CoveringFn = ()

111111 rnf Coinductive = ()

112112 rnf AssertTotal = ()

113113 rnf Dictionary = ()

114114 rnf Implicit = ()

115+ rnf NoImplicit = ()

115116 rnf (CExport x1) = rnf x1 `seq` ()

117+ rnf ErrorHandler = ()

118+ rnf ErrorReverse = ()

116119 rnf Reflection = ()

117120 rnf (Specialise x1) = rnf x1 `seq` ()

121+ rnf Constructor = ()

118122

119123instance NFData DataOpt where

120124 rnf Codata = ()

121125 rnf DefaultEliminator = ()

122126 rnf DefaultCaseFun = ()

127+ rnf DataErrRev = ()

123128

124129instance (NFData t) => NFData (PDecl' t) where

125130 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -210,6 +215,7 @@ instance NFData PTerm where

210215 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

211216 rnf (PDPair x1 x2 x3 x4 x5)

212217 = 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` ()

213219 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

214220 rnf (PHidden x1) = rnf x1 `seq` ()

215221 rnf PType = ()

@@ -227,8 +233,11 @@ instance NFData PTerm where

227233 rnf (PElabError x1) = rnf x1 `seq` ()

228234 rnf PImpossible = ()

229235 rnf (PCoerced x1) = rnf x1 `seq` ()

236+ rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

230237 rnf (PUnifyLog x1) = rnf x1 `seq` ()

231238 rnf (PNoImplicits x1) = rnf x1 `seq` ()

239+ rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

240+ rnf (PUnquote x1) = rnf x1 `seq` ()

232241

233242instance (NFData t) => NFData (PTactic' t) where

234243 rnf (Intro x1) = rnf x1 `seq` ()

@@ -236,6 +245,7 @@ instance (NFData t) => NFData (PTactic' t) where

236245 rnf (Focus x1) = rnf x1 `seq` ()

237246 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

238247 rnf (Rewrite x1) = rnf x1 `seq` ()

248+ rnf DoUnify = ()

239249 rnf (Induction x1) = rnf x1 `seq` ()

240250 rnf (CaseTac x1) = rnf x1 `seq` ()

241251 rnf (Equiv x1) = rnf x1 `seq` ()

@@ -245,6 +255,7 @@ instance (NFData t) => NFData (PTactic' t) where

245255 rnf (Exact x1) = rnf x1 `seq` ()

246256 rnf Compute = ()

247257 rnf Trivial = ()

258+ rnf TCInstance = ()

248259 rnf (ProofSearch r r1 r2 x1 x2)

249260 = rnf x1 `seq` rnf x2 `seq` ()

250261 rnf Solve = ()

@@ -255,11 +266,16 @@ instance (NFData t) => NFData (PTactic' t) where

255266 rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

256267 rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

257268 rnf (ApplyTactic x1) = rnf x1 `seq` ()

269+ rnf (ByReflection x1) = rnf x1 `seq` ()

258270 rnf (Reflect x1) = rnf x1 `seq` ()

259271 rnf (Fill x1) = rnf x1 `seq` ()

260272 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

261273 rnf Qed = ()

262274 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` ()

263279 rnf Skip = ()

264280 rnf (TFail x1) = rnf x1 `seq` ()

265281 rnf SourceFC = ()

src/Idris/IBC.hs+82−80

@@ -9,6 +9,7 @@ import Idris.Core.CaseTree

99import Idris.AbsSyntax

1010import Idris.Imports

1111import Idris.Error

12+import Idris.DeepSeq

1213import Idris.Delaborate

1314import qualified Idris.Docstrings as D

1415import Idris.Docstrings (Docstring)

@@ -25,6 +26,7 @@ import qualified Data.Text as T

2526import qualified Data.Set as S

2627

2728import Control.Monad

29+import Control.DeepSeq

2830import Control.Monad.State.Strict hiding (get, put)

2931import qualified Control.Monad.State.Strict as ST

3032import System.FilePath

@@ -37,44 +39,44 @@ ibcVersion = 90

3739

3840data IBCFile = IBCFile { ver :: Word8,

3941 sourcefile :: FilePath,

40− symbols :: [Name],

41− ibc_imports :: [(Bool, FilePath)],

42− ibc_importdirs :: [FilePath],

43− ibc_implicits :: [(Name, [PArg])],

44− ibc_fixes :: [FixDecl],

45− ibc_statics :: [(Name, [Bool])],

46− ibc_classes :: [(Name, ClassInfo)],

47− ibc_instances :: [(Bool, Name, Name)],

48− ibc_dsls :: [(Name, DSL)],

49− ibc_datatypes :: [(Name, TypeInfo)],

50− ibc_optimise :: [(Name, OptInfo)],

51− ibc_syntax :: [Syntax],

52− ibc_keywords :: [String],

53− ibc_objs :: [(Codegen, FilePath)],

54− ibc_libs :: [(Codegen, String)],

55− ibc_cgflags :: [(Codegen, String)],

56− ibc_dynamic_libs :: [String],

57− ibc_hdrs :: [(Codegen, String)],

58− ibc_access :: [(Name, Accessibility)],

59− ibc_total :: [(Name, Totality)],

60− ibc_totcheckfail :: [(FC, String)],

61− ibc_flags :: [(Name, [FnOpt])],

62− ibc_fninfo :: [(Name, FnInfo)],

63− ibc_cg :: [(Name, CGInfo)],

64− ibc_defs :: [(Name, Def)],

65− ibc_docstrings :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

66− ibc_transforms :: [(Name, (Term, Term))],

67− ibc_errRev :: [(Term, Term)],

68− ibc_coercions :: [Name],

69− ibc_lineapps :: [(FilePath, Int, PTerm)],

70− ibc_namehints :: [(Name, Name)],

71− ibc_metainformation :: [(Name, MetaInformation)],

72− ibc_errorhandlers :: [Name],

73− ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

74− ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

75− ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],

76− ibc_postulates :: [Name],

77− ibc_parsedSpan :: Maybe FC

42+ symbols :: ![Name],

43+ ibc_imports :: ![(Bool, FilePath)],

44+ ibc_importdirs :: ![FilePath],

45+ ibc_implicits :: ![(Name, [PArg])],

46+ ibc_fixes :: ![FixDecl],

47+ ibc_statics :: ![(Name, [Bool])],

48+ ibc_classes :: ![(Name, ClassInfo)],

49+ ibc_instances :: ![(Bool, Name, Name)],

50+ ibc_dsls :: ![(Name, DSL)],

51+ ibc_datatypes :: ![(Name, TypeInfo)],

52+ ibc_optimise :: ![(Name, OptInfo)],

53+ ibc_syntax :: ![Syntax],

54+ ibc_keywords :: ![String],

55+ ibc_objs :: ![(Codegen, FilePath)],

56+ ibc_libs :: ![(Codegen, String)],

57+ ibc_cgflags :: ![(Codegen, String)],

58+ ibc_dynamic_libs :: ![String],

59+ ibc_hdrs :: ![(Codegen, String)],

60+ ibc_access :: ![(Name, Accessibility)],

61+ ibc_total :: ![(Name, Totality)],

62+ ibc_totcheckfail :: ![(FC, String)],

63+ ibc_flags :: ![(Name, [FnOpt])],

64+ ibc_fninfo :: ![(Name, FnInfo)],

65+ ibc_cg :: ![(Name, CGInfo)],

66+ ibc_defs :: ![(Name, Def)],

67+ ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

68+ ibc_transforms :: ![(Name, (Term, Term))],

69+ ibc_errRev :: ![(Term, Term)],

70+ ibc_coercions :: ![Name],

71+ ibc_lineapps :: ![(FilePath, Int, PTerm)],

72+ ibc_namehints :: ![(Name, Name)],

73+ ibc_metainformation :: ![(Name, MetaInformation)],

74+ ibc_errorhandlers :: ![Name],

75+ ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

76+ ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],

77+ ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

78+ ibc_postulates :: ![Name],

79+ ibc_parsedSpan :: !(Maybe FC)

7880 }

7981 deriving Show

8082{-!

@@ -189,11 +191,11 @@ ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

189191ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

190192ibc i (IBCDef n) f

191193 = do f' <- case lookupDefExact n (tt_ctxt i) of

192− Just v -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

193− return f' { ibc_defs = (n,v) : ibc_defs f' }

194+ Just v -> do -- (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

195+ return f { ibc_defs = (n,v) : ibc_defs f }

194196 _ -> ifail "IBC write failed"

195197 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 }

197199 _ -> return f' -- Not a pattern definition

198200 where

199201 updateDef :: Def -> StateT (IBCFile, Int) Idris Def

@@ -296,43 +298,43 @@ process reexp i fn

296298 v <- verbose

297299 quiet <- getQuiet

298300-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

299− pImportDirs (ibc_importdirs i)

300− pImports (ibc_imports i)

301− pImps (ibc_implicits i)

302− pFixes (ibc_fixes i)

303− pStatics (ibc_statics i)

304− pClasses (ibc_classes i)

305− pInstances (ibc_instances i)

306− pDSLs (ibc_dsls i)

307− pDatatypes (ibc_datatypes i)

308− pOptimise (ibc_optimise i)

309− pSyntax (ibc_syntax i)

310− pKeywords (ibc_keywords i)

311− pObjs (ibc_objs i)

312− pLibs (ibc_libs i)

313− pCGFlags (ibc_cgflags i)

314− pDyLibs (ibc_dynamic_libs i)

315− pHdrs (ibc_hdrs i)

316− pDefs reexp (symbols i) (ibc_defs i)

317− pPatdefs (ibc_patdefs i)

318− pAccess reexp (ibc_access i)

319− pFlags (ibc_flags i)

320− pFnInfo (ibc_fninfo i)

321− pTotal (ibc_total i)

322− pTotCheckErr (ibc_totcheckfail i)

323− pCG (ibc_cg i)

324− pDocs (ibc_docstrings i)

325− pCoercions (ibc_coercions i)

326− pTrans (ibc_transforms i)

327− pErrRev (ibc_errRev i)

328− pLineApps (ibc_lineapps i)

329− pNameHints (ibc_namehints i)

330− pMetaInformation (ibc_metainformation i)

331− pErrorHandlers (ibc_errorhandlers i)

332− pFunctionErrorHandlers (ibc_function_errorhandlers i)

333− pMetavars (ibc_metavars i)

334− pPostulates (ibc_postulates i)

335− pParsedSpan (ibc_parsedSpan i)

301+ pImportDirs $ force (ibc_importdirs i)

302+ pImports $ force (ibc_imports i)

303+ pImps $ force (ibc_implicits i)

304+ pFixes $ force (ibc_fixes i)

305+ pStatics $ force (ibc_statics i)

306+ pClasses $ force (ibc_classes i)

307+ pInstances $ force (ibc_instances i)

308+ pDSLs $ force (ibc_dsls i)

309+ pDatatypes $ force (ibc_datatypes i)

310+ pOptimise $ force (ibc_optimise i)

311+ pSyntax $ force (ibc_syntax i)

312+ pKeywords $ force (ibc_keywords i)

313+ pObjs $ force (ibc_objs i)

314+ pLibs $ force (ibc_libs i)

315+ pCGFlags $ force (ibc_cgflags i)

316+ pDyLibs $ force (ibc_dynamic_libs i)

317+ pHdrs $ force (ibc_hdrs i)

318+ pDefs reexp (symbols i) $ force (ibc_defs i)

319+ pPatdefs $ force (ibc_patdefs i)

320+ pAccess reexp $ force (ibc_access i)

321+ pFlags $ force (ibc_flags i)

322+ pFnInfo $ force (ibc_fninfo i)

323+ pTotal $ force (ibc_total i)

324+ pTotCheckErr $ force (ibc_totcheckfail i)

325+ pCG $ force (ibc_cg i)

326+ pDocs $ force (ibc_docstrings i)

327+ pCoercions $ force (ibc_coercions i)

328+ pTrans $ force (ibc_transforms i)

329+ pErrRev $ force (ibc_errRev i)

330+ pLineApps $ force (ibc_lineapps i)

331+ pNameHints $ force (ibc_namehints i)

332+ pMetaInformation $ force (ibc_metainformation i)

333+ pErrorHandlers $ force (ibc_errorhandlers i)

334+ pFunctionErrorHandlers $ force (ibc_function_errorhandlers i)

335+ pMetavars $ force (ibc_metavars i)

336+ pPostulates $ force (ibc_postulates i)

337+ pParsedSpan $ force (ibc_parsedSpan i)

336338

337339timestampOlder :: FilePath -> FilePath -> Idris ()

338340timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -462,13 +464,13 @@ pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

462464pPatdefs ds

463465 = mapM_ (\ (n, d) ->

464466 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) }))

466468 ds

467469

468470pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

469471pDefs reexp syms ds

470472 = mapM_ (\ (n, d) ->

471− do let d' = updateDef d

473+ do let d' = force d -- (updateDef d)

472474 case d' of

473475 TyDecl _ _ -> return ()

474476 _ -> do iLOG $ "SOLVING " ++ show n