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

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

compare with master

unifiedsplit

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

190 put e

191 put (ElabScriptStaging n) = do putWord8 43

192 put n

193−

193+ put (FancyMsg xs) = do putWord8 44

194+ put xs

194 get = do i <- getWord8

195 get = do i <- getWord8

195 case i of

196 case i of

196 0 -> fmap Msg get

197 0 -> fmap Msg get

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

262 41 -> fmap NoValidAlts get

263 41 -> fmap NoValidAlts get

263 42 -> fmap RunningElabScript get

264 42 -> fmap RunningElabScript get

264 43 -> fmap ElabScriptStaging get

265 43 -> fmap ElabScriptStaging get

266+ 44 -> fmap FancyMsg get

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

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

266----- Generated by 'derive'

268----- Generated by 'derive'

267

269

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

160

161

161instance NFData ErrorReportPart where

162instance NFData ErrorReportPart where

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

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

src/Idris/Core/TT.hs+1

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

298 | ElabScriptStuck t

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

300 | ElabScriptStaging Name

301+ | FancyMsg [ErrorReportPart]

301 deriving (Eq, Functor, Data, Typeable)

302 deriving (Eq, Functor, Data, Typeable)

302

303

303type Err = Err' Term

304type Err = Err' Term

src/Idris/Delaborate.hs+2

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

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

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

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

510+pprintErr' i (FancyMsg parts) =

511+ fillSep (map (showPart i) parts)

510

512

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

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

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

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

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 123

43+ibcVersion = 124

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/ProofSearch.hs+14−5

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

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

197 return True

198 TType _ -> return True

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

199+ _ -> typeNotSearchable ty

200

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

202 conReady as n

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

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

283 $ checkConstructor ist others

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

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

285+ Nothing -> typeNotSearchable t

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

286+ _ -> typeNotSearchable t

287

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

289 -- applying them too

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

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

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

328 aty <- goal

329− psRec True d locs tys) newhs

329+ psRec True d locs tys) newhs

330 solve

331

332 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+ _ -> []

334

343

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

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

336-- index to help pick a relevant constructor

345-- index to help pick a relevant constructor