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

git.iko.soy/Idris-dev

on master help sign in

Strictness improvements

543cd7eEdwin Brady13 years ago

idris.cabal+2

compare with master

unifiedsplit

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

324 , Idris.Coverage

325 , Idris.DSL

326 , Idris.DataOpts

327+ , Idris.DeepSeq

327 , Idris.Delaborate

328 , Idris.Delaborate

328 , Idris.Docs

329 , Idris.Docs

329 , Idris.ElabDecls

330 , Idris.ElabDecls

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

406 , vector-binary-instances

407 , vector-binary-instances

407 , network

408 , network

408 , xml

409 , xml

410+ , deepseq

409

411

410 Extensions: MultiParamTypeClasses

412 Extensions: MultiParamTypeClasses

411 , FunctionalDependencies

413 , FunctionalDependencies

src/Core/CaseTree.hs+7−7

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

11import Data.List hiding (partition)

12import Debug.Trace

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

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

15 deriving Show

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

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

19− | STerm t

19+ | STerm !t

20 | UnmatchedCase String -- ^ error message

21 | ImpossibleCase -- ^ already checked to be impossible

22 deriving (Eq, Ord, Functor)

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

27type SC = SC' Term

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

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

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

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

31− | ConstCase Const (SC' t)

31+ | ConstCase Const !(SC' t)

32− | SucCase Name (SC' t)

32+ | SucCase Name !(SC' t)

33− | DefaultCase (SC' t)

33+ | DefaultCase !(SC' t)

34 deriving (Show, Eq, Ord, Functor)

35{-!

36deriving instance Binary CaseAlt

src/Core/Evaluate.hs+11−11

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

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

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

582

583−data Def = Function Type Term

583+data Def = Function !Type !Term

584− | TyDecl NameType Type

584+ | TyDecl NameType !Type

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

586 | CaseOp CaseInfo

587− Type

587+ !Type

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

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

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

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

590− CaseDefs

590+ !CaseDefs

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

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

593

594data CaseDefs = CaseDefs {

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

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

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

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

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

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

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

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

599 }

600

601data CaseInfo = CaseInfo {

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

719

720addCtxtDef :: Name -> Def -> Context -> Context

721addCtxtDef 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

723 c { definitions = ctxt' }

724

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

src/Core/TT.hs+19

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

66{-!

67deriving instance Binary FC

68+deriving instance NFData FC

68!-}

69!-}

70instance Sized FC where

71instance Sized FC where

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

103 | ProviderError String

104 | ProviderError String

104 | LoadingFailed String Err

105 | LoadingFailed String Err

105 deriving Eq

106 deriving Eq

107+{-!

108+deriving instance NFData Err

109+!-}

106

110

107instance Sized Err where

111instance Sized Err where

108 size (Msg msg) = length msg

112 size (Msg msg) = length msg

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

225 deriving (Eq, Ord)

229 deriving (Eq, Ord)

226{-!

230{-!

227deriving instance Binary Name

231deriving instance Binary Name

232+deriving instance NFData Name

228!-}

233!-}

229

234

230data SpecialName = WhereN Int Name Name

235data SpecialName = WhereN Int Name Name

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

235 deriving (Eq, Ord)

240 deriving (Eq, Ord)

236{-!

241{-!

237deriving instance Binary SpecialName

242deriving instance Binary SpecialName

243+deriving instance NFData SpecialName

238!-}

244!-}

239

245

240instance Sized Name where

246instance Sized Name where

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

369

375

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

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

371 deriving (Show, Eq, Ord)

377 deriving (Show, Eq, Ord)

378+{-!

379+deriving instance NFData IntTy

380+deriving instance NFData NativeTy

381+deriving instance NFData ArithTy

382+!-}

372

383

373instance Pretty ArithTy where

384instance Pretty ArithTy where

374 pretty (ATInt ITNative) = text "Int"

385 pretty (ATInt ITNative) = text "Int"

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

400 deriving (Eq, Ord)

411 deriving (Eq, Ord)

401{-!

412{-!

402deriving instance Binary Const

413deriving instance Binary Const

414+deriving instance NFData Const

403!-}

415!-}

404

416

405instance Sized Const where

417instance Sized Const where

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

442

454

443{-!

455{-!

444deriving instance Binary Raw

456deriving instance Binary Raw

457+deriving instance NFData Raw

445!-}

458!-}

446

459

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

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

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

461 deriving (Show, Eq, Ord, Functor)

474 deriving (Show, Eq, Ord, Functor)

462{-!

475{-!

463deriving instance Binary Binder

476deriving instance Binary Binder

477+deriving instance NFData Binder

464!-}

478!-}

465

479

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

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

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

515data UExp = UVar Int -- ^ universe variable

529data UExp = UVar Int -- ^ universe variable

516 | UVal Int -- ^ explicit universe level

530 | UVal Int -- ^ explicit universe level

517 deriving (Eq, Ord)

531 deriving (Eq, Ord)

532+{-!

533+deriving instance NFData UExp

534+!-}

518

535

519instance Sized UExp where

536instance Sized UExp where

520 size _ = 1

537 size _ = 1

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

551 deriving (Show, Ord)

568 deriving (Show, Ord)

552{-!

569{-!

553deriving instance Binary NameType

570deriving instance Binary NameType

571+deriving instance NFData NameType

554!-}

572!-}

555

573

556instance Sized NameType where

574instance Sized NameType where

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

580 deriving (Ord, Functor)

598 deriving (Ord, Functor)

581{-!

599{-!

582deriving instance Binary TT

600deriving instance Binary TT

601+deriving instance NFData TT

583!-}

602!-}

584

603

585class TermSize a where

604class TermSize a where

src/Idris/AbsSyntaxTree.hs+23

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

134 deriving (Show, Eq)

135{-!

136deriving instance Binary SizeChange

137+deriving instance NFData SizeChange

137!-}

138!-}

138

139

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

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

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

146 deriving Show

147 deriving Show

147{-!

148{-!

148deriving instance Binary CGInfo

149deriving instance Binary CGInfo

150+deriving instance NFData CGInfo

149!-}

151!-}

150

152

151primDefs = [UN "unsafePerformPrimIO",

153primDefs = [UN "unsafePerformPrimIO",

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

301 deriving Eq

303 deriving Eq

302{-!

304{-!

303deriving instance Binary Fixity

305deriving instance Binary Fixity

306+deriving instance NFData Fixity

304!-}

307!-}

305

308

306instance Show Fixity where

309instance Show Fixity where

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

317

320

318{-!

321{-!

319deriving instance Binary FixDecl

322deriving instance Binary FixDecl

323+deriving instance NFData FixDecl

320!-}

324!-}

321

325

322instance Ord FixDecl where

326instance Ord FixDecl where

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

327 deriving (Show, Eq)

331 deriving (Show, Eq)

328{-!

332{-!

329deriving instance Binary Static

333deriving instance Binary Static

334+deriving instance NFData Static

330!-}

335!-}

331

336

332-- Mark bindings with their explicitness, and laziness

337-- Mark bindings with their explicitness, and laziness

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

349

354

350{-!

355{-!

351deriving instance Binary Plicity

356deriving instance Binary Plicity

357+deriving instance NFData Plicity

352!-}

358!-}

353

359

354impl = Imp False Dynamic "" False

360impl = Imp False Dynamic "" False

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

369 deriving (Show, Eq)

375 deriving (Show, Eq)

370{-!

376{-!

371deriving instance Binary FnOpt

377deriving instance Binary FnOpt

378+deriving instance NFData FnOpt

372!-}

379!-}

373

380

374type FnOpts = [FnOpt]

381type FnOpts = [FnOpt]

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

416 deriving Functor

423 deriving Functor

417{-!

424{-!

418deriving instance Binary PDecl'

425deriving instance Binary PDecl'

426+deriving instance NFData PDecl'

419!-}

427!-}

420

428

421-- For elaborator state

429-- For elaborator state

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

438 deriving Functor

446 deriving Functor

439{-!

447{-!

440deriving instance Binary PClause'

448deriving instance Binary PClause'

449+deriving instance NFData PClause'

441!-}

450!-}

442

451

443-- | Data declaration

452-- | Data declaration

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

451 deriving Functor

460 deriving Functor

452{-!

461{-!

453deriving instance Binary PData'

462deriving instance Binary PData'

463+deriving instance NFData PData'

454!-}

464!-}

455

465

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

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

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

581

591

582{-!

592{-!

583deriving instance Binary PTerm

593deriving instance Binary PTerm

594+deriving instance NFData PTerm

584!-}

595!-}

585

596

586mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

597mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

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

628 deriving (Show, Eq, Functor)

639 deriving (Show, Eq, Functor)

629{-!

640{-!

630deriving instance Binary PTactic'

641deriving instance Binary PTactic'

642+deriving instance NFData PTactic'

631!-}

643!-}

632

644

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

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

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

663 deriving (Eq, Functor)

675 deriving (Eq, Functor)

664{-!

676{-!

665deriving instance Binary PDo'

677deriving instance Binary PDo'

678+deriving instance NFData PDo'

666!-}

679!-}

667

680

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

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

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

703

716

704{-!

717{-!

705deriving instance Binary PArg'

718deriving instance Binary PArg'

719+deriving instance NFData PArg'

706!-}

720!-}

707

721

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

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

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

722 deriving Show

736 deriving Show

723{-!

737{-!

724deriving instance Binary ClassInfo

738deriving instance Binary ClassInfo

739+deriving instance NFData ClassInfo

725!-}

740!-}

726

741

727data OptInfo = Optimise { collapsible :: Bool,

742data OptInfo = Optimise { collapsible :: Bool,

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

731 deriving Show

746 deriving Show

732{-!

747{-!

733deriving instance Binary OptInfo

748deriving instance Binary OptInfo

749+deriving instance NFData OptInfo

734!-}

750!-}

735

751

736

752

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

740 deriving Show

756 deriving Show

741{-!

757{-!

742deriving instance Binary TypeInfo

758deriving instance Binary TypeInfo

759+deriving instance NFData TypeInfo

743!-}

760!-}

744

761

745-- Syntactic sugar info

762-- Syntactic sugar info

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

757 deriving (Show, Functor)

774 deriving (Show, Functor)

758{-!

775{-!

759deriving instance Binary DSL'

776deriving instance Binary DSL'

777+deriving instance NFData DSL'

760!-}

778!-}

761

779

762type DSL = DSL' PTerm

780type DSL = DSL' PTerm

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

765 deriving Show

783 deriving Show

766{-!

784{-!

767deriving instance Binary SynContext

785deriving instance Binary SynContext

786+deriving instance NFData SynContext

768!-}

787!-}

769

788

770data Syntax = Rule [SSymbol] PTerm SynContext

789data Syntax = Rule [SSymbol] PTerm SynContext

771 deriving Show

790 deriving Show

772{-!

791{-!

773deriving instance Binary Syntax

792deriving instance Binary Syntax

793+deriving instance NFData Syntax

774!-}

794!-}

775

795

776data SSymbol = Keyword Name

796data SSymbol = Keyword Name

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

781 deriving Show

801 deriving Show

782{-!

802{-!

783deriving instance Binary SSymbol

803deriving instance Binary SSymbol

804+deriving instance NFData SSymbol

784!-}

805!-}

785

806

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

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

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

799 deriving (Show, Eq)

820 deriving (Show, Eq)

800{-!

821{-!

801deriving instance Binary Using

822deriving instance Binary Using

823+deriving instance NFData Using

802!-}

824!-}

803

825

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

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

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

811 dsl_info :: DSL }

833 dsl_info :: DSL }

812 deriving Show

834 deriving Show

813{-!

835{-!

836+deriving instance NFData SyntaxInfo

814deriving instance Binary SyntaxInfo

837deriving instance Binary SyntaxInfo

815!-}

838!-}

816

839

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

15import Idris.Primitives

16import Idris.Inliner

17import Idris.PartialEval

18+import Idris.DeepSeq

18import IRTS.Lang

19import IRTS.Lang

19import Paths_idris

20import Paths_idris

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

25import Core.Typecheck

26import Core.Typecheck

26import Core.CaseTree

27import Core.CaseTree

29+import Control.DeepSeq

28import Control.Monad

30import Control.Monad

29import Control.Monad.State

31import Control.Monad.State

30import Data.List

32import Data.List

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

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

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

687 ctxt <- getContext

689 ctxt <- getContext

688 ist <- getIState

690 ist <- getIState

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

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

690 (idris_patdefs ist) })

692 (idris_patdefs ist) })

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

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

692 case lookupTy n ctxt of

694 case lookupTy n ctxt of

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

741 getLHS (_, l, _) = l

743 getLHS (_, l, _) = l

742

744

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

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

744− normalisePats ctxt [] y)

746+ force (normalisePats ctxt [] y))

745 simple_lhs ctxt t = t

747 simple_lhs ctxt t = t

746

748

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

748

750

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

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

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

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

src/Idris/REPL.hs+5−3

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

23import Idris.Colours

24import Idris.Inliner

25import Idris.CaseSplit

26+import Idris.DeepSeq

27import Paths_idris

28import Paths_idris

28import Util.System

29import Util.System

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

67import Data.Char

68import Data.Char

68import Data.Version

69import Data.Version

69import Data.Word (Word)

70import Data.Word (Word)

71+import Control.DeepSeq

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

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

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

417process h fn (Eval t)

419process h fn (Eval t)

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

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

419 ctxt <- getContext

421 ctxt <- getContext

420− ist <- getIState

421− let tm' = normaliseAll ctxt [] tm

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

422− let ty' = normaliseAll ctxt [] ty

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

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

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

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

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

426+ ist <- getIState

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

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

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

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

427 imp <- impShow

429 imp <- impShow