83ca4ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Friendlier error on proof search failure

Now, proof search doesn't throw an INTERNAL ERROR when called on a goal that isn't a datatype. Instead, it provides the following message: Prover error: Attempted to find an element of type Nat -> Bool using proof search, but proof search only works on datatypes with constructors. When the goal is a function type, which seems to be a likely reason why it would fail, it adds the sentence: In particular, function types are not supported. Additionally, a variant of the Msg constructor for errors, called FancyMsg, was introduced. This allows the use of the ErrorReportPart type to define custom messages. Fixes #2713.

commit83ca4aebecf06f9e4978997984d6044c77f88bee authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 11 Oct 2015, 00:55 (11 years ago) parent4f68012

6 files changed+22−7

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+3−1 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+2 src/Idris/IBC.hs+1−1 src/Idris/ProofSearch.hs+14−5

src/Idris/Core/Binary.hs+3−1

@@ -190,7 +190,8 @@ instance Binary a => Binary (Err' a) where

190190 put e

191191 put (ElabScriptStaging n) = do putWord8 43

192192 put n

193−

193+ put (FancyMsg xs) = do putWord8 44

194+ put xs

194195 get = do i <- getWord8

195196 case i of

196197 0 -> fmap Msg get

@@ -262,6 +263,7 @@ instance Binary a => Binary (Err' a) where

262263 41 -> fmap NoValidAlts get

263264 42 -> fmap RunningElabScript get

264265 43 -> fmap ElabScriptStaging get

266+ 44 -> fmap FancyMsg get

265267 _ -> error "Corrupted binary data for Err'"

266268----- Generated by 'derive'

267269

src/Idris/Core/DeepSeq.hs+1

@@ -157,6 +157,7 @@ instance NFData Err where

157157 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

158158 rnf (RunningElabScript x1) = rnf x1 `seq` ()

159159 rnf (ElabScriptStaging x1) = rnf x1 `seq` ()

160+ rnf (FancyMsg x1) = rnf x1 `seq` ()

160161

161162instance NFData ErrorReportPart where

162163 rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+1

@@ -298,6 +298,7 @@ data Err' t

298298 | ElabScriptStuck t

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

300300 | ElabScriptStaging Name

301+ | FancyMsg [ErrorReportPart]

301302 deriving (Eq, Functor, Data, Typeable)

302303

303304type Err = Err' Term

src/Idris/Delaborate.hs+2

@@ -507,6 +507,8 @@ pprintErr' i (ElabScriptStaging n) =

507507 text "Can't run elaboration script because it contains pattern matching that has not yet been elaborated." <$>

508508 text "Try lifting the script to a top-level definition." <$>

509509 text "In particular, the problem is caused by:" <+> annName n

510+pprintErr' i (FancyMsg parts) =

511+ fillSep (map (showPart i) parts)

510512

511513showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

512514showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 123

43+ibcVersion = 124

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+14−5

@@ -196,7 +196,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

196196 Nothing -> -- local variable, go for it

197197 return True

198198 TType _ -> return True

199− _ -> fail "Not a data type"

199+ _ -> typeNotSearchable ty

200200

201201 conReady :: [Term] -> Name -> ElabD Bool

202202 conReady as n

@@ -282,8 +282,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

282282 -- since that's part of the point...)

283283 $ checkConstructor ist others

284284 tryCons d locs tys (others ++ getFn d fn)

285− Nothing -> fail "Not a data type"

286− _ -> fail "Not a data type"

285+ Nothing -> typeNotSearchable t

286+ _ -> typeNotSearchable t

287287

288288 -- if there are local variables which have a function type, try

289289 -- applying them too

@@ -326,11 +326,20 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

326326 let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)

327327 mapM_ (\ (_, h) -> do focus h

328328 aty <- goal

329− psRec True d locs tys) newhs

329+ psRec True d locs tys) newhs

330330 solve

331331

332332 isImp (PImp p _ _ _ _) = (True, p)

333− isImp arg = (False, priority arg)

333+ isImp arg = (False, priority arg)

334+

335+ typeNotSearchable ty =

336+ lift $ tfail $ FancyMsg $

337+ [TextPart "Attempted to find an element of type",

338+ TermPart ty,

339+ TextPart "using proof search, but proof search only works on datatypes with constructors."] ++

340+ case ty of

341+ (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

342+ _ -> []

334343

335344-- In interactive mode, only search for things if there is some

336345-- index to help pick a relevant constructor