9baa5ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use GHC generics for NFData instances

9baa5ceEcho Nolan10 years ago

src/IRTS/CodegenCommon.hs+4−1

compare with master

unifiedsplit

@@ -1,3 +1,4 @@

1+{-# LANGUAGE DeriveGeneric #-}

1{-|

2{-|

2Module : IRTS.CodegenCommon

3Module : IRTS.CodegenCommon

3Description : Common data structures required for all code generators.

4Description : Common data structures required for all code generators.

@@ -7,12 +8,14 @@ Maintainer : The Idris Community.

7-}

8-}

8module IRTS.CodegenCommon where

9module IRTS.CodegenCommon where

11+import GHC.Generics (Generic)

12+

10import Idris.Core.TT

13import Idris.Core.TT

11import IRTS.Simplified

14import IRTS.Simplified

12import IRTS.Defunctionalise

15import IRTS.Defunctionalise

14data DbgLevel = NONE | DEBUG | TRACE deriving Eq

17data DbgLevel = NONE | DEBUG | TRACE deriving Eq

15−data OutputType = Raw | Object | Executable deriving (Eq, Show)

18+data OutputType = Raw | Object | Executable deriving (Eq, Show, Generic)

17-- | Everything which might be needed in a code generator.

20-- | Everything which might be needed in a code generator.

18--

21--

src/IRTS/Lang.hs+3−2

@@ -5,7 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE PatternGuards, DeriveFunctor #-}

8+{-# LANGUAGE PatternGuards, DeriveFunctor, DeriveGeneric #-}

10module IRTS.Lang where

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

18import Data.List

19import Debug.Trace

20+import GHC.Generics (Generic)

21data Endianness = Native | BE | LE deriving (Show, Eq)

22data Endianness = Native | BE | LE deriving (Show, Eq)

@@ -93,7 +94,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

93 -- core or another machine. 'id' is a valid implementation

94 -- core or another machine. 'id' is a valid implementation

94 | LExternal Name

95 | LExternal Name

95 | LNoOp

96 | LNoOp

96− deriving (Show, Eq)

97+ deriving (Show, Eq, Generic)

98-- Supported target languages for foreign calls

99-- Supported target languages for foreign calls

100

src/Idris/AbsSyntaxTree.hs+46−40

@@ -6,7 +6,8 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

9− DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}

9+ DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,

10+ PatternGuards #-}

11module Idris.AbsSyntaxTree where

12module Idris.AbsSyntaxTree where

@@ -47,6 +48,7 @@ import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

47import Data.Traversable (Traversable)

48import Data.Traversable (Traversable)

48import Data.Typeable

49import Data.Typeable

49import Data.Foldable (Foldable)

50import Data.Foldable (Foldable)

51+import GHC.Generics (Generic)

51import Debug.Trace

53import Debug.Trace

@@ -112,7 +114,7 @@ data IOption = IOption {

112 , opt_evaltypes :: Bool -- ^ normalise types in `:t`

114 , opt_evaltypes :: Bool -- ^ normalise types in `:t`

113 , opt_desugarnats :: Bool

115 , opt_desugarnats :: Bool

114 , opt_autoimpls :: Bool

116 , opt_autoimpls :: Bool

115− } deriving (Show, Eq)

117+ } deriving (Show, Eq, Generic)

116

118

117defaultOpts = IOption { opt_logLevel = 0

119defaultOpts = IOption { opt_logLevel = 0

118 , opt_logcats = []

120 , opt_logcats = []

@@ -150,7 +152,7 @@ data PPOption = PPOption {

150 } deriving (Show)

152 } deriving (Show)

151

153

152data Optimisation = PETransform -- ^ partial eval and associated transforms

154data Optimisation = PETransform -- ^ partial eval and associated transforms

153− deriving (Show, Eq)

155+ deriving (Show, Eq, Generic)

154

156

155defaultOptimise = [PETransform]

157defaultOptimise = [PETransform]

156

158

@@ -185,7 +187,8 @@ ppOption opt = PPOption {

185ppOptionIst :: IState -> PPOption

187ppOptionIst :: IState -> PPOption

186ppOptionIst = ppOption . idris_options

188ppOptionIst = ppOption . idris_options

187

189

188−data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

190+data LanguageExt = TypeProviders | ErrorReflection

191+ deriving (Show, Eq, Read, Ord, Generic)

189

192

190-- | The output mode in use

193-- | The output mode in use

191data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

194data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

@@ -196,13 +199,13 @@ data OutputMode = RawOutput Handle -- ^ Print user output directly to the

196data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

199data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

197 | ColsWide Int -- ^ Manually specified - must be positive

200 | ColsWide Int -- ^ Manually specified - must be positive

198 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

201 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

199− deriving (Show, Eq)

202+ deriving (Show, Eq, Generic)

200

203

201-- | If a function has no totality annotation, what do we assume?

204-- | If a function has no totality annotation, what do we assume?

202data DefaultTotality = DefaultCheckingTotal -- ^ Total

205data DefaultTotality = DefaultCheckingTotal -- ^ Total

203 | DefaultCheckingPartial -- ^ Partial

206 | DefaultCheckingPartial -- ^ Partial

204 | DefaultCheckingCovering -- ^Total coverage, but may diverge

207 | DefaultCheckingCovering -- ^Total coverage, but may diverge

205− deriving (Show, Eq)

208+ deriving (Show, Eq, Generic)

206

209

207-- | The global state used in the Idris monad

210-- | The global state used in the Idris monad

208data IState = IState {

211data IState = IState {

@@ -305,13 +308,14 @@ data IState = IState {

305 , idris_ttstats :: M.Map Term (Int, Term)

308 , idris_ttstats :: M.Map Term (Int, Term)

306 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

309 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

307 }

310 }

311+ deriving Generic

308

312

309-- Required for parsers library, and therefore trifecta

313-- Required for parsers library, and therefore trifecta

310instance Show IState where

314instance Show IState where

311 show = const "{internal state}"

315 show = const "{internal state}"

312

316

313data SizeChange = Smaller | Same | Bigger | Unknown

317data SizeChange = Smaller | Same | Bigger | Unknown

314− deriving (Show, Eq)

318+ deriving (Show, Eq, Generic)

315{-!

319{-!

316deriving instance Binary SizeChange

320deriving instance Binary SizeChange

317deriving instance NFData SizeChange

321deriving instance NFData SizeChange

@@ -324,7 +328,7 @@ data CGInfo = CGInfo {

324 calls :: [Name]

328 calls :: [Name]

325 , scg :: [SCGEntry]

329 , scg :: [SCGEntry]

326 , usedpos :: [(Int, [UsageReason])]

330 , usedpos :: [(Int, [UsageReason])]

327− } deriving Show

331+ } deriving (Show, Generic)

328{-!

332{-!

329deriving instance Binary CGInfo

333deriving instance Binary CGInfo

330deriving instance NFData CGInfo

334deriving instance NFData CGInfo

@@ -384,7 +388,7 @@ data IBCWrite = IBCFix FixDecl

384 | IBCDeprecate Name String

388 | IBCDeprecate Name String

385 | IBCFragile Name String

389 | IBCFragile Name String

386 | IBCConstraint FC UConstraint

390 | IBCConstraint FC UConstraint

387− deriving Show

391+ deriving (Show, Generic)

388

392

389-- | The initial state for the compiler

393-- | The initial state for the compiler

390idrisInit :: IState

394idrisInit :: IState

@@ -420,12 +424,12 @@ throwError = Trans.lift . throwE

420

424

421data Codegen = Via IRFormat String

425data Codegen = Via IRFormat String

422 | Bytecode

426 | Bytecode

423− deriving (Show, Eq)

427+ deriving (Show, Eq, Generic)

424{-!

428{-!

425deriving instance NFData Codegen

429deriving instance NFData Codegen

426!-}

430!-}

427

431

428−data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)

432+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)

429

433

430data HowMuchDocs = FullDocs | OverviewDocs

434data HowMuchDocs = FullDocs | OverviewDocs

431

435

@@ -511,7 +515,7 @@ data LogCat = IParse

511 | IErasure

515 | IErasure

512 | ICoverage

516 | ICoverage

513 | IIBC

517 | IIBC

514− deriving (Show, Eq, Ord)

518+ deriving (Show, Eq, Ord, Generic)

515

519

516strLogCat :: LogCat -> String

520strLogCat :: LogCat -> String

517strLogCat IParse = "parser"

521strLogCat IParse = "parser"

@@ -606,7 +610,7 @@ data Opt = Filename String

606 | DesugarNats

610 | DesugarNats

607 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

611 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

608 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

612 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

609− deriving (Show, Eq)

613+ deriving (Show, Eq, Generic)

610

614

611data ElabShellCmd = EQED

615data ElabShellCmd = EQED

612 | EAbandon

616 | EAbandon

@@ -625,7 +629,7 @@ data Fixity = Infixl { prec :: Int }

625 | Infixr { prec :: Int }

629 | Infixr { prec :: Int }

626 | InfixN { prec :: Int }

630 | InfixN { prec :: Int }

627 | PrefixN { prec :: Int }

631 | PrefixN { prec :: Int }

628− deriving Eq

632+ deriving (Eq, Generic)

629{-!

633{-!

630deriving instance Binary Fixity

634deriving instance Binary Fixity

631deriving instance NFData Fixity

635deriving instance NFData Fixity

@@ -638,7 +642,7 @@ instance Show Fixity where

638 show (PrefixN i) = "prefix " ++ show i

642 show (PrefixN i) = "prefix " ++ show i

639

643

640data FixDecl = Fix Fixity String

644data FixDecl = Fix Fixity String

641− deriving Eq

645+ deriving (Eq, Generic)

642

646

643instance Show FixDecl where

647instance Show FixDecl where

644 show (Fix f s) = show f ++ " " ++ s

648 show (Fix f s) = show f ++ " " ++ s

@@ -653,7 +657,7 @@ instance Ord FixDecl where

653

657

654

658

655data Static = Static | Dynamic

659data Static = Static | Dynamic

656− deriving (Show, Eq, Data, Typeable)

660+ deriving (Show, Eq, Data, Generic, Typeable)

657{-!

661{-!

658deriving instance Binary Static

662deriving instance Binary Static

659deriving instance NFData Static

663deriving instance NFData Static

@@ -677,7 +681,7 @@ data Plicity = Imp { pargopts :: [ArgOpt]

677 , pstatic :: Static

681 , pstatic :: Static

678 , pscript :: PTerm

682 , pscript :: PTerm

679 }

683 }

680− deriving (Show, Eq, Data, Typeable)

684+ deriving (Show, Eq, Data, Generic, Typeable)

681

685

682{-!

686{-!

683deriving instance Binary Plicity

687deriving instance Binary Plicity

@@ -721,7 +725,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

721 | Constructor -- ^ Data constructor type

725 | Constructor -- ^ Data constructor type

722 | AutoHint -- ^ use in auto implicit search

726 | AutoHint -- ^ use in auto implicit search

723 | PEGenerated -- ^ generated by partial evaluator

727 | PEGenerated -- ^ generated by partial evaluator

724− deriving (Show, Eq)

728+ deriving (Show, Eq, Generic)

725{-!

729{-!

726deriving instance Binary FnOpt

730deriving instance Binary FnOpt

727deriving instance NFData FnOpt

731deriving instance NFData FnOpt

@@ -739,7 +743,7 @@ dictionary = elem Dictionary

739-- | Type provider - what to provide

743-- | Type provider - what to provide

740data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

744data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

741 | ProvPostulate t -- ^ goal type must be Type, so only term

745 | ProvPostulate t -- ^ goal type must be Type, so only term

742− deriving (Show, Eq, Functor)

746+ deriving (Show, Eq, Functor, Generic)

743

747

744type ProvideWhat = ProvideWhat' PTerm

748type ProvideWhat = ProvideWhat' PTerm

745

749

@@ -824,7 +828,7 @@ data PDecl' t

824 -- | FC is decl-level, for errors, and Strings represent the

828 -- | FC is decl-level, for errors, and Strings represent the

825 -- namespace

829 -- namespace

826 | PRunElabDecl FC t [String]

830 | PRunElabDecl FC t [String]

827− deriving Functor

831+ deriving (Functor, Generic)

828{-!

832{-!

829deriving instance Binary PDecl'

833deriving instance Binary PDecl'

830deriving instance NFData PDecl'

834deriving instance NFData PDecl'

@@ -851,6 +855,7 @@ data Directive = DLib Codegen String

851 | DFragile Name String

855 | DFragile Name String

852 | DAutoImplicits Bool

856 | DAutoImplicits Bool

853 | DUsed FC Name Name

857 | DUsed FC Name Name

858+ deriving Generic

854

859

855-- | A set of instructions for things that need to happen in IState

860-- | A set of instructions for things that need to happen in IState

856-- after a term elaboration when there's been reflected elaboration.

861-- after a term elaboration when there's been reflected elaboration.

@@ -895,7 +900,7 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A

895 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]

900 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]

896 | PClauseR FC [t] t [PDecl' t]

901 | PClauseR FC [t] t [PDecl' t]

897 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]

902 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]

898− deriving Functor

903+ deriving (Functor, Generic)

899{-!

904{-!

900deriving instance Binary PClause'

905deriving instance Binary PClause'

901deriving instance NFData PClause'

906deriving instance NFData PClause'

@@ -913,7 +918,7 @@ data PData' t =

913 | PLaterdecl { d_name :: Name

918 | PLaterdecl { d_name :: Name

914 , d_name_fc :: FC

919 , d_name_fc :: FC

915 , d_tcon :: t

920 , d_tcon :: t

916− } deriving Functor

921+ } deriving (Functor, Generic)

917

922

918-- | Transform the FCs in a PData and its associated terms. The first

923-- | Transform the FCs in a PData and its associated terms. The first

919-- function transforms the general-purpose FCs, and the second

924-- function transforms the general-purpose FCs, and the second

@@ -1103,7 +1108,7 @@ updateNs ns t = mapPT updateRef t

1103data PunInfo = IsType

1108data PunInfo = IsType

1104 | IsTerm

1109 | IsTerm

1105 | TypeOrTerm

1110 | TypeOrTerm

1106− deriving (Eq, Show, Data, Typeable)

1111+ deriving (Eq, Show, Data, Typeable, Generic)

1107

1112

1108-- | High level language terms

1113-- | High level language terms

1109data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

1114data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

@@ -1170,12 +1175,12 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

1170 | PConstSugar FC PTerm

1175 | PConstSugar FC PTerm

1171 -- ^ A desugared constant. The FC is a precise source

1176 -- ^ A desugared constant. The FC is a precise source

1172 -- location that will be used to highlight it later.

1177 -- location that will be used to highlight it later.

1173− deriving (Eq, Data, Typeable)

1178+ deriving (Eq, Data, Typeable, Generic)

1174

1179

1175data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

1180data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

1176 | FirstSuccess

1181 | FirstSuccess

1177 | TryImplicit

1182 | TryImplicit

1178− deriving (Eq, Data, Typeable)

1183+ deriving (Eq, Data, Generic, Typeable)

1179

1184

1180-- | Transform the FCs in a PTerm. The first function transforms the

1185-- | Transform the FCs in a PTerm. The first function transforms the

1181-- general-purpose FCs, and the second transforms those that are used

1186-- general-purpose FCs, and the second transforms those that are used

@@ -1296,7 +1301,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

1296 | TFail [ErrorReportPart]

1301 | TFail [ErrorReportPart]

1297 | Qed | Abandon

1302 | Qed | Abandon

1298 | SourceFC

1303 | SourceFC

1299− deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)

1304+ deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)

1300{-!

1305{-!

1301deriving instance Binary PTactic'

1306deriving instance Binary PTactic'

1302deriving instance NFData PTactic'

1307deriving instance NFData PTactic'

@@ -1343,7 +1348,7 @@ data PDo' t = DoExp FC t

1343 | DoBindP FC t t [(t,t)]

1348 | DoBindP FC t t [(t,t)]

1344 | DoLet FC Name FC t t -- ^ second FC is precise name location

1349 | DoLet FC Name FC t t -- ^ second FC is precise name location

1345 | DoLetP FC t t

1350 | DoLetP FC t t

1346− deriving (Eq, Functor, Data, Typeable)

1351+ deriving (Eq, Functor, Data, Generic, Typeable)

1347{-!

1352{-!

1348deriving instance Binary PDo'

1353deriving instance Binary PDo'

1349deriving instance NFData PDo'

1354deriving instance NFData PDo'

@@ -1384,13 +1389,13 @@ data PArg' t = PImp { priority :: Int

1384 , getScript :: t

1389 , getScript :: t

1385 , getTm :: t

1390 , getTm :: t

1386 }

1391 }

1387− deriving (Show, Eq, Functor, Data, Typeable)

1392+ deriving (Show, Eq, Functor, Data, Generic, Typeable)

1388

1393

1389data ArgOpt = AlwaysShow

1394data ArgOpt = AlwaysShow

1390 | HideDisplay

1395 | HideDisplay

1391 | InaccessibleArg

1396 | InaccessibleArg

1392 | UnknownImp

1397 | UnknownImp

1393− deriving (Show, Eq, Data, Typeable)

1398+ deriving (Show, Eq, Data, Generic, Typeable)

1394

1399

1395instance Sized a => Sized (PArg' a) where

1400instance Sized a => Sized (PArg' a) where

1396 size (PImp p _ l nm trm) = 1 + size nm + size trm

1401 size (PImp p _ l nm trm) = 1 + size nm + size trm

@@ -1480,7 +1485,7 @@ data ClassInfo = CI {

1480 , class_params :: [Name]

1485 , class_params :: [Name]

1481 , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded

1486 , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded

1482 , class_determiners :: [Int]

1487 , class_determiners :: [Int]

1483− } deriving Show

1488+ } deriving (Show, Generic)

1484{-!

1489{-!

1485deriving instance Binary ClassInfo

1490deriving instance Binary ClassInfo

1486deriving instance NFData ClassInfo

1491deriving instance NFData ClassInfo

@@ -1491,17 +1496,17 @@ data RecordInfo = RI {

1491 record_parameters :: [(Name,PTerm)]

1496 record_parameters :: [(Name,PTerm)]

1492 , record_constructor :: Name

1497 , record_constructor :: Name

1493 , record_projections :: [Name]

1498 , record_projections :: [Name]

1494− } deriving Show

1499+ } deriving (Show, Generic)

1495

1500

1496-- Type inference data

1501-- Type inference data

1497

1502

1498data TIData = TIPartial -- ^ a function with a partially defined type

1503data TIData = TIPartial -- ^ a function with a partially defined type

1499 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

1504 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

1500− deriving Show

1505+ deriving (Show, Generic)

1501

1506

1502-- | Miscellaneous information about functions

1507-- | Miscellaneous information about functions

1503data FnInfo = FnInfo { fn_params :: [Int] }

1508data FnInfo = FnInfo { fn_params :: [Int] }

1504− deriving Show

1509+ deriving (Show, Generic)

1505{-!

1510{-!

1506deriving instance Binary FnInfo

1511deriving instance Binary FnInfo

1507deriving instance NFData FnInfo

1512deriving instance NFData FnInfo

@@ -1510,7 +1515,7 @@ deriving instance NFData FnInfo

1510data OptInfo = Optimise {

1515data OptInfo = Optimise {

1511 inaccessible :: [(Int,Name)] -- includes names for error reporting

1516 inaccessible :: [(Int,Name)] -- includes names for error reporting

1512 , detaggable :: Bool

1517 , detaggable :: Bool

1513− } deriving Show

1518+ } deriving (Show, Generic)

1514{-!

1519{-!

1515deriving instance Binary OptInfo

1520deriving instance Binary OptInfo

1516deriving instance NFData OptInfo

1521deriving instance NFData OptInfo

@@ -1528,7 +1533,7 @@ data DSL' t = DSL {

1528 , dsl_lambda :: Maybe t

1533 , dsl_lambda :: Maybe t

1529 , dsl_let :: Maybe t

1534 , dsl_let :: Maybe t

1530 , dsl_pi :: Maybe t

1535 , dsl_pi :: Maybe t

1531− } deriving (Show, Functor)

1536+ } deriving (Show, Functor, Generic)

1532{-!

1537{-!

1533deriving instance Binary DSL'

1538deriving instance Binary DSL'

1534deriving instance NFData DSL'

1539deriving instance NFData DSL'

@@ -1539,7 +1544,7 @@ type DSL = DSL' PTerm

1539data SynContext = PatternSyntax

1544data SynContext = PatternSyntax

1540 | TermSyntax

1545 | TermSyntax

1541 | AnySyntax

1546 | AnySyntax

1542− deriving Show

1547+ deriving (Show, Generic)

1543{-!

1548{-!

1544deriving instance Binary SynContext

1549deriving instance Binary SynContext

1545deriving instance NFData SynContext

1550deriving instance NFData SynContext

@@ -1547,7 +1552,7 @@ deriving instance NFData SynContext

1547

1552

1548data Syntax = Rule [SSymbol] PTerm SynContext

1553data Syntax = Rule [SSymbol] PTerm SynContext

1549 | DeclRule [SSymbol] [PDecl]

1554 | DeclRule [SSymbol] [PDecl]

1550− deriving Show

1555+ deriving (Show, Generic)

1551

1556

1552syntaxNames :: Syntax -> [Name]

1557syntaxNames :: Syntax -> [Name]

1553syntaxNames (Rule syms _ _) = mapMaybe ename syms

1558syntaxNames (Rule syms _ _) = mapMaybe ename syms

@@ -1570,7 +1575,7 @@ data SSymbol = Keyword Name

1570 | Binding Name

1575 | Binding Name

1571 | Expr Name

1576 | Expr Name

1572 | SimpleExpr Name

1577 | SimpleExpr Name

1573− deriving (Show, Eq)

1578+ deriving (Show, Eq, Generic)

1574

1579

1575

1580

1576{-!

1581{-!

@@ -1579,6 +1584,7 @@ deriving instance NFData SSymbol

1579!-}

1584!-}

1580

1585

1581newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }

1586newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }

1587+ deriving Generic

1582

1588

1583emptySyntaxRules :: SyntaxRules

1589emptySyntaxRules :: SyntaxRules

1584emptySyntaxRules = SyntaxRules []

1590emptySyntaxRules = SyntaxRules []

@@ -1632,7 +1638,7 @@ initDSL = DSL (PRef f [] (sUN ">>="))

1632

1638

1633data Using = UImplicit Name PTerm

1639data Using = UImplicit Name PTerm

1634 | UConstraint Name [Name]

1640 | UConstraint Name [Name]

1635− deriving (Show, Eq, Data, Typeable)

1641+ deriving (Show, Eq, Data, Generic, Typeable)

1636{-!

1642{-!

1637deriving instance Binary Using

1643deriving instance Binary Using

1638deriving instance NFData Using

1644deriving instance NFData Using

@@ -1656,7 +1662,7 @@ data SyntaxInfo = Syn {

1656 , syn_in_quasiquote :: Int

1662 , syn_in_quasiquote :: Int

1657 , syn_toplevel :: Bool

1663 , syn_toplevel :: Bool

1658 , withAppAllowed :: Bool

1664 , withAppAllowed :: Bool

1659− } deriving Show

1665+ } deriving (Show, Generic)

1660{-!

1666{-!

1661deriving instance NFData SyntaxInfo

1667deriving instance NFData SyntaxInfo

1662deriving instance Binary SyntaxInfo

1668deriving instance Binary SyntaxInfo

src/Idris/Colours.hs+3−1

@@ -1,3 +1,4 @@

1+{-# LANGUAGE DeriveGeneric #-}

1{-|

2{-|

2Module : Idris.Colours

3Module : Idris.Colours

3Description : Support for colours within Idris.

4Description : Support for colours within Idris.

@@ -14,6 +15,7 @@ module Idris.Colours (

14 , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise

15 , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise

15 ) where

16 ) where

18+import GHC.Generics (Generic)

17import System.Console.ANSI

19import System.Console.ANSI

18import System.IO (Handle)

20import System.IO (Handle)

@@ -37,7 +39,7 @@ data ColourTheme = ColourTheme { keywordColour :: IdrisColour

37 , promptColour :: IdrisColour

39 , promptColour :: IdrisColour

38 , postulateColour :: IdrisColour

40 , postulateColour :: IdrisColour

39 }

41 }

40− deriving (Eq, Show)

42+ deriving (Eq, Show, Generic)

42-- | Idris's default console colour theme

44-- | Idris's default console colour theme

43defaultTheme :: ColourTheme

45defaultTheme :: ColourTheme

src/Idris/Core/CaseTree.hs+6−4

@@ -18,7 +18,8 @@ allows casing on arbitrary terms, here we choose to maintain the distinction

18in order to allow for better optimisation opportunities.

20-}

21−{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

21+{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances,

22+ DeriveGeneric #-}

23module Idris.Core.CaseTree (

24module Idris.Core.CaseTree (

24 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo

25 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo

@@ -36,6 +37,7 @@ import Data.Maybe

36import Data.List hiding (partition)

37import Data.List hiding (partition)

37import qualified Data.List(partition)

38import qualified Data.List(partition)

38import Debug.Trace

39import Debug.Trace

40+import GHC.Generics (Generic)

40data CaseDef = CaseDef [Name] !SC [Term]

42data CaseDef = CaseDef [Name] !SC [Term]

41 deriving Show

43 deriving Show

@@ -45,14 +47,14 @@ data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first

45 | STerm !t

47 | STerm !t

46 | UnmatchedCase String -- ^ error message

48 | UnmatchedCase String -- ^ error message

47 | ImpossibleCase -- ^ already checked to be impossible

49 | ImpossibleCase -- ^ already checked to be impossible

48− deriving (Eq, Ord, Functor)

50+ deriving (Eq, Ord, Functor, Generic)

49{-!

51{-!

50deriving instance Binary SC'

52deriving instance Binary SC'

51deriving instance NFData SC'

53deriving instance NFData SC'

52!-}

54!-}

54data CaseType = Updatable | Shared

56data CaseType = Updatable | Shared

55− deriving (Eq, Ord, Show)

57+ deriving (Eq, Ord, Show, Generic)

57type SC = SC' Term

59type SC = SC' Term

@@ -61,7 +63,7 @@ data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

61 | ConstCase Const !(SC' t)

63 | ConstCase Const !(SC' t)

62 | SucCase Name !(SC' t)

64 | SucCase Name !(SC' t)

63 | DefaultCase !(SC' t)

65 | DefaultCase !(SC' t)

64− deriving (Show, Eq, Ord, Functor)

66+ deriving (Show, Eq, Ord, Functor, Generic)

65{-!

67{-!

66deriving instance Binary CaseAlt'

68deriving instance Binary CaseAlt'

67deriving instance NFData CaseAlt'

69deriving instance NFData CaseAlt'

src/Idris/Core/DeepSeq.hs+37−278

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

1{-|

2Module : Idris.Core.DeepSeq

3−Description : Marshalling information for TT.

3+Description : NFData instances for TT.

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

@@ -16,287 +16,46 @@ import Idris.Core.Evaluate

17import Control.DeepSeq

19−instance NFData Name where

19+instance NFData Name

20− rnf (UN x1) = rnf x1 `seq` ()

21− rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

22− rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

23− rnf (SN x1) = rnf x1 `seq` ()

24− rnf (SymRef x1) = rnf x1 `seq` ()

26−instance NFData Context where

21+instance NFData Context

27− rnf ctxt = rnf (next_tvar ctxt) `seq` rnf (definitions ctxt) `seq` ()

29-- | Forcing the contents of a context, for diagnosing and working

23-- | Forcing the contents of a context, for diagnosing and working

30-- around space leaks

24-- around space leaks

31forceDefCtxt :: Context -> Context

25forceDefCtxt :: Context -> Context

32forceDefCtxt (force -> !ctxt) = ctxt

26forceDefCtxt (force -> !ctxt) = ctxt

34−instance NFData NameOutput where

28+instance NFData NameOutput

35− rnf TypeOutput = ()

36− rnf FunOutput = ()

37− rnf DataOutput = ()

38− rnf MetavarOutput = ()

39− rnf PostulateOutput = ()

40−

41−instance NFData TextFormatting where

29+instance NFData TextFormatting

42− rnf BoldText = ()

43− rnf ItalicText = ()

44− rnf UnderlineText = ()

45−

46−instance NFData Ordering where

30+instance NFData Ordering

47− rnf LT = ()

48− rnf EQ = ()

49− rnf GT = ()

50−

51−instance NFData OutputAnnotation where

31+instance NFData OutputAnnotation

52− rnf (AnnName x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

53− rnf (AnnBoundName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

54− rnf (AnnConst x1) = rnf x1 `seq` ()

55− rnf (AnnData x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

56− rnf (AnnType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

57− rnf (AnnKeyword) = ()

58− rnf (AnnFC x) = rnf x `seq` ()

59− rnf (AnnTextFmt x) = rnf x `seq` ()

60− rnf (AnnLink x) = rnf x `seq` ()

61− rnf (AnnTerm x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

62− rnf (AnnSearchResult x1) = rnf x1 `seq` ()

63− rnf (AnnErr x1) = rnf x1 `seq` ()

64− rnf (AnnNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

65− rnf (AnnQuasiquote) = ()

66− rnf (AnnAntiquote) = ()

67−

68−instance NFData SpecialName where

32+instance NFData SpecialName

69− rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

70− rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

71− rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

72− rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

73− rnf (MethodN x1) = rnf x1 `seq` ()

74− rnf (CaseN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

75− rnf (ElimN x1) = rnf x1 `seq` ()

76− rnf (InstanceCtorN x1) = rnf x1 `seq` ()

77− rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

78−

79−instance NFData Universe where

33+instance NFData Universe

80− rnf NullType = ()

81− rnf UniqueType = ()

82− rnf AllTypes = ()

83−

84−instance NFData Raw where

34+instance NFData Raw

85− rnf (Var x1) = rnf x1 `seq` ()

86− rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

87− rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

88− rnf RType = ()

89− rnf (RUType x1) = rnf x1 `seq` ()

90− rnf (RConstant x1) = x1 `seq` ()

91−

92−instance NFData FC where

35+instance NFData FC

93− rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

94− rnf NoFC = ()

95− rnf (FileFC f) = rnf f `seq` ()

96−

97−instance NFData FC' where

36+instance NFData FC'

98− rnf (FC' fc) = rnf fc `seq` ()

99−

100−instance NFData Provenance where

37+instance NFData Provenance

101− rnf ExpectedType = ()

102− rnf InferredVal = ()

103− rnf GivenVal = ()

104− rnf (SourceTerm x1) = rnf x1 `seq` ()

105− rnf (TooManyArgs x1) = rnf x1 `seq` ()

106−

107−instance NFData UConstraint where

38+instance NFData UConstraint

108− rnf (ULT x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

109− rnf (ULE x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

110−

111−instance NFData ConstraintFC where

39+instance NFData ConstraintFC

112− rnf (ConstraintFC x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

113−

114−instance NFData Err where

40+instance NFData Err

115− rnf (Msg x1) = rnf x1 `seq` ()

116− rnf (InternalMsg x1) = rnf x1 `seq` ()

117− rnf (CantUnify x1 x2 x3 x4 x5 x6)

118− = rnf x1 `seq`

119− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

120− rnf (InfiniteUnify x1 x2 x3)

121− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

122− rnf (CantConvert x1 x2 x3)

123− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

124− rnf (UnifyScope x1 x2 x3 x4)

125− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

126− rnf (ElaboratingArg x1 x2 x3 x4)

127− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

128− rnf (CantInferType x1) = rnf x1 `seq` ()

129− rnf (CantMatch x1) = rnf x1 `seq` ()

130− rnf (ReflectionError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

131− rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

132− rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

133− rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

134− rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

135− rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

136− rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

137− rnf (CantIntroduce x1) = rnf x1 `seq` ()

138− rnf (TooManyArguments x1) = rnf x1 `seq` ()

139− rnf (WithFnType x1) = rnf x1 `seq` ()

140− rnf (NoSuchVariable x1) = rnf x1 `seq` ()

141− rnf (NoTypeDecl x1) = rnf x1 `seq` ()

142− rnf (NotInjective x1 x2 x3)

143− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

144− rnf (CantResolve x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

145− rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

146− rnf (CantResolveAlts x1) = rnf x1 `seq` ()

147− rnf (NoValidAlts x1) = rnf x1 `seq` ()

148− rnf (IncompleteTerm x1) = rnf x1 `seq` ()

149− rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

150− rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

151− rnf ProgramLineComment = ()

152− rnf (Inaccessible x1) = rnf x1 `seq` ()

153− rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

154− rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

155− rnf (AlreadyDefined x1) = rnf x1 `seq` ()

156− rnf (ProofSearchFail x1) = rnf x1 `seq` ()

157− rnf (NoRewriting x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

158− rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

159− rnf (Elaborating x1 x2 x3 x4)

160− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

161− rnf (ProviderError x1) = rnf x1 `seq` ()

162− rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163− rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

164− rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

165− rnf (RunningElabScript x1) = rnf x1 `seq` ()

166− rnf (ElabScriptStaging x1) = rnf x1 `seq` ()

167− rnf (FancyMsg x1) = rnf x1 `seq` ()

168−

169−instance NFData ErrorReportPart where

41+instance NFData ErrorReportPart

170− rnf (TextPart x1) = rnf x1 `seq` ()

171− rnf (TermPart x1) = rnf x1 `seq` ()

172− rnf (RawPart x1) = rnf x1 `seq` ()

173− rnf (NamePart x1) = rnf x1 `seq` ()

174− rnf (SubReport x1) = rnf x1 `seq` ()

175−

176−instance NFData ImplicitInfo where

42+instance NFData ImplicitInfo

177− rnf (Impl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

178−

179−instance (NFData b) => NFData (Binder b) where

43+instance (NFData b) => NFData (Binder b)

180− rnf (Lam x1) = rnf x1 `seq` ()

181− rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

182− rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

183− rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

184− rnf (Hole x1) = rnf x1 `seq` ()

185− rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

186− rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

187− rnf (PVar x1) = rnf x1 `seq` ()

188− rnf (PVTy x1) = rnf x1 `seq` ()

189−

190−instance NFData UExp where

44+instance NFData UExp

191− rnf (UVar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

192− rnf (UVal x1) = rnf x1 `seq` ()

193−

194−instance NFData NameType where

45+instance NFData NameType

195− rnf Bound = ()

196− rnf Ref = ()

197− rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

198− rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

199−

200−instance NFData NativeTy where

46+instance NFData NativeTy

201− rnf IT8 = ()

202− rnf IT16 = ()

203− rnf IT32 = ()

204− rnf IT64 = ()

205−

206−instance NFData IntTy where

47+instance NFData IntTy

207− rnf (ITFixed x1) = rnf x1 `seq` ()

208− rnf ITNative = ()

209− rnf ITBig = ()

210− rnf ITChar = ()

211−

212−instance NFData ArithTy where

48+instance NFData ArithTy

213− rnf (ATInt x1) = rnf x1 `seq` ()

214− rnf ATFloat = ()

215−

216−instance NFData Const where

49+instance NFData Const

217− rnf (I x1) = rnf x1 `seq` ()

50+instance (NFData a) => NFData (AppStatus a)

218− rnf (BI x1) = rnf x1 `seq` ()

219− rnf (Fl x1) = rnf x1 `seq` ()

220− rnf (Ch x1) = rnf x1 `seq` ()

221− rnf (Str x1) = rnf x1 `seq` ()

222− rnf (B8 x1) = rnf x1 `seq` ()

223− rnf (B16 x1) = rnf x1 `seq` ()

224− rnf (B32 x1) = rnf x1 `seq` ()

225− rnf (B64 x1) = rnf x1 `seq` ()

226− rnf (AType x1) = rnf x1 `seq` ()

227− rnf WorldType = ()

228− rnf TheWorld = ()

229− rnf StrType = ()

230− rnf VoidType = ()

231− rnf Forgot = ()

232−

233−instance (NFData n) => NFData (TT n) where

51+instance (NFData n) => NFData (TT n)

234− rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

235− rnf (V x1) = rnf x1 `seq` ()

236− rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

237− rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()

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

239− rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

240− rnf Erased = ()

241− rnf Impossible = ()

242− rnf (TType x1) = rnf x1 `seq` ()

243− rnf (UType _) = ()

244−

245−instance NFData Accessibility where

52+instance NFData Accessibility

246− rnf Public = ()

247− rnf Frozen = ()

248− rnf Hidden = ()

249− rnf Private = ()

250−

251−

252−instance NFData Totality where

53+instance NFData Totality

253− rnf (Total x1) = rnf x1 `seq` ()

254− rnf Productive = ()

255− rnf (Partial x1) = rnf x1 `seq` ()

256− rnf Unchecked = ()

257− rnf Generated = ()

258−

259−instance NFData PReason where

54+instance NFData PReason

260− rnf (Other x1) = rnf x1 `seq` ()

261− rnf Itself = ()

262− rnf NotCovering = ()

263− rnf NotPositive = ()

264− rnf (UseUndef x1) = rnf x1 `seq` ()

265− rnf ExternalIO = ()

266− rnf BelieveMe = ()

267− rnf (Mutual x1) = rnf x1 `seq` ()

268− rnf NotProductive = ()

269−

270−instance NFData MetaInformation where

55+instance NFData MetaInformation

271− rnf EmptyMI = ()

272− rnf (DataMI x1) = rnf x1 `seq` ()

273−

274−instance NFData Def where

56+instance NFData Def

275− rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

276− rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

277− rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

278− rnf (CaseOp x1 x2 x3 x4 x5 x6)

279− = rnf x1 `seq`

280− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

281−

282−instance NFData CaseInfo where

57+instance NFData CaseInfo

283− rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

284−

285−instance NFData CaseDefs where

58+instance NFData CaseDefs

286− rnf (CaseDefs x1 x2 x3 x4)

59+instance NFData CaseType

287− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

288−

289−instance (NFData t) => NFData (SC' t) where

60+instance (NFData t) => NFData (SC' t)

290− rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

291− rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

292− rnf (STerm x1) = rnf x1 `seq` ()

293− rnf (UnmatchedCase x1) = rnf x1 `seq` ()

294− rnf ImpossibleCase = ()

295−

296−instance (NFData t) => NFData (CaseAlt' t) where

61+instance (NFData t) => NFData (CaseAlt' t)

297− rnf (ConCase x1 x2 x3 x4)

298− = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()

299− rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()

300− rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()

301− rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()

302− rnf (DefaultCase x1) = rnf x1 `seq` ()

src/Idris/Core/Evaluate.hs+10−6

@@ -6,7 +6,7 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,

9− PatternGuards #-}

9+ PatternGuards, DeriveGeneric #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

@@ -31,6 +31,7 @@ import Control.Monad.State -- not Strict!

31import qualified Data.Binary as B

32import Data.Binary hiding (get, put)

33import Data.Maybe (listToMaybe)

34+import GHC.Generics (Generic)

35import Idris.Core.TT

36import Idris.Core.TT

36import Idris.Core.CaseTree

37import Idris.Core.CaseTree

@@ -700,6 +701,7 @@ data Def = Function !Type !Term

700 ![Either Term (Term, Term)] -- original definition

701 ![Either Term (Term, Term)] -- original definition

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

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

702 !CaseDefs

703 !CaseDefs

704+ deriving Generic

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

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

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

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

705

707

@@ -709,12 +711,14 @@ data CaseDefs = CaseDefs {

709 cases_inlined :: !([Name], SC),

711 cases_inlined :: !([Name], SC),

710 cases_runtime :: !([Name], SC)

712 cases_runtime :: !([Name], SC)

711 }

713 }

714+ deriving Generic

712

715

713data CaseInfo = CaseInfo {

716data CaseInfo = CaseInfo {

714 case_inlinable :: Bool, -- decided by machine

717 case_inlinable :: Bool, -- decided by machine

715 case_alwaysinline :: Bool, -- decided by %inline flag

718 case_alwaysinline :: Bool, -- decided by %inline flag

716 tc_dictionary :: Bool

719 tc_dictionary :: Bool

717 }

720 }

721+ deriving Generic

718

722

719{-!

723{-!

720deriving instance Binary Def

724deriving instance Binary Def

@@ -761,7 +765,7 @@ instance Show Def where

761-- Private => Programs can't access the name, doesn't reduce internally

765-- Private => Programs can't access the name, doesn't reduce internally

762

766

763data Accessibility = Hidden | Public | Frozen | Private

767data Accessibility = Hidden | Public | Frozen | Private

764− deriving (Eq, Ord)

768+ deriving (Eq, Ord, Generic)

765{-!

769{-!

766deriving instance NFData Accessibility

770deriving instance NFData Accessibility

767!-}

771!-}

@@ -780,7 +784,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

780 | Partial PReason

784 | Partial PReason

781 | Unchecked

785 | Unchecked

782 | Generated

786 | Generated

783− deriving Eq

787+ deriving (Eq, Generic)

784{-!

788{-!

785deriving instance NFData Totality

789deriving instance NFData Totality

786!-}

790!-}

@@ -788,7 +792,7 @@ deriving instance NFData Totality

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

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

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

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

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

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

791− deriving (Show, Eq)

795+ deriving (Show, Eq, Generic)

792{-!

796{-!

793deriving instance NFData PReason

797deriving instance NFData PReason

794!-}

798!-}

@@ -825,14 +829,14 @@ deriving instance Binary PReason

825data MetaInformation =

829data MetaInformation =

826 EmptyMI -- ^ No meta-information

830 EmptyMI -- ^ No meta-information

827 | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters

831 | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters

828− deriving (Eq, Show)

832+ deriving (Eq, Show, Generic)

829

833

830-- | Contexts used for global definitions and for proof state. They contain

834-- | Contexts used for global definitions and for proof state. They contain

831-- universe constraints and existing definitions.

835-- universe constraints and existing definitions.

832data Context = MkContext {

836data Context = MkContext {

833 next_tvar :: Int,

837 next_tvar :: Int,

834 definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)

838 definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)

835− } deriving Show

839+ } deriving (Show, Generic)

836

840

837

841

838-- | The initial empty context

842-- | The initial empty context

src/Idris/Core/TT.hs+28−27

@@ -23,7 +23,7 @@ TT is the core language of Idris. The language has:

23 programs with implicit syntax into fully explicit terms.

24-}

25{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,

26− DeriveDataTypeable, PatternGuards #-}

26+ DeriveDataTypeable, DeriveGeneric, PatternGuards #-}

27{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

28module Idris.Core.TT(

29 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

@@ -80,6 +80,7 @@ import qualified Data.Vector.Unboxed as V

80import qualified Data.Binary as B

81import Data.Binary hiding (get, put)

82import Foreign.Storable (sizeOf)

83+import GHC.Generics (Generic)

84import Numeric.IEEE (IEEE (identicalIEEE))

85import Numeric.IEEE (IEEE (identicalIEEE))

@@ -96,7 +97,7 @@ data FC = FC { _fc_fname :: String, -- ^ Filename

96 }

97 }

97 | NoFC -- ^ Locations for machine-generated terms

98 | NoFC -- ^ Locations for machine-generated terms

98 | FileFC { _fc_fname :: String } -- ^ Locations with file only

99 | FileFC { _fc_fname :: String } -- ^ Locations with file only

99− deriving (Data, Typeable, Ord)

100+ deriving (Data, Generic, Typeable, Ord)

100

101

101-- TODO: find uses and destroy them, doing this case analysis at call sites

102-- TODO: find uses and destroy them, doing this case analysis at call sites

102-- | Give a notion of filename associated with an FC

103-- | Give a notion of filename associated with an FC

@@ -159,7 +160,7 @@ instance Eq FC where

159 _ == _ = True

160 _ == _ = True

160

161

161-- | FC with equality

162-- | FC with equality

162−newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Typeable, Ord)

163+newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Generic, Typeable, Ord)

163

164

164instance Eq FC' where

165instance Eq FC' where

165 FC' fc == FC' fc' = fcEq fc fc'

166 FC' fc == FC' fc' = fcEq fc fc'

@@ -198,10 +199,10 @@ instance Show FC where

198 show (FileFC f) = f

199 show (FileFC f) = f

199

200

200-- | Output annotation for pretty-printed name - decides colour

201-- | Output annotation for pretty-printed name - decides colour

201−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)

202+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic)

202

203

203-- | Text formatting output

204-- | Text formatting output

204−data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)

205+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic)

205

206

206-- | Output annotations for pretty-printing

207-- | Output annotations for pretty-printing

207data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

208data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -227,7 +228,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

227 -- from that file.

228 -- from that file.

228 | AnnQuasiquote

229 | AnnQuasiquote

229 | AnnAntiquote

230 | AnnAntiquote

230− deriving (Show, Eq)

231+ deriving (Show, Eq, Generic)

231

232

232-- | Used for error reflection

233-- | Used for error reflection

233data ErrorReportPart = TextPart String

234data ErrorReportPart = TextPart String

@@ -235,7 +236,7 @@ data ErrorReportPart = TextPart String

235 | TermPart Term

236 | TermPart Term

236 | RawPart Raw

237 | RawPart Raw

237 | SubReport [ErrorReportPart]

238 | SubReport [ErrorReportPart]

238− deriving (Show, Eq, Data, Typeable)

239+ deriving (Show, Eq, Data, Generic, Typeable)

239

240

241

241data Provenance = ExpectedType

242data Provenance = ExpectedType

@@ -243,7 +244,7 @@ data Provenance = ExpectedType

243 | InferredVal

244 | InferredVal

244 | GivenVal

245 | GivenVal

245 | SourceTerm Term

246 | SourceTerm Term

246− deriving (Show, Eq, Data, Typeable)

247+ deriving (Show, Eq, Data, Generic, Typeable)

247{-!

248{-!

248deriving instance NFData Err

249deriving instance NFData Err

249deriving instance Binary Err

250deriving instance Binary Err

@@ -309,7 +310,7 @@ data Err' t

309 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

310 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

310 | ElabScriptStaging Name

311 | ElabScriptStaging Name

311 | FancyMsg [ErrorReportPart]

312 | FancyMsg [ErrorReportPart]

312− deriving (Eq, Functor, Data, Typeable)

313+ deriving (Eq, Functor, Data, Generic, Typeable)

313

314

314type Err = Err' Term

315type Err = Err' Term

315

316

@@ -467,7 +468,7 @@ data Name = UN !T.Text -- ^ User-provided name

467 | MN !Int !T.Text -- ^ Machine chosen names

468 | MN !Int !T.Text -- ^ Machine chosen names

468 | SN !SpecialName -- ^ Decorated function names

469 | SN !SpecialName -- ^ Decorated function names

469 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

470 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

470− deriving (Eq, Ord, Data, Typeable)

471+ deriving (Eq, Ord, Data, Generic, Typeable)

471

472

472txt :: String -> T.Text

473txt :: String -> T.Text

473txt = T.pack

474txt = T.pack

@@ -510,7 +511,7 @@ data SpecialName = WhereN !Int !Name !Name

510 | ElimN !Name

511 | ElimN !Name

511 | InstanceCtorN !Name

512 | InstanceCtorN !Name

512 | MetaN !Name !Name

513 | MetaN !Name !Name

513− deriving (Eq, Ord, Data, Typeable)

514+ deriving (Eq, Ord, Data, Generic, Typeable)

514{-!

515{-!

515deriving instance Binary SpecialName

516deriving instance Binary SpecialName

516deriving instance NFData SpecialName

517deriving instance NFData SpecialName

@@ -675,7 +676,7 @@ addAlist [] ctxt = ctxt

675addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

676addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

676

677

677data NativeTy = IT8 | IT16 | IT32 | IT64

678data NativeTy = IT8 | IT16 | IT32 | IT64

678− deriving (Show, Eq, Ord, Enum, Data, Typeable)

679+ deriving (Show, Eq, Ord, Enum, Data, Generic, Typeable)

679

680

680instance Pretty NativeTy OutputAnnotation where

681instance Pretty NativeTy OutputAnnotation where

681 pretty IT8 = text "Bits8"

682 pretty IT8 = text "Bits8"

@@ -684,7 +685,7 @@ instance Pretty NativeTy OutputAnnotation where

684 pretty IT64 = text "Bits64"

685 pretty IT64 = text "Bits64"

685

686

686data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

687data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

687− deriving (Show, Eq, Ord, Data, Typeable)

688+ deriving (Show, Eq, Ord, Data, Generic, Typeable)

688

689

689intTyName :: IntTy -> String

690intTyName :: IntTy -> String

690intTyName ITNative = "Int"

691intTyName ITNative = "Int"

@@ -693,7 +694,7 @@ intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

693intTyName (ITChar) = "Char"

694intTyName (ITChar) = "Char"

694

695

695data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723

696data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723

696− deriving (Show, Eq, Ord, Data, Typeable)

697+ deriving (Show, Eq, Ord, Data, Generic, Typeable)

697{-!

698{-!

698deriving instance NFData IntTy

699deriving instance NFData IntTy

699deriving instance NFData NativeTy

700deriving instance NFData NativeTy

@@ -725,7 +726,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

725 | AType ArithTy | StrType

726 | AType ArithTy | StrType

726 | WorldType | TheWorld

727 | WorldType | TheWorld

727 | VoidType | Forgot

728 | VoidType | Forgot

728− deriving (Ord, Data, Typeable)

729+ deriving (Ord, Data, Generic, Typeable)

729

730

730-- We need to compare Double using bit-pattern identity rather than

731-- We need to compare Double using bit-pattern identity rather than

731-- Haskell's Eq, which equates 0.0 and -0.0, leading to a

732-- Haskell's Eq, which equates 0.0 and -0.0, leading to a

@@ -821,7 +822,7 @@ constDocs (B64 w) = "The sixty-four-bit value 0x" ++

821constDocs prim = "Undocumented"

822constDocs prim = "Undocumented"

822

823

823data Universe = NullType | UniqueType | AllTypes

824data Universe = NullType | UniqueType | AllTypes

824− deriving (Eq, Ord, Data, Typeable)

825+ deriving (Eq, Ord, Data, Generic, Typeable)

825

826

826instance Show Universe where

827instance Show Universe where

827 show UniqueType = "UniqueType"

828 show UniqueType = "UniqueType"

@@ -834,7 +835,7 @@ data Raw = Var Name

834 | RType

835 | RType

835 | RUType Universe

836 | RUType Universe

836 | RConstant Const

837 | RConstant Const

837− deriving (Show, Eq, Data, Typeable)

838+ deriving (Show, Eq, Data, Generic, Typeable)

838

839

839instance Sized Raw where

840instance Sized Raw where

840 size (Var name) = 1

841 size (Var name) = 1

@@ -854,7 +855,7 @@ deriving instance NFData Raw

854

855

855data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,

856data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,

856 machine_gen :: Bool }

857 machine_gen :: Bool }

857− deriving (Show, Eq, Ord, Data, Typeable)

858+ deriving (Show, Eq, Ord, Data, Generic, Typeable)

858

859

859{-!

860{-!

860deriving instance Binary ImplicitInfo

861deriving instance Binary ImplicitInfo

@@ -906,7 +907,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

906 -- that make up pattern-match clauses)

907 -- that make up pattern-match clauses)

907 | PVTy { binderTy :: !b }

908 | PVTy { binderTy :: !b }

908 -- ^ The type of a pattern binding

909 -- ^ The type of a pattern binding

909− deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)

910+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)

910{-!

911{-!

911deriving instance Binary Binder

912deriving instance Binary Binder

912deriving instance NFData Binder

913deriving instance NFData Binder

@@ -951,7 +952,7 @@ internalNS = "(internal)"

951-- | Universe expressions for universe checking

952-- | Universe expressions for universe checking

952data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate

953data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate

953 | UVal Int -- ^ explicit universe level

954 | UVal Int -- ^ explicit universe level

954− deriving (Eq, Ord, Data, Typeable)

955+ deriving (Eq, Ord, Data, Generic, Typeable)

955{-!

956{-!

956deriving instance NFData UExp

957deriving instance NFData UExp

957!-}

958!-}

@@ -969,11 +970,11 @@ instance Show UExp where

969-- | Universe constraints

970-- | Universe constraints

970data UConstraint = ULT UExp UExp -- ^ Strictly less than

971data UConstraint = ULT UExp UExp -- ^ Strictly less than

971 | ULE UExp UExp -- ^ Less than or equal to

972 | ULE UExp UExp -- ^ Less than or equal to

972− deriving (Eq, Ord, Data, Typeable)

973+ deriving (Eq, Ord, Data, Generic, Typeable)

973

974

974data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

975data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

975 ufc :: FC }

976 ufc :: FC }

976− deriving (Show, Data, Typeable)

977+ deriving (Show, Data, Generic, Typeable)

977

978

978instance Eq ConstraintFC where

979instance Eq ConstraintFC where

979 x == y = uconstraint x == uconstraint y

980 x == y = uconstraint x == uconstraint y

@@ -991,7 +992,7 @@ data NameType = Bound

991 | Ref

992 | Ref

992 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

993 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

993 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

994 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

994− deriving (Show, Ord, Data, Typeable)

995+ deriving (Show, Ord, Data, Generic, Typeable)

995{-!

996{-!

996deriving instance Binary NameType

997deriving instance Binary NameType

997deriving instance NFData NameType

998deriving instance NFData NameType

@@ -1013,7 +1014,7 @@ instance Eq NameType where

1013data AppStatus n = Complete

1014data AppStatus n = Complete

1014 | MaybeHoles

1015 | MaybeHoles

1015 | Holes [n]

1016 | Holes [n]

1016− deriving (Eq, Ord, Functor, Data, Typeable, Show)

1017+ deriving (Eq, Ord, Functor, Data, Generic, Typeable, Show)

1017

1018

1018-- | Terms in the core language. The type parameter is the type of

1019-- | Terms in the core language. The type parameter is the type of

1019-- identifiers used for bindings and explicit named references;

1020-- identifiers used for bindings and explicit named references;

@@ -1031,7 +1032,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

1031 | Impossible -- ^ special case for totality checking

1032 | Impossible -- ^ special case for totality checking

1032 | TType UExp -- ^ the type of types at some level

1033 | TType UExp -- ^ the type of types at some level

1033 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

1034 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

1034− deriving (Ord, Functor, Data, Typeable)

1035+ deriving (Ord, Functor, Data, Generic, Typeable)

1035{-!

1036{-!

1036deriving instance Binary TT

1037deriving instance Binary TT

1037deriving instance NFData TT

1038deriving instance NFData TT

@@ -1096,7 +1097,7 @@ data DataOpt = Codata -- ^ Set if the the data-type is coinductive

1096 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

1097 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

1097 | DefaultCaseFun -- ^ Set if a case function should be generated for data type

1098 | DefaultCaseFun -- ^ Set if a case function should be generated for data type

1098 | DataErrRev

1099 | DataErrRev

1099− deriving (Show, Eq)

1100+ deriving (Show, Eq, Generic)

1100

1101

1101type DataOpts = [DataOpt]

1102type DataOpts = [DataOpt]

1102

1103

@@ -1105,7 +1106,7 @@ data TypeInfo = TI { con_names :: [Name],

1105 data_opts :: DataOpts,

1106 data_opts :: DataOpts,

1106 param_pos :: [Int],

1107 param_pos :: [Int],

1107 mutual_types :: [Name] }

1108 mutual_types :: [Name] }

1108− deriving Show

1109+ deriving (Show, Generic)

1109{-!

1110{-!

1110deriving instance Binary TypeInfo

1111deriving instance Binary TypeInfo

1111deriving instance NFData TypeInfo

1112deriving instance NFData TypeInfo

src/Idris/DeepSeq.hs+59−680

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

1{-|

2Module : Idris.DeepSeq

3−Description : Specify how to marshall Idris' IR.

3+Description : NFData instances for Idris' types

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

@@ -26,323 +26,10 @@ import Control.DeepSeq

26import qualified Cheapskate.Types as CT

27import qualified Idris.Docstrings as D

29−instance NFData a => NFData (D.Docstring a) where

29+-- These types don't have Generic instances

30− rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()

31−

32instance NFData CT.Options where

30instance NFData CT.Options where

33 rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

31 rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

35−instance NFData ConsoleWidth where

36− rnf InfinitelyWide = ()

37− rnf (ColsWide x) = rnf x `seq` ()

38− rnf AutomaticWidth = ()

39−

40−instance NFData PrimFn where

41− rnf (LPlus x) = rnf x `seq` ()

42− rnf (LMinus x) = rnf x `seq` ()

43− rnf (LTimes x) = rnf x `seq` ()

44− rnf (LUDiv x) = rnf x `seq` ()

45− rnf (LSDiv x) = rnf x `seq` ()

46− rnf (LURem x) = rnf x `seq` ()

47− rnf (LSRem x) = rnf x `seq` ()

48− rnf (LAnd x) = rnf x `seq` ()

49− rnf (LOr x) = rnf x `seq` ()

50− rnf (LXOr x) = rnf x `seq` ()

51− rnf (LCompl x) = rnf x `seq` ()

52− rnf (LSHL x) = rnf x `seq` ()

53− rnf (LLSHR x) = rnf x `seq` ()

54− rnf (LASHR x) = rnf x `seq` ()

55− rnf (LEq x) = rnf x `seq` ()

56− rnf (LLt x) = rnf x `seq` ()

57− rnf (LLe x) = rnf x `seq` ()

58− rnf (LGt x) = rnf x `seq` ()

59− rnf (LGe x) = rnf x `seq` ()

60− rnf (LSLt x) = rnf x `seq` ()

61− rnf (LSLe x) = rnf x `seq` ()

62− rnf (LSGt x) = rnf x `seq` ()

63− rnf (LSGe x) = rnf x `seq` ()

64− rnf (LSExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

65− rnf (LZExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

66− rnf (LTrunc x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

67− rnf (LStrConcat) = ()

68− rnf (LStrLt) = ()

69− rnf (LStrEq) = ()

70− rnf (LStrLen) = ()

71− rnf (LIntFloat x) = rnf x `seq` ()

72− rnf (LFloatInt x) = rnf x `seq` ()

73− rnf (LIntStr x) = rnf x `seq` ()

74− rnf (LStrInt x) = rnf x `seq` ()

75− rnf (LFloatStr) = ()

76− rnf (LStrFloat) = ()

77− rnf (LChInt x) = rnf x `seq` ()

78− rnf (LIntCh x) = rnf x `seq` ()

79− rnf (LBitCast x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

80− rnf (LFExp) = ()

81− rnf (LFLog) = ()

82− rnf (LFSin) = ()

83− rnf (LFCos) = ()

84− rnf (LFTan) = ()

85− rnf (LFASin) = ()

86− rnf (LFACos) = ()

87− rnf (LFATan) = ()

88− rnf (LFSqrt) = ()

89− rnf (LFFloor) = ()

90− rnf (LFCeil) = ()

91− rnf (LFNegate) = ()

92− rnf (LStrHead) = ()

93− rnf (LStrTail) = ()

94− rnf (LStrCons) = ()

95− rnf (LStrIndex) = ()

96− rnf (LStrRev) = ()

97− rnf (LStrSubstr) = ()

98− rnf (LReadStr) = ()

99− rnf (LWriteStr) = ()

100− rnf (LSystemInfo) = ()

101− rnf (LFork) = ()

102− rnf (LPar) = ()

103− rnf (LExternal x) = rnf x `seq` ()

104− rnf (LNoOp) = ()

105−

106−instance NFData SyntaxRules where

107− rnf (SyntaxRules xs) = rnf xs `seq` ()

108−

109−instance NFData DynamicLib where

110− rnf (Lib x _) = rnf x `seq` ()

111−

112−

113−instance NFData Opt where

114− rnf (Filename str) = rnf str `seq` ()

115− rnf (Quiet) = ()

116− rnf (NoBanner) = ()

117− rnf (ColourREPL bool) = rnf bool `seq` ()

118− rnf (Idemode) = ()

119− rnf (IdemodeSocket) = ()

120− rnf (ShowLoggingCats) = ()

121− rnf (ShowLibs) = ()

122− rnf (ShowLibdir) = ()

123− rnf (ShowIncs) = ()

124− rnf (ShowPkgs) = ()

125− rnf (NoBasePkgs) = ()

126− rnf (NoPrelude) = ()

127− rnf (NoBuiltins) = ()

128− rnf (NoREPL) = ()

129− rnf (OLogging i) = rnf i `seq` ()

130− rnf (OLogCats cs) = rnf cs `seq` ()

131− rnf (Output str) = rnf str `seq` ()

132− rnf (Interface) = ()

133− rnf (TypeCase) = ()

134− rnf (TypeInType) = ()

135− rnf (DefaultTotal) = ()

136− rnf (DefaultPartial) = ()

137− rnf (WarnPartial) = ()

138− rnf (WarnReach) = ()

139− rnf (EvalTypes) = ()

140− rnf (DesugarNats) = ()

141− rnf (NoCoverage) = ()

142− rnf (ErrContext) = ()

143− rnf (ShowImpl) = ()

144− rnf (Verbose) = ()

145− rnf (Port str) = rnf str `seq` ()

146− rnf (IBCSubDir str) = rnf str `seq` ()

147− rnf (ImportDir str) = rnf str `seq` ()

148− rnf (PkgBuild str) = rnf str `seq` ()

149− rnf (PkgInstall str) = rnf str `seq` ()

150− rnf (PkgClean str) = rnf str `seq` ()

151− rnf (PkgCheck str) = rnf str `seq` ()

152− rnf (PkgREPL str) = rnf str `seq` ()

153− rnf (PkgMkDoc str) = rnf str `seq` ()

154− rnf (PkgTest str) = rnf str `seq` ()

155− rnf (PkgIndex fp) = rnf fp `seq` ()

156− rnf (WarnOnly) = ()

157− rnf (Pkg str) = rnf str `seq` ()

158− rnf (BCAsm str) = rnf str `seq` ()

159− rnf (DumpDefun str) = rnf str `seq` ()

160− rnf (DumpCases str) = rnf str `seq` ()

161− rnf (UseCodegen cg) = rnf cg `seq` ()

162− rnf (CodegenArgs str) = rnf str `seq` ()

163− rnf (OutputTy ot) = rnf ot `seq` ()

164− rnf (Extension le) = rnf le `seq` ()

165− rnf (InterpretScript str) = rnf str `seq` ()

166− rnf (EvalExpr str) = rnf str `seq` ()

167− rnf (TargetTriple str) = rnf str `seq` ()

168− rnf (TargetCPU str) = rnf str `seq` ()

169− rnf (OptLevel i) = rnf i `seq` ()

170− rnf (AddOpt o) = rnf o `seq` ()

171− rnf (RemoveOpt o) = rnf o `seq` ()

172− rnf (Client str) = rnf str `seq` ()

173− rnf (ShowOrigErr) = ()

174− rnf (AutoWidth) = ()

175− rnf (AutoSolve) = ()

176− rnf (UseConsoleWidth cw) = rnf cw `seq` ()

177− rnf DumpHighlights = ()

178− rnf NoElimDeprecationWarnings = ()

179− rnf NoOldTacticDeprecationWarnings = ()

180−

181−

182−instance NFData TIData where

183− rnf TIPartial = ()

184− rnf (TISolution xs) = rnf xs `seq` ()

185−

186−instance NFData IOption where

187− rnf (IOption

188− opt_logLevel

189− opt_logcats

190− opt_typecase

191− opt_typeintype

192− opt_coverage

193− opt_showimp

194− opt_errContext

195− opt_repl

196− opt_verbose

197− opt_nobanner

198− opt_quiet

199− opt_codegen

200− opt_outputTy

201− opt_ibcsubdir

202− opt_importdirs

203− opt_triple

204− opt_cpu

205− opt_cmdline

206− opt_origerr

207− opt_autoSolve

208− opt_autoImport

209− opt_optimise

210− opt_printdepth

211− opt_evaltypes

212− opt_desugarnats

213− opt_autoimpls) =

214− rnf opt_logLevel

215− `seq` rnf opt_typecase

216− `seq` rnf opt_typeintype

217− `seq` rnf opt_coverage

218− `seq` rnf opt_showimp

219− `seq` rnf opt_errContext

220− `seq` rnf opt_repl

221− `seq` rnf opt_verbose

222− `seq` rnf opt_nobanner

223− `seq` rnf opt_quiet

224− `seq` rnf opt_codegen

225− `seq` rnf opt_outputTy

226− `seq` rnf opt_ibcsubdir

227− `seq` rnf opt_importdirs

228− `seq` rnf opt_triple

229− `seq` rnf opt_cpu

230− `seq` rnf opt_cmdline

231− `seq` rnf opt_origerr

232− `seq` rnf opt_autoSolve

233− `seq` rnf opt_autoImport

234− `seq` rnf opt_optimise

235− `seq` rnf opt_printdepth

236− `seq` rnf opt_evaltypes

237− `seq` rnf opt_desugarnats

238− `seq` rnf opt_autoimpls

239− `seq` ()

240−

241−instance NFData LanguageExt where

242− rnf TypeProviders = ()

243− rnf ErrorReflection = ()

244−

245−instance NFData Optimisation where

246− rnf PETransform = ()

247−

248−instance NFData ColourTheme where

249− rnf (ColourTheme keywordColour

250− boundVarColour

251− implicitColour

252− functionColour

253− typeColour

254− dataColour

255− promptColour

256− postulateColour) =

257− rnf keywordColour

258− `seq` rnf boundVarColour

259− `seq` rnf implicitColour

260− `seq` rnf functionColour

261− `seq` rnf typeColour

262− `seq` rnf dataColour

263− `seq` rnf promptColour

264− `seq` rnf postulateColour

265− `seq` ()

266−

267−instance NFData IdrisColour where

268− rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

269−

270−instance NFData OutputType where

271− rnf Raw = ()

272− rnf Object = ()

273− rnf Executable = ()

274−

275−instance NFData IBCWrite where

276− rnf (IBCFix fixDecl) = rnf fixDecl `seq` ()

277− rnf (IBCImp name) = rnf name `seq` ()

278− rnf (IBCStatic name) = rnf name `seq` ()

279− rnf (IBCClass name) = rnf name `seq` ()

280− rnf (IBCInstance b1 b2 n1 n2) = rnf b1 `seq` rnf b2 `seq` rnf n1 `seq` rnf n2 `seq` ()

281− rnf (IBCDSL name) = rnf name `seq` ()

282− rnf (IBCData name) = rnf name `seq` ()

283− rnf (IBCOpt name) = rnf name `seq` ()

284− rnf (IBCMetavar name) = rnf name `seq` ()

285− rnf (IBCSyntax syntax) = rnf syntax `seq` ()

286− rnf (IBCKeyword string) = rnf string `seq` ()

287− rnf (IBCImport imp) = rnf imp `seq` ()

288− rnf (IBCImportDir filePath) = rnf filePath `seq` ()

289− rnf (IBCObj codegen filePath) = rnf codegen `seq` rnf filePath `seq` ()

290− rnf (IBCLib codegen string) = rnf codegen `seq` rnf string `seq` ()

291− rnf (IBCCGFlag codegen string) = rnf codegen `seq` rnf string `seq` ()

292− rnf (IBCDyLib string) = rnf string `seq` ()

293− rnf (IBCHeader codegen string) = rnf codegen `seq` rnf string `seq` ()

294− rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()

295− rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()

296− rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()

297− rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` ()

298− rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()

299− rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()

300− rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()

301− rnf (IBCErrRev terms) = rnf terms `seq` ()

302− rnf (IBCCG name) = rnf name `seq` ()

303− rnf (IBCDoc name) = rnf name `seq` ()

304− rnf (IBCCoercion name) = rnf name `seq` ()

305− rnf (IBCDef name) = rnf name `seq` ()

306− rnf (IBCNameHint names) = rnf names `seq` ()

307− rnf (IBCLineApp filePath int pTerm) = rnf filePath `seq` rnf int `seq` rnf pTerm `seq` ()

308− rnf (IBCErrorHandler name) = rnf name `seq` ()

309− rnf (IBCFunctionErrorHandler n1 n2 n3) = rnf n1 `seq` rnf n2 `seq` rnf n3 `seq` ()

310− rnf (IBCPostulate name) = rnf name `seq` ()

311− rnf (IBCExtern extern) = rnf extern `seq` ()

312− rnf (IBCTotCheckErr fc string) = rnf fc `seq` rnf string `seq` ()

313− rnf (IBCParsedRegion fc) = rnf fc `seq` ()

314− rnf (IBCModDocs name) = rnf name `seq` ()

315− rnf (IBCUsage usage) = rnf usage `seq` ()

316− rnf (IBCExport name) = rnf name `seq` ()

317− rnf (IBCAutoHint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

318− rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

319− rnf (IBCRecord x) = rnf x `seq` ()

320− rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

321− rnf (IBCConstraint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

322−

323−

324−instance NFData a => NFData (D.Block a) where

325− rnf (D.Para lines) = rnf lines `seq` ()

326− rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()

327− rnf (D.Blockquote bs) = rnf bs `seq` ()

328− rnf (D.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()

329− rnf (D.CodeBlock attr txt tm) = rnf attr `seq` rnf txt `seq` ()

330− rnf (D.HtmlBlock txt) = rnf txt `seq` ()

331− rnf D.HRule = ()

332−

333−instance NFData a => NFData (D.Inline a) where

334− rnf (D.Str txt) = rnf txt `seq` ()

335− rnf D.Space = ()

336− rnf D.SoftBreak = ()

337− rnf D.LineBreak = ()

338− rnf (D.Emph xs) = rnf xs `seq` ()

339− rnf (D.Strong xs) = rnf xs `seq` ()

340− rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()

341− rnf (D.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()

342− rnf (D.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()

343− rnf (D.Entity a) = rnf a `seq` ()

344− rnf (D.RawHtml x) = rnf x `seq` ()

345−

346instance NFData CT.ListType where

33instance NFData CT.ListType where

347 rnf (CT.Bullet c) = rnf c `seq` ()

34 rnf (CT.Bullet c) = rnf c `seq` ()

348 rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()

35 rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()

@@ -354,373 +41,65 @@ instance NFData CT.NumWrapper where

354 rnf CT.PeriodFollowing = ()

41 rnf CT.PeriodFollowing = ()

355 rnf CT.ParenFollowing = ()

42 rnf CT.ParenFollowing = ()

356

357−instance NFData DocTerm where

44+instance NFData DynamicLib where

358− rnf Unchecked = ()

45+ rnf (Lib x _) = rnf x `seq` ()

359− rnf (Checked x1) = rnf x1 `seq` ()

360− rnf (Example x1) = rnf x1 `seq` ()

361− rnf (Failing x1) = rnf x1 `seq` ()

362−

363−-- All generated by 'derive'

364−

365−instance NFData SizeChange where

366− rnf Smaller = ()

367− rnf Same = ()

368− rnf Bigger = ()

369− rnf Unknown = ()

370−

371−instance NFData FnInfo where

372− rnf (FnInfo x1) = rnf x1 `seq` ()

373−

374−instance NFData Codegen where

375− rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

376− rnf Bytecode = ()

377−

378−instance NFData IRFormat where

379− rnf _ = ()

380−

381−instance NFData LogCat where

382− rnf _ = ()

383−

384−instance NFData CGInfo where

385− rnf (CGInfo x1 x2 x3)

386− = rnf x1 `seq`

387− rnf x2 `seq` rnf x3 `seq` ()

388−

389−instance NFData Fixity where

390− rnf (Infixl x1) = rnf x1 `seq` ()

391− rnf (Infixr x1) = rnf x1 `seq` ()

392− rnf (InfixN x1) = rnf x1 `seq` ()

393− rnf (PrefixN x1) = rnf x1 `seq` ()

394−

395−instance NFData FixDecl where

396− rnf (Fix x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

397−

398−instance NFData Static where

399− rnf Static = ()

400− rnf Dynamic = ()

401−

402−instance NFData ArgOpt where

403− rnf _ = ()

404−

405−instance NFData Plicity where

406− rnf (Imp x1 x2 x3 x4 x5)

407− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

408− rnf (Exp x1 x2 x3)

409− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

410− rnf (Constraint x1 x2)

411− = rnf x1 `seq` rnf x2 `seq` ()

412− rnf (TacImp x1 x2 x3)

413− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

414−

415−instance NFData FnOpt where

416− rnf Inlinable = ()

417− rnf TotalFn = ()

418− rnf PartialFn = ()

419− rnf CoveringFn = ()

420− rnf Coinductive = ()

421− rnf AssertTotal = ()

422− rnf Dictionary = ()

423− rnf Implicit = ()

424− rnf NoImplicit = ()

425− rnf (CExport x1) = rnf x1 `seq` ()

426− rnf ErrorHandler = ()

427− rnf ErrorReverse = ()

428− rnf Reflection = ()

429− rnf (Specialise x1) = rnf x1 `seq` ()

430− rnf Constructor = ()

431− rnf AutoHint = ()

432− rnf PEGenerated = ()

433−

434−instance NFData DataOpt where

435− rnf Codata = ()

436− rnf DefaultEliminator = ()

437− rnf DefaultCaseFun = ()

438− rnf DataErrRev = ()

439−

440−instance (NFData t) => NFData (PDecl' t) where

441− rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

442− rnf (PTy x1 x2 x3 x4 x5 x6 x7 x8)

443− = rnf x1 `seq`

444− rnf x2 `seq`

445− rnf x3 `seq`

446− rnf x4 `seq`

447− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

448− rnf (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)

449− = rnf x1 `seq`

450− rnf x2 `seq`

451− rnf x3 `seq`

452− rnf x4 `seq`

453− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

454− rnf (PClauses x1 x2 x3 x4)

455− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

456− rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

457− rnf (PData x1 x2 x3 x4 x5 x6)

458− = rnf x1 `seq`

459− rnf x2 `seq`

460− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

461− rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

462− rnf (POpenInterfaces x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

463− rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

464− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

465− = rnf x1 `seq`

466− rnf x2 `seq`

467− rnf x3 `seq`

468− rnf x4 `seq`

469− rnf x5 `seq`

470− rnf x6 `seq`

471− rnf x7 `seq`

472− rnf x8 `seq`

473− rnf x9 `seq`

474− rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

475− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11 x12)

476− = rnf x1 `seq`

477− rnf x2 `seq`

478− rnf x3 `seq`

479− rnf x4 `seq`

480− rnf x5 `seq`

481− rnf x6 `seq`

482− rnf x7 `seq`

483− rnf x8 `seq`

484− rnf x9 `seq`

485− rnf x10 `seq`

486− rnf x11 `seq` rnf x12 `seq` ()

487− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

488− = rnf x1 `seq`

489− rnf x2 `seq`

490− rnf x3 `seq`

491− rnf x4 `seq`

492− rnf x5 `seq`

493− rnf x6 `seq`

494− rnf x7 `seq`

495− rnf x8 `seq`

496− rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()

497− rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

498− rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

499− rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

500− rnf (PDirective x1) = ()

501− rnf (PProvider x1 x2 x3 x4 x5 x6)

502− = rnf x1 `seq`

503− rnf x2 `seq`

504− rnf x3 `seq`

505− rnf x4 `seq`

506− rnf x5 `seq` rnf x6 `seq` ()

507− rnf (PTransform x1 x2 x3 x4)

508− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

509− rnf (PRunElabDecl x1 x2 x3)

510− = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

511−

512−instance NFData t => NFData (ProvideWhat' t) where

513− rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

514− rnf (ProvPostulate tm) = rnf tm `seq` ()

515−

516−instance NFData PunInfo where

517− rnf x = x `seq` ()

518−

519−instance (NFData t) => NFData (PClause' t) where

520− rnf (PClause x1 x2 x3 x4 x5 x6)

521− = rnf x1 `seq`

522− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

523− rnf (PWith x1 x2 x3 x4 x5 x6 x7)

524− = rnf x1 `seq`

525− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

526− rnf (PClauseR x1 x2 x3 x4)

527− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

528− rnf (PWithR x1 x2 x3 x4 x5)

529− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

530−

531−instance (NFData t) => NFData (PData' t) where

532− rnf (PDatadecl x1 x2 x3 x4)

533− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

534− rnf (PLaterdecl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

535−

536−instance NFData PTerm where

537− rnf (PQuote x1) = rnf x1 `seq` ()

538− rnf (PRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

539− rnf (PInferRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

540− rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

541− rnf (PLam _ x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

542− rnf (PPi x1 x2 x3 x4 x5)

543− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

544− rnf (PLet _ x1 x2 x3 x4 x5)

545− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

546− rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

547− rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

548− rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

549− rnf (PWithApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

550− rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

551− rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

552− rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

553− rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

554− rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

555− rnf (PResolveTC x1) = rnf x1 `seq` ()

556− rnf (PRewrite x1 x2 x3 x4 x5)

557− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

558− rnf (PPair x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` x5 `seq` ()

559− rnf (PDPair x1 x2 x3 x4 x5 x6)

560− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` x6 `seq` ()

561− rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

562− rnf (PAlternative x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

563− rnf (PHidden x1) = rnf x1 `seq` ()

564− rnf (PType fc) = rnf fc `seq` ()

565− rnf (PUniverse _) = ()

566− rnf (PGoal x1 x2 x3 x4)

567− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

568− rnf (PConstant x1 x2) = x1 `seq` x2 `seq` ()

569− rnf Placeholder = ()

570− rnf (PDoBlock x1) = rnf x1 `seq` ()

571− rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

572− rnf (PReturn x1) = rnf x1 `seq` ()

573− rnf (PMetavar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

574− rnf (PProof x1) = rnf x1 `seq` ()

575− rnf (PTactics x1) = rnf x1 `seq` ()

576− rnf (PElabError x1) = rnf x1 `seq` ()

577− rnf PImpossible = ()

578− rnf (PCoerced x1) = rnf x1 `seq` ()

579− rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

580− rnf (PUnifyLog x1) = rnf x1 `seq` ()

581− rnf (PNoImplicits x1) = rnf x1 `seq` ()

582− rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

583− rnf (PUnquote x1) = rnf x1 `seq` ()

584− rnf (PQuoteName x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

585− rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

586− rnf (PConstSugar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

587−

588−instance NFData PAltType where

589− rnf (ExactlyOne x1) = rnf x1 `seq` ()

590− rnf FirstSuccess = ()

591− rnf TryImplicit = ()

592−

593−instance (NFData t) => NFData (PTactic' t) where

594− rnf (Intro x1) = rnf x1 `seq` ()

595− rnf Intros = ()

596− rnf (Focus x1) = rnf x1 `seq` ()

597− rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

598− rnf (Rewrite x1) = rnf x1 `seq` ()

599− rnf DoUnify = ()

600− rnf (Induction x1) = rnf x1 `seq` ()

601− rnf (CaseTac x1) = rnf x1 `seq` ()

602− rnf (Equiv x1) = rnf x1 `seq` ()

603− rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

604− rnf (MatchRefine x1) = rnf x1 `seq` ()

605− rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

606− rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

607− rnf (Exact x1) = rnf x1 `seq` ()

608− rnf Compute = ()

609− rnf Trivial = ()

610− rnf TCInstance = ()

611− rnf (ProofSearch r r1 r2 x1 x2 x3)

612− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

613− rnf Solve = ()

614− rnf Attack = ()

615− rnf ProofState = ()

616− rnf ProofTerm = ()

617− rnf Undo = ()

618− rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

619− rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

620− rnf (ApplyTactic x1) = rnf x1 `seq` ()

621− rnf (ByReflection x1) = rnf x1 `seq` ()

622− rnf (Reflect x1) = rnf x1 `seq` ()

623− rnf (Fill x1) = rnf x1 `seq` ()

624− rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

625− rnf Qed = ()

626− rnf Abandon = ()

627− rnf (TCheck x1) = rnf x1 `seq` ()

628− rnf (TEval x1) = rnf x1 `seq` ()

629− rnf (TDocStr x1) = x1 `seq` ()

630− rnf (TSearch x1) = rnf x1 `seq` ()

631− rnf Skip = ()

632− rnf (TFail x1) = rnf x1 `seq` ()

633− rnf SourceFC = ()

634− rnf Unfocus = ()

635−

636−instance (NFData t) => NFData (PDo' t) where

637− rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

638− rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

639− rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

640− rnf (DoLet x1 x2 x3 x4 x5)

641− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

642− rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

643−

644−instance (NFData t) => NFData (PArg' t) where

645− rnf (PImp x1 x2 x3 x4 x5)

646− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

647− rnf (PExp x1 x2 x3 x4)

648− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

649− rnf (PConstraint x1 x2 x3 x4)

650− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

651− rnf (PTacImplicit x1 x2 x3 x4 x5)

652− = rnf x1 `seq`

653− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

654−

655−instance NFData ClassInfo where

656− rnf (CI x1 x2 x3 x4 x5 x6 x7)

657− = rnf x1 `seq`

658− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

659−

660−instance NFData RecordInfo where

661− rnf (RI x1 x2 x3)

662− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

663−

664−instance NFData OptInfo where

665− rnf (Optimise x1 x2)

666− = rnf x1 `seq` rnf x2 `seq` ()

667−

668−instance NFData TypeInfo where

669− rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

670−

671−instance (NFData t) => NFData (DSL' t) where

672− rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

673− = rnf x1 `seq`

674− rnf x2 `seq`

675− rnf x3 `seq`

676− rnf x4 `seq`

677− rnf x5 `seq`

678− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

679−

680−instance NFData SynContext where

681− rnf PatternSyntax = ()

682− rnf TermSyntax = ()

683− rnf AnySyntax = ()

684−

685−instance NFData Syntax where

686− rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

687− rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

688−

689−instance NFData SSymbol where

690− rnf (Keyword x1) = rnf x1 `seq` ()

691− rnf (Symbol x1) = rnf x1 `seq` ()

692− rnf (Binding x1) = rnf x1 `seq` ()

693− rnf (Expr x1) = rnf x1 `seq` ()

694− rnf (SimpleExpr x1) = rnf x1 `seq` ()

695−

696−instance NFData Using where

697− rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

698− rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

699

700−instance NFData SyntaxInfo where

47+instance NFData IdrisColour where

701− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

48+ rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

702− = rnf x1 `seq`

703− rnf x2 `seq`

704− rnf x3 `seq`

705− rnf x4 `seq`

706− rnf x5 `seq`

707− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()

708

50+-- Handle doesn't have an NFData instance

709instance NFData OutputMode where

51instance NFData OutputMode where

710− rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

52+ rnf (RawOutput x) = ()

711 rnf (IdeMode x y) = rnf x `seq` ()

53 rnf (IdeMode x y) = rnf x `seq` ()

712

55+instance NFData a => NFData (D.Docstring a)

56+instance NFData ConsoleWidth

57+instance NFData PrimFn

58+instance NFData SyntaxRules

59+instance NFData Opt

60+instance NFData TIData

61+instance NFData IOption

62+instance NFData LanguageExt

63+instance NFData Optimisation

64+instance NFData ColourTheme

65+instance NFData OutputType

66+instance NFData IBCWrite

67+instance NFData a => NFData (D.Block a)

68+instance NFData a => NFData (D.Inline a)

69+instance NFData DocTerm

70+instance NFData SizeChange

71+instance NFData FnInfo

72+instance NFData Codegen

73+instance NFData IRFormat

74+instance NFData LogCat

75+instance NFData CGInfo

76+instance NFData Fixity

77+instance NFData FixDecl

78+instance NFData Static

79+instance NFData ArgOpt

80+instance NFData Plicity

81+instance NFData FnOpt

82+instance NFData DataOpt

83+instance NFData Directive

84+instance (NFData t) => NFData (PDecl' t)

85+instance NFData t => NFData (ProvideWhat' t)

86+instance NFData PunInfo

87+instance (NFData t) => NFData (PClause' t)

88+instance (NFData t) => NFData (PData' t)

89+instance NFData PTerm

90+instance NFData PAltType

91+instance (NFData t) => NFData (PTactic' t)

92+instance (NFData t) => NFData (PDo' t)

93+instance (NFData t) => NFData (PArg' t)

94+instance NFData ClassInfo

95+instance NFData RecordInfo

96+instance NFData OptInfo

97+instance NFData TypeInfo

98+instance (NFData t) => NFData (DSL' t)

99+instance NFData SynContext

100+instance NFData Syntax

101+instance NFData SSymbol

102+instance NFData Using

103+instance NFData SyntaxInfo

713−instance NFData DefaultTotality where

104+instance NFData DefaultTotality

714− rnf DefaultCheckingTotal = ()

715− rnf DefaultCheckingPartial = ()

716− rnf DefaultCheckingCovering = ()

717−

718−instance NFData IState where

105+instance NFData IState

719− rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

720− x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

721− x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

722− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77)

723− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

724− rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

725− rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

726− rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` rnf x77 `seq` ()

src/Idris/Docstrings.hs+6−6

@@ -6,7 +6,7 @@ License : BSD3

6Maintainer : The Idris Community.

7-}

9−{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

9+{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11module Idris.Docstrings (

12 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring

@@ -30,7 +30,7 @@ import Data.Foldable (Foldable)

30import Data.Traversable (Traversable)

31import qualified Data.Sequence as S

33−import Control.DeepSeq (NFData(..))

33+import GHC.Generics (Generic)

35import Text.Blaze.Html (Html)

@@ -39,7 +39,7 @@ data DocTerm = Unchecked

39 | Checked Term

40 | Example Term

41 | Failing Err

42− deriving Show

42+ deriving (Show, Generic)

44-- | Render a term in the documentation

45renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation

@@ -53,7 +53,7 @@ renderDocTerm pp norm (Failing err) src = annotate (AnnErr err) $ text src

53-- | Representation of Idris's inline documentation. The type paramter

54-- represents the type of terms that are associated with code blocks.

55data Docstring a = DocString CT.Options (Blocks a)

56− deriving (Show, Functor, Foldable, Traversable)

56+ deriving (Show, Functor, Foldable, Traversable, Generic)

58type Blocks a = S.Seq (Block a)

@@ -65,7 +65,7 @@ data Block a = Para (Inlines a)

65 | CodeBlock CT.CodeAttr T.Text a

66 | HtmlBlock T.Text

67 | HRule

68− deriving (Show, Functor, Foldable, Traversable)

68+ deriving (Show, Functor, Foldable, Traversable, Generic)

70data Inline a = Str T.Text

71 | Space

@@ -78,7 +78,7 @@ data Inline a = Str T.Text

78 | Image (Inlines a) T.Text T.Text

79 | Entity T.Text

80 | RawHtml T.Text

81− deriving (Show, Functor, Foldable, Traversable)

81+ deriving (Show, Functor, Foldable, Traversable, Generic)

83type Inlines a = S.Seq (Inline a)