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

git.iko.soy/Idris-dev

on master help sign in

Remove a needless 'nub'

8ea27aeEdwin Brady10 years ago

src/Idris/AbsSyntaxTree.hs+9−9

compare with master

unifiedsplit

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

586

587

588data Static = Static | Dynamic

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

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

590{-!

591deriving instance Binary Static

592!-}

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

609 , pstatic :: Static

610 , pscript :: PTerm

611 }

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

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

613

614{-!

615deriving instance Binary Plicity

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

1040data PunInfo = IsType

1041 | IsTerm

1042 | TypeOrTerm

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

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

1044

1045-- | High level language terms

1046data 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

1106 | PConstSugar FC PTerm

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

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

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

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

1110

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

1112 | FirstSuccess

1113 | TryImplicit

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

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

1115

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

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

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

1230 | TFail [ErrorReportPart]

1231 | Qed | Abandon

1232 | SourceFC

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

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

1234{-!

1235deriving instance Binary PTactic'

1236!-}

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

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

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

1278 | DoLetP FC t t

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

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

1280{-!

1281deriving instance Binary PDo'

1282!-}

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

1316 , getScript :: t

1317 , getTm :: t

1318 }

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

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

1320

1321data ArgOpt = AlwaysShow

1322 | HideDisplay

1323 | InaccessibleArg

1324 | UnknownImp

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

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

1326

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

1328 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

234 | TermPart Term

235 | RawPart Raw

236 | SubReport [ErrorReportPart]

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

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

238

239

240data Provenance = ExpectedType

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

242 | InferredVal

243 | GivenVal

244 | SourceTerm Term

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

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

246{-!

247deriving instance Binary Err

248!-}

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

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

308 | ElabScriptStaging Name

309 | FancyMsg [ErrorReportPart]

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

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

311

312type Err = Err' Term

313

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

820 | RType

821 | RUType Universe

822 | RConstant Const

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

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

824

825instance Sized Raw where

826 size (Var name) = 1

src/Idris/Coverage.hs+6−4

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

96 let tryclauses = mkClauses parg all_args

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

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

99+

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

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

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

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

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

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

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

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

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

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

127

129

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

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

129 -- (xs)

131 -- (xs)

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

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

131− Right ms -> False

133+ Right ms -> False

132− Left miss -> True) xs

134+ Left miss -> True) xs

133

135

134

136

135 mergePlaceholders :: PTerm -> PTerm -> PTerm

137 mergePlaceholders :: PTerm -> PTerm -> PTerm

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

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

582 OK _ -> return True

583 err -> return False

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

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

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

586+ if tcgen then return (recoverableCoverage ctxt err)

586 else return (validCoverageCase ctxt err ||

587 else return (validCoverageCase ctxt err ||

587 recoverableCoverage ctxt err)

588 recoverableCoverage ctxt err)

588

589