8ea27ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove a needless 'nub'

When generating cases for coverage checking, it doesn't help to remove any repeats. Profiling shows that this achieves very little other than taking a long time to run, and there are very few repeats anyway, so any benefits are massively outweighed by the cost.

commit8ea27ae997ea1e4214ce47ad228bd7c35a891459 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 19 Nov 2016, 19:18 (10 years ago) parent7813874

4 files changed+21−18

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+9−9 src/Idris/Core/TT.hs+4−4 src/Idris/Coverage.hs+6−4 src/Idris/Elab/Clause.hs+2−1

src/Idris/AbsSyntaxTree.hs+9−9

@@ -586,7 +586,7 @@ instance Ord FixDecl where

586586

587587

588588data Static = Static | Dynamic

589− deriving (Show, Eq, Data, Generic, Typeable)

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

590590{-!

591591deriving instance Binary Static

592592!-}

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

609609 , pstatic :: Static

610610 , pscript :: PTerm

611611 }

612− deriving (Show, Eq, Data, Generic, Typeable)

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

613613

614614{-!

615615deriving instance Binary Plicity

@@ -1040,7 +1040,7 @@ updateNs ns t = mapPT updateRef t

10401040data PunInfo = IsType

10411041 | IsTerm

10421042 | TypeOrTerm

1043− deriving (Eq, Show, Data, Typeable, Generic)

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

10441044

10451045-- | High level language terms

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

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

11061106 | PConstSugar FC PTerm

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

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

1109− deriving (Eq, Data, Typeable, Generic)

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

11101110

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

11121112 | FirstSuccess

11131113 | TryImplicit

1114− deriving (Eq, Data, Generic, Typeable)

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

11151115

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

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

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

12301230 | TFail [ErrorReportPart]

12311231 | Qed | Abandon

12321232 | SourceFC

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

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

12341234{-!

12351235deriving instance Binary PTactic'

12361236!-}

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

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

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

12781278 | DoLetP FC t t

1279− deriving (Eq, Functor, Data, Generic, Typeable)

1279+ deriving (Eq, Ord, Functor, Data, Generic, Typeable)

12801280{-!

12811281deriving instance Binary PDo'

12821282!-}

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

13161316 , getScript :: t

13171317 , getTm :: t

13181318 }

1319− deriving (Show, Eq, Functor, Data, Generic, Typeable)

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

13201320

13211321data ArgOpt = AlwaysShow

13221322 | HideDisplay

13231323 | InaccessibleArg

13241324 | UnknownImp

1325− deriving (Show, Eq, Data, Generic, Typeable)

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

13261326

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

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

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

@@ -234,7 +234,7 @@ data ErrorReportPart = TextPart String

234234 | TermPart Term

235235 | RawPart Raw

236236 | SubReport [ErrorReportPart]

237− deriving (Show, Eq, Data, Generic, Typeable)

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

238238

239239

240240data Provenance = ExpectedType

@@ -242,7 +242,7 @@ data Provenance = ExpectedType

242242 | InferredVal

243243 | GivenVal

244244 | SourceTerm Term

245− deriving (Show, Eq, Data, Generic, Typeable)

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

246246{-!

247247deriving instance Binary Err

248248!-}

@@ -307,7 +307,7 @@ data Err' t

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

308308 | ElabScriptStaging Name

309309 | FancyMsg [ErrorReportPart]

310− deriving (Eq, Functor, Data, Generic, Typeable)

310+ deriving (Eq, Ord, Functor, Data, Generic, Typeable)

311311

312312type Err = Err' Term

313313

@@ -820,7 +820,7 @@ data Raw = Var Name

820820 | RType

821821 | RUType Universe

822822 | RConstant Const

823− deriving (Show, Eq, Data, Generic, Typeable)

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

824824

825825instance Sized Raw where

826826 size (Var name) = 1

src/Idris/Coverage.hs+6−4

@@ -96,7 +96,9 @@ genClauses fc n xs given

9696 let tryclauses = mkClauses parg all_args

9797 logCoverage 3 $ show (length tryclauses) ++ " initially to check"

9898 logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)

99− let new = filter (noMatch i) (nub tryclauses)

99+

100+ let xsdelab = map (\x -> stripUnmatchable i (delab' i x True True)) xs

101+ let new = filter (noMatch i xsdelab) tryclauses

100102 logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"

101103 logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

102104-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

@@ -127,9 +129,9 @@ genClauses fc n xs given

127129

128130 -- Return whether the given clause matches none of the input clauses

129131 -- (xs)

130− noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of

131− Right ms -> False

132− Left miss -> True) xs

132+ noMatch i xs tm = all (\x -> case matchClause i x tm of

133+ Right ms -> False

134+ Left miss -> True) xs

133135

134136

135137 mergePlaceholders :: PTerm -> PTerm -> PTerm

src/Idris/Elab/Clause.hs+2−1

@@ -582,7 +582,8 @@ checkPossible info fc tcgen fname lhs_in

582582 OK _ -> return True

583583 err -> return False

584584 -- if it's a recoverable error, the case may become possible

585− Error err -> if tcgen then return (recoverableCoverage ctxt err)

585+ Error err -> do logLvl 10 "Impossible case"

586+ if tcgen then return (recoverableCoverage ctxt err)

586587 else return (validCoverageCase ctxt err ||

587588 recoverableCoverage ctxt err)

588589