543cd7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Strictness improvements

Add 'NFData' instances (autogenerated using 'derive') to force complete evaluation. Also make the context and case trees strict, since they need to be evaluated fully when writing out the intermediate file. Fixes #559

commit543cd7ea30e970a9ecee266f42ee758e7b1aeaa7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Nov 2013, 10:02 (13 years ago) parent7041f65

8 files changed+457−24

compare with master

unifiedsplit

idris.cabal+2 src/Core/CaseTree.hs+7−7 src/Core/Evaluate.hs+11−11 src/Core/TT.hs+19 src/Idris/AbsSyntaxTree.hs+23 src/Idris/DeepSeq.hs+385 src/Idris/ElabDecls.hs+5−3 src/Idris/REPL.hs+5−3

idris.cabal+2

@@ -324,6 +324,7 @@ Executable idris

324324 , Idris.Coverage

325325 , Idris.DSL

326326 , Idris.DataOpts

327+ , Idris.DeepSeq

327328 , Idris.Delaborate

328329 , Idris.Docs

329330 , Idris.ElabDecls

@@ -406,6 +407,7 @@ Executable idris

406407 , vector-binary-instances

407408 , network

408409 , xml

410+ , deepseq

409411

410412 Extensions: MultiParamTypeClasses

411413 , FunctionalDependencies

src/Core/CaseTree.hs+7−7

@@ -11,12 +11,12 @@ import Data.Maybe

1111import Data.List hiding (partition)

1212import Debug.Trace

1313

14−data CaseDef = CaseDef [Name] SC [Term]

14+data CaseDef = CaseDef [Name] !SC [Term]

1515 deriving Show

1616

1717data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

1818 | ProjCase t [CaseAlt' t] -- ^ special case for projections

19− | STerm t

19+ | STerm !t

2020 | UnmatchedCase String -- ^ error message

2121 | ImpossibleCase -- ^ already checked to be impossible

2222 deriving (Eq, Ord, Functor)

@@ -26,11 +26,11 @@ deriving instance Binary SC

2626

2727type SC = SC' Term

2828

29−data CaseAlt' t = ConCase Name Int [Name] (SC' t)

30− | FnCase Name [Name] (SC' t) -- ^ reflection function

31− | ConstCase Const (SC' t)

32− | SucCase Name (SC' t)

33− | DefaultCase (SC' t)

29+data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

30+ | FnCase Name [Name] !(SC' t) -- ^ reflection function

31+ | ConstCase Const !(SC' t)

32+ | SucCase Name !(SC' t)

33+ | DefaultCase !(SC' t)

3434 deriving (Show, Eq, Ord, Functor)

3535{-!

3636deriving instance Binary CaseAlt

src/Core/Evaluate.hs+11−11

@@ -580,22 +580,22 @@ spec ctxt statics genv tm = error "spec undefined"

580580 An Operator is a function which explains how to reduce.

581581 A CaseOp is a function defined by a simple case tree -}

582582

583−data Def = Function Type Term

584− | TyDecl NameType Type

583+data Def = Function !Type !Term

584+ | TyDecl NameType !Type

585585 | Operator Type Int ([Value] -> Maybe Value)

586586 | CaseOp CaseInfo

587− Type

588− [Either Term (Term, Term)] -- original definition

589− [([Name], Term, Term)] -- simplified for totality check definition

590− CaseDefs

587+ !Type

588+ ![Either Term (Term, Term)] -- original definition

589+ ![([Name], Term, Term)] -- simplified for totality check definition

590+ !CaseDefs

591591-- [Name] SC -- Compile time case definition

592592-- [Name] SC -- Run time cae definitions

593593

594594data CaseDefs = CaseDefs {

595− cases_totcheck :: ([Name], SC),

596− cases_compiletime :: ([Name], SC),

597− cases_inlined :: ([Name], SC),

598− cases_runtime :: ([Name], SC)

595+ cases_totcheck :: !([Name], SC),

596+ cases_compiletime :: !([Name], SC),

597+ cases_inlined :: !([Name], SC),

598+ cases_runtime :: !([Name], SC)

599599 }

600600

601601data CaseInfo = CaseInfo {

@@ -719,7 +719,7 @@ setTotal n t uctxt

719719

720720addCtxtDef :: Name -> Def -> Context -> Context

721721addCtxtDef n d c = let ctxt = definitions c

722− ctxt' = addDef n (d, Public, Unchecked) ctxt in

722+ ctxt' = addDef n (d, Public, Unchecked) $! ctxt in

723723 c { definitions = ctxt' }

724724

725725addTyDecl :: Name -> NameType -> Type -> Context -> Context

src/Core/TT.hs+19

@@ -65,6 +65,7 @@ fileFC s = FC s 0 0

6565

6666{-!

6767deriving instance Binary FC

68+deriving instance NFData FC

6869!-}

6970

7071instance Sized FC where

@@ -103,6 +104,9 @@ data Err = Msg String

103104 | ProviderError String

104105 | LoadingFailed String Err

105106 deriving Eq

107+{-!

108+deriving instance NFData Err

109+!-}

106110

107111instance Sized Err where

108112 size (Msg msg) = length msg

@@ -225,6 +229,7 @@ data Name = UN String -- ^ User-provided name

225229 deriving (Eq, Ord)

226230{-!

227231deriving instance Binary Name

232+deriving instance NFData Name

228233!-}

229234

230235data SpecialName = WhereN Int Name Name

@@ -235,6 +240,7 @@ data SpecialName = WhereN Int Name Name

235240 deriving (Eq, Ord)

236241{-!

237242deriving instance Binary SpecialName

243+deriving instance NFData SpecialName

238244!-}

239245

240246instance Sized Name where

@@ -369,6 +375,11 @@ data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

369375

370376data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

371377 deriving (Show, Eq, Ord)

378+{-!

379+deriving instance NFData IntTy

380+deriving instance NFData NativeTy

381+deriving instance NFData ArithTy

382+!-}

372383

373384instance Pretty ArithTy where

374385 pretty (ATInt ITNative) = text "Int"

@@ -400,6 +411,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

400411 deriving (Eq, Ord)

401412{-!

402413deriving instance Binary Const

414+deriving instance NFData Const

403415!-}

404416

405417instance Sized Const where

@@ -442,6 +454,7 @@ instance Pretty Raw where

442454

443455{-!

444456deriving instance Binary Raw

457+deriving instance NFData Raw

445458!-}

446459

447460-- | All binding forms are represented in a unform fashion.

@@ -461,6 +474,7 @@ data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}

461474 deriving (Show, Eq, Ord, Functor)

462475{-!

463476deriving instance Binary Binder

477+deriving instance NFData Binder

464478!-}

465479

466480instance Sized a => Sized (Binder a) where

@@ -515,6 +529,9 @@ type RProgram = [(Name, RDef)]

515529data UExp = UVar Int -- ^ universe variable

516530 | UVal Int -- ^ explicit universe level

517531 deriving (Eq, Ord)

532+{-!

533+deriving instance NFData UExp

534+!-}

518535

519536instance Sized UExp where

520537 size _ = 1

@@ -551,6 +568,7 @@ data NameType = Bound

551568 deriving (Show, Ord)

552569{-!

553570deriving instance Binary NameType

571+deriving instance NFData NameType

554572!-}

555573

556574instance Sized NameType where

@@ -580,6 +598,7 @@ data TT n = P NameType n (TT n) -- ^ named references

580598 deriving (Ord, Functor)

581599{-!

582600deriving instance Binary TT

601+deriving instance NFData TT

583602!-}

584603

585604class TermSize a where

src/Idris/AbsSyntaxTree.hs+23

@@ -134,6 +134,7 @@ data SizeChange = Smaller | Same | Bigger | Unknown

134134 deriving (Show, Eq)

135135{-!

136136deriving instance Binary SizeChange

137+deriving instance NFData SizeChange

137138!-}

138139

139140type SCGEntry = (Name, [Maybe (Int, SizeChange)])

@@ -146,6 +147,7 @@ data CGInfo = CGInfo { argsdef :: [Name],

146147 deriving Show

147148{-!

148149deriving instance Binary CGInfo

150+deriving instance NFData CGInfo

149151!-}

150152

151153primDefs = [UN "unsafePerformPrimIO",

@@ -301,6 +303,7 @@ data Fixity = Infixl { prec :: Int }

301303 deriving Eq

302304{-!

303305deriving instance Binary Fixity

306+deriving instance NFData Fixity

304307!-}

305308

306309instance Show Fixity where

@@ -317,6 +320,7 @@ instance Show FixDecl where

317320

318321{-!

319322deriving instance Binary FixDecl

323+deriving instance NFData FixDecl

320324!-}

321325

322326instance Ord FixDecl where

@@ -327,6 +331,7 @@ data Static = Static | Dynamic

327331 deriving (Show, Eq)

328332{-!

329333deriving instance Binary Static

334+deriving instance NFData Static

330335!-}

331336

332337-- Mark bindings with their explicitness, and laziness

@@ -349,6 +354,7 @@ data Plicity = Imp { plazy :: Bool,

349354

350355{-!

351356deriving instance Binary Plicity

357+deriving instance NFData Plicity

352358!-}

353359

354360impl = Imp False Dynamic "" False

@@ -369,6 +375,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

369375 deriving (Show, Eq)

370376{-!

371377deriving instance Binary FnOpt

378+deriving instance NFData FnOpt

372379!-}

373380

374381type FnOpts = [FnOpt]

@@ -416,6 +423,7 @@ data PDecl' t

416423 deriving Functor

417424{-!

418425deriving instance Binary PDecl'

426+deriving instance NFData PDecl'

419427!-}

420428

421429-- For elaborator state

@@ -438,6 +446,7 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level de

438446 deriving Functor

439447{-!

440448deriving instance Binary PClause'

449+deriving instance NFData PClause'

441450!-}

442451

443452-- | Data declaration

@@ -451,6 +460,7 @@ data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

451460 deriving Functor

452461{-!

453462deriving instance Binary PData'

463+deriving instance NFData PData'

454464!-}

455465

456466-- Handy to get a free function for applying PTerm -> PTerm functions

@@ -581,6 +591,7 @@ data PTerm = PQuote Raw

581591

582592{-!

583593deriving instance Binary PTerm

594+deriving instance NFData PTerm

584595!-}

585596

586597mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

@@ -628,6 +639,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

628639 deriving (Show, Eq, Functor)

629640{-!

630641deriving instance Binary PTactic'

642+deriving instance NFData PTactic'

631643!-}

632644

633645instance Sized a => Sized (PTactic' a) where

@@ -663,6 +675,7 @@ data PDo' t = DoExp FC t

663675 deriving (Eq, Functor)

664676{-!

665677deriving instance Binary PDo'

678+deriving instance NFData PDo'

666679!-}

667680

668681instance Sized a => Sized (PDo' a) where

@@ -703,6 +716,7 @@ instance Sized a => Sized (PArg' a) where

703716

704717{-!

705718deriving instance Binary PArg'

719+deriving instance NFData PArg'

706720!-}

707721

708722pimp n t mach = PImp 1 mach True n t ""

@@ -722,6 +736,7 @@ data ClassInfo = CI { instanceName :: Name,

722736 deriving Show

723737{-!

724738deriving instance Binary ClassInfo

739+deriving instance NFData ClassInfo

725740!-}

726741

727742data OptInfo = Optimise { collapsible :: Bool,

@@ -731,6 +746,7 @@ data OptInfo = Optimise { collapsible :: Bool,

731746 deriving Show

732747{-!

733748deriving instance Binary OptInfo

749+deriving instance NFData OptInfo

734750!-}

735751

736752

@@ -740,6 +756,7 @@ data TypeInfo = TI { con_names :: [Name],

740756 deriving Show

741757{-!

742758deriving instance Binary TypeInfo

759+deriving instance NFData TypeInfo

743760!-}

744761

745762-- Syntactic sugar info

@@ -757,6 +774,7 @@ data DSL' t = DSL { dsl_bind :: t,

757774 deriving (Show, Functor)

758775{-!

759776deriving instance Binary DSL'

777+deriving instance NFData DSL'

760778!-}

761779

762780type DSL = DSL' PTerm

@@ -765,12 +783,14 @@ data SynContext = PatternSyntax | TermSyntax | AnySyntax

765783 deriving Show

766784{-!

767785deriving instance Binary SynContext

786+deriving instance NFData SynContext

768787!-}

769788

770789data Syntax = Rule [SSymbol] PTerm SynContext

771790 deriving Show

772791{-!

773792deriving instance Binary Syntax

793+deriving instance NFData Syntax

774794!-}

775795

776796data SSymbol = Keyword Name

@@ -781,6 +801,7 @@ data SSymbol = Keyword Name

781801 deriving Show

782802{-!

783803deriving instance Binary SSymbol

804+deriving instance NFData SSymbol

784805!-}

785806

786807initDSL = DSL (PRef f (UN ">>="))

@@ -799,6 +820,7 @@ data Using = UImplicit Name PTerm

799820 deriving (Show, Eq)

800821{-!

801822deriving instance Binary Using

823+deriving instance NFData Using

802824!-}

803825

804826data SyntaxInfo = Syn { using :: [Using],

@@ -811,6 +833,7 @@ data SyntaxInfo = Syn { using :: [Using],

811833 dsl_info :: DSL }

812834 deriving Show

813835{-!

836+deriving instance NFData SyntaxInfo

814837deriving instance Binary SyntaxInfo

815838!-}

816839

src/Idris/DeepSeq.hsnew file+385

@@ -0,0 +1,385 @@

1+module Idris.DeepSeq where

3+import Core.TT

4+import Idris.AbsSyntax

6+import Control.DeepSeq

8+-- All generated by 'derive'

10+instance NFData Raw where

11+ rnf (Var x1) = rnf x1 `seq` ()

12+ rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

13+ rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

14+ rnf RType = ()

15+ rnf (RForce x1) = rnf x1 `seq` ()

16+ rnf (RConstant x1) = rnf x1 `seq` ()

17+

18+instance NFData FC where

19+ rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

20+

21+instance NFData Name where

22+ rnf (UN x1) = rnf x1 `seq` ()

23+ rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

24+ rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

25+ rnf NErased = ()

26+ rnf (SN x1) = rnf x1 `seq` ()

27+

28+instance NFData SpecialName where

29+ rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

30+ rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

31+ rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

32+ rnf (MethodN x1) = rnf x1 `seq` ()

33+ rnf (CaseN x1) = rnf x1 `seq` ()

34+

35+instance NFData Const where

36+ rnf (I x1) = rnf x1 `seq` ()

37+ rnf (BI x1) = rnf x1 `seq` ()

38+ rnf (Fl x1) = rnf x1 `seq` ()

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

40+ rnf (Str x1) = rnf x1 `seq` ()

41+ rnf (B8 x1) = rnf x1 `seq` ()

42+ rnf (B16 x1) = rnf x1 `seq` ()

43+ rnf (B32 x1) = rnf x1 `seq` ()

44+ rnf (B64 x1) = rnf x1 `seq` ()

45+ rnf (B8V x1) = rnf x1 `seq` ()

46+ rnf (B16V x1) = rnf x1 `seq` ()

47+ rnf (B32V x1) = rnf x1 `seq` ()

48+ rnf (B64V x1) = rnf x1 `seq` ()

49+ rnf (AType x1) = rnf x1 `seq` ()

50+ rnf StrType = ()

51+ rnf PtrType = ()

52+ rnf VoidType = ()

53+ rnf Forgot = ()

54+

55+instance NFData IntTy where

56+ rnf (ITFixed x1) = rnf x1 `seq` ()

57+ rnf ITNative = ()

58+ rnf ITBig = ()

59+ rnf ITChar = ()

60+ rnf (ITVec x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

61+

62+

63+instance NFData NativeTy where

64+ rnf IT8 = ()

65+ rnf IT16 = ()

66+ rnf IT32 = ()

67+ rnf IT64 = ()

68+

69+

70+instance NFData ArithTy where

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

72+ rnf ATFloat = ()

73+

74+instance NFData Err where

75+ rnf (Msg x1) = rnf x1 `seq` ()

76+ rnf (InternalMsg x1) = rnf x1 `seq` ()

77+ rnf (CantUnify x1 x2 x3 x4 x5 x6)

78+ = rnf x1 `seq`

79+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

80+ rnf (InfiniteUnify x1 x2 x3)

81+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

82+ rnf (CantConvert x1 x2 x3)

83+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

84+ rnf (UnifyScope x1 x2 x3 x4)

85+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

86+ rnf (CantInferType x1) = rnf x1 `seq` ()

87+ rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

88+ rnf (CantIntroduce x1) = rnf x1 `seq` ()

89+ rnf (NoSuchVariable x1) = rnf x1 `seq` ()

90+ rnf (NoTypeDecl x1) = rnf x1 `seq` ()

91+ rnf (NotInjective x1 x2 x3)

92+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

93+ rnf (CantResolve x1) = rnf x1 `seq` ()

94+ rnf (CantResolveAlts x1) = rnf x1 `seq` ()

95+ rnf (IncompleteTerm x1) = rnf x1 `seq` ()

96+ rnf UniverseError = ()

97+ rnf ProgramLineComment = ()

98+ rnf (Inaccessible x1) = rnf x1 `seq` ()

99+ rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

100+ rnf (AlreadyDefined x1) = rnf x1 `seq` ()

101+ rnf (ProofSearchFail x1) = rnf x1 `seq` ()

102+ rnf (NoRewriting x1) = rnf x1 `seq` ()

103+ rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104+ rnf (Elaborating x1 x2 x3)

105+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

106+ rnf (ProviderError x1) = rnf x1 `seq` ()

107+ rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

108+

109+instance (NFData b) => NFData (Binder b) where

110+ rnf (Lam x1) = rnf x1 `seq` ()

111+ rnf (Pi x1) = rnf x1 `seq` ()

112+ rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

113+ rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

114+ rnf (Hole x1) = rnf x1 `seq` ()

115+ rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

116+ rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

117+ rnf (PVar x1) = rnf x1 `seq` ()

118+ rnf (PVTy x1) = rnf x1 `seq` ()

119+

120+instance NFData UExp where

121+ rnf (UVar x1) = rnf x1 `seq` ()

122+ rnf (UVal x1) = rnf x1 `seq` ()

123+

124+instance NFData NameType where

125+ rnf Bound = ()

126+ rnf Ref = ()

127+ rnf (DCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

128+ rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

129+

130+instance (NFData n) => NFData (TT n) where

131+ rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

132+ rnf (V x1) = rnf x1 `seq` ()

133+ rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

134+ rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

136+ rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

137+ rnf Erased = ()

138+ rnf Impossible = ()

139+ rnf (TType x1) = rnf x1 `seq` ()

140+

141+instance NFData SizeChange where

142+ rnf Smaller = ()

143+ rnf Same = ()

144+ rnf Bigger = ()

145+ rnf Unknown = ()

146+

147+instance NFData CGInfo where

148+ rnf (CGInfo x1 x2 x3 x4 x5)

149+ = rnf x1 `seq`

150+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

151+

152+instance NFData Fixity where

153+ rnf (Infixl x1) = rnf x1 `seq` ()

154+ rnf (Infixr x1) = rnf x1 `seq` ()

155+ rnf (InfixN x1) = rnf x1 `seq` ()

156+ rnf (PrefixN x1) = rnf x1 `seq` ()

157+

158+instance NFData FixDecl where

159+ rnf (Fix x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

160+

161+instance NFData Static where

162+ rnf Static = ()

163+ rnf Dynamic = ()

164+

165+instance NFData Plicity where

166+ rnf (Imp x1 x2 x3 x4)

167+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

168+ rnf (Exp x1 x2 x3 x4)

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

170+ rnf (Constraint x1 x2 x3)

171+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

172+ rnf (TacImp x1 x2 x3 x4)

173+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

174+

175+instance NFData FnOpt where

176+ rnf Inlinable = ()

177+ rnf TotalFn = ()

178+ rnf PartialFn = ()

179+ rnf Coinductive = ()

180+ rnf AssertTotal = ()

181+ rnf Dictionary = ()

182+ rnf Implicit = ()

183+ rnf (CExport x1) = rnf x1 `seq` ()

184+ rnf Reflection = ()

185+ rnf (Specialise x1) = rnf x1 `seq` ()

186+

187+instance (NFData t) => NFData (PDecl' t) where

188+ rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

189+ rnf (PTy x1 x2 x3 x4 x5 x6)

190+ = rnf x1 `seq`

191+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

192+ rnf (PPostulate x1 x2 x3 x4 x5 x6)

193+ = rnf x1 `seq`

194+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

195+ rnf (PClauses x1 x2 x3 x4)

196+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

197+ rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

198+ rnf (PData x1 x2 x3 x4 x5)

199+ = rnf x1 `seq`

200+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

201+ rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

202+ rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

203+ rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

204+ = rnf x1 `seq`

205+ rnf x2 `seq`

206+ rnf x3 `seq`

207+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

208+ rnf (PClass x1 x2 x3 x4 x5 x6 x7)

209+ = rnf x1 `seq`

210+ rnf x2 `seq`

211+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

212+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

213+ = rnf x1 `seq`

214+ rnf x2 `seq`

215+ rnf x3 `seq`

216+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

217+ rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

218+ rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

219+ rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

220+ rnf (PDirective x1) = ()

221+ rnf (PProvider x1 x2 x3 x4 x5)

222+ = rnf x1 `seq`

223+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

224+ rnf (PTransform x1 x2 x3 x4)

225+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

226+

227+instance (NFData t) => NFData (PClause' t) where

228+ rnf (PClause x1 x2 x3 x4 x5 x6)

229+ = rnf x1 `seq`

230+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

231+ rnf (PWith x1 x2 x3 x4 x5 x6)

232+ = rnf x1 `seq`

233+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

234+ rnf (PClauseR x1 x2 x3 x4)

235+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

236+ rnf (PWithR x1 x2 x3 x4)

237+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

238+

239+instance (NFData t) => NFData (PData' t) where

240+ rnf (PDatadecl x1 x2 x3)

241+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

242+ rnf (PLaterdecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

243+

244+instance NFData PTerm where

245+ rnf (PQuote x1) = rnf x1 `seq` ()

246+ rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

247+ rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

248+ rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

249+ rnf (PLam x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

250+ rnf (PPi x1 x2 x3 x4)

251+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

252+ rnf (PLet x1 x2 x3 x4)

253+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

254+ rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

255+ rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

256+ rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

257+ rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

258+ rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

259+ rnf (PTrue x1) = rnf x1 `seq` ()

260+ rnf (PFalse x1) = rnf x1 `seq` ()

261+ rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

262+ rnf (PResolveTC x1) = rnf x1 `seq` ()

263+ rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

264+ rnf (PRewrite x1 x2 x3 x4)

265+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

266+ rnf (PPair x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

267+ rnf (PDPair x1 x2 x3 x4)

268+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

269+ rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

270+ rnf (PHidden x1) = rnf x1 `seq` ()

271+ rnf PType = ()

272+ rnf (PGoal x1 x2 x3 x4)

273+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

274+ rnf (PConstant x1) = rnf x1 `seq` ()

275+ rnf Placeholder = ()

276+ rnf (PDoBlock x1) = rnf x1 `seq` ()

277+ rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

278+ rnf (PReturn x1) = rnf x1 `seq` ()

279+ rnf (PMetavar x1) = rnf x1 `seq` ()

280+ rnf (PProof x1) = rnf x1 `seq` ()

281+ rnf (PTactics x1) = rnf x1 `seq` ()

282+ rnf (PElabError x1) = rnf x1 `seq` ()

283+ rnf PImpossible = ()

284+ rnf (PCoerced x1) = rnf x1 `seq` ()

285+ rnf (PUnifyLog x1) = rnf x1 `seq` ()

286+ rnf (PNoImplicits x1) = rnf x1 `seq` ()

287+

288+instance (NFData t) => NFData (PTactic' t) where

289+ rnf (Intro x1) = rnf x1 `seq` ()

290+ rnf Intros = ()

291+ rnf (Focus x1) = rnf x1 `seq` ()

292+ rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

293+ rnf (Rewrite x1) = rnf x1 `seq` ()

294+ rnf (Equiv x1) = rnf x1 `seq` ()

295+ rnf (MatchRefine x1) = rnf x1 `seq` ()

296+ rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

297+ rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

298+ rnf (Exact x1) = rnf x1 `seq` ()

299+ rnf Compute = ()

300+ rnf Trivial = ()

301+ rnf (ProofSearch x1 x2 x3)

302+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

303+ rnf Solve = ()

304+ rnf Attack = ()

305+ rnf ProofState = ()

306+ rnf ProofTerm = ()

307+ rnf Undo = ()

308+ rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

309+ rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

310+ rnf (ApplyTactic x1) = rnf x1 `seq` ()

311+ rnf (Reflect x1) = rnf x1 `seq` ()

312+ rnf (Fill x1) = rnf x1 `seq` ()

313+ rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

314+ rnf Qed = ()

315+ rnf Abandon = ()

316+

317+instance (NFData t) => NFData (PDo' t) where

318+ rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

319+ rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

320+ rnf (DoBindP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

321+ rnf (DoLet x1 x2 x3 x4)

322+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

323+ rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

324+

325+instance (NFData t) => NFData (PArg' t) where

326+ rnf (PImp x1 x2 x3 x4 x5 x6)

327+ = rnf x1 `seq`

328+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

329+ rnf (PExp x1 x2 x3 x4)

330+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

331+ rnf (PConstraint x1 x2 x3 x4)

332+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

333+ rnf (PTacImplicit x1 x2 x3 x4 x5 x6)

334+ = rnf x1 `seq`

335+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

336+

337+instance NFData ClassInfo where

338+ rnf (CI x1 x2 x3 x4 x5)

339+ = rnf x1 `seq`

340+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

341+

342+instance NFData OptInfo where

343+ rnf (Optimise x1 x2 x3 x4)

344+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

345+

346+instance NFData TypeInfo where

347+ rnf (TI x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

348+

349+instance (NFData t) => NFData (DSL' t) where

350+ rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

351+ = rnf x1 `seq`

352+ rnf x2 `seq`

353+ rnf x3 `seq`

354+ rnf x4 `seq`

355+ rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

356+

357+instance NFData SynContext where

358+ rnf PatternSyntax = ()

359+ rnf TermSyntax = ()

360+ rnf AnySyntax = ()

361+

362+instance NFData Syntax where

363+ rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

364+

365+instance NFData SSymbol where

366+ rnf (Keyword x1) = rnf x1 `seq` ()

367+ rnf (Symbol x1) = rnf x1 `seq` ()

368+ rnf (Binding x1) = rnf x1 `seq` ()

369+ rnf (Expr x1) = rnf x1 `seq` ()

370+ rnf (SimpleExpr x1) = rnf x1 `seq` ()

371+

372+instance NFData Using where

373+ rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

374+ rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

375+

376+

377+instance NFData SyntaxInfo where

378+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8)

379+ = rnf x1 `seq`

380+ rnf x2 `seq`

381+ rnf x3 `seq`

382+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

383+

384+

385+

src/Idris/ElabDecls.hs+5−3

@@ -15,6 +15,7 @@ import Idris.Providers

1515import Idris.Primitives

1616import Idris.Inliner

1717import Idris.PartialEval

18+import Idris.DeepSeq

1819import IRTS.Lang

1920import Paths_idris

2021

@@ -25,6 +26,7 @@ import Core.Execute

2526import Core.Typecheck

2627import Core.CaseTree

2728

29+import Control.DeepSeq

2830import Control.Monad

2931import Control.Monad.State

3032import Data.List

@@ -686,7 +688,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

686688 logLvl 3 $ "Optimised: " ++ show tree'

687689 ctxt <- getContext

688690 ist <- getIState

689− putIState (ist { idris_patdefs = addDef n (pdef', pmissing)

691+ putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)

690692 (idris_patdefs ist) })

691693 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

692694 case lookupTy n ctxt of

@@ -741,10 +743,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

741743 getLHS (_, l, _) = l

742744

743745 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

744− normalisePats ctxt [] y)

746+ force (normalisePats ctxt [] y))

745747 simple_lhs ctxt t = t

746748

747− simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)

749+ simple_rt ctxt (p, x, y) = (p, x, force (rt_simplify ctxt [] y))

748750

749751 -- this is so pattern types are in the right form for erasure

750752 normalisePats ctxt env (Bind n (PVar t) sc)

src/Idris/REPL.hs+5−3

@@ -23,6 +23,7 @@ import Idris.Imports

2323import Idris.Colours

2424import Idris.Inliner

2525import Idris.CaseSplit

26+import Idris.DeepSeq

2627

2728import Paths_idris

2829import Util.System

@@ -67,6 +68,7 @@ import Data.List

6768import Data.Char

6869import Data.Version

6970import Data.Word (Word)

71+import Control.DeepSeq

7072

7173import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

7274

@@ -417,11 +419,11 @@ process h fn (ChangeDirectory f)

417419process h fn (Eval t)

418420 = do (tm, ty) <- elabVal toplevel False t

419421 ctxt <- getContext

420− ist <- getIState

421− let tm' = normaliseAll ctxt [] tm

422− let ty' = normaliseAll ctxt [] ty

422+ let tm' = force (normaliseAll ctxt [] tm)

423+ let ty' = force (normaliseAll ctxt [] ty)

423424 -- Add value to context, call it "it"

424425 updateContext (addCtxtDef (UN "it") (Function ty' tm'))

426+ ist <- getIState

425427 logLvl 3 $ "Raw: " ++ show (tm', ty')

426428 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

427429 imp <- impShow