f417e6c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2203 from david-christiansen/wip/tactical

Better errors on stuck reflected elaborators

commitf417e6c948ccf033f717a101c39d5ba308b0924a authorDavid Christiansen <david@davidchristiansen.dk> dateWed 29 Apr 2015, 10:28 (11 years ago) parent2c505fc 8073344

6 files changed+20−11

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+9−5 src/Idris/Core/DeepSeq.hs+2−1 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/TT.hs+2−1 src/Idris/Delaborate.hs+4−1 src/Idris/Elab/Term.hs+1−1

src/Idris/Core/Binary.hs+9−5

@@ -166,16 +166,18 @@ instance Binary a => Binary (Err' a) where

166166 put t

167167 put (CantMatch t) = do putWord8 35

168168 put t

169− put (ElabDebug x1 x2 x3) = do putWord8 36

170− put x1

171− put x2

172− put x3

169+ put (ElabScriptDebug x1 x2 x3) = do putWord8 36

170+ put x1

171+ put x2

172+ put x3

173173 put (NoEliminator s t) = do putWord8 37

174174 put s

175175 put t

176176 put (InvalidTCArg n t) = do putWord8 38

177177 put n

178178 put t

179+ put (ElabScriptStuck x1) = do putWord8 39

180+ put x1

179181

180182 get = do i <- getWord8

181183 case i of

@@ -234,13 +236,15 @@ instance Binary a => Binary (Err' a) where

234236 36 -> do x1 <- get

235237 x2 <- get

236238 x3 <- get

237− return (ElabDebug x1 x2 x3)

239+ return (ElabScriptDebug x1 x2 x3)

238240 37 -> do x1 <- get

239241 x2 <- get

240242 return (NoEliminator x1 x2)

241243 38 -> do x1 <- get

242244 x2 <- get

243245 return (InvalidTCArg x1 x2)

246+ 39 -> do x1 <- get

247+ return (ElabScriptStuck x1)

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

245249----- Generated by 'derive'

246250

src/Idris/Core/DeepSeq.hs+2−1

@@ -105,7 +105,8 @@ instance NFData Err where

105105 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

106106 rnf (ProviderError x1) = rnf x1 `seq` ()

107107 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

108− rnf (ElabDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

108+ rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

109+ rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

109110

110111instance NFData ImplicitInfo where

111112 rnf (Impl x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+2−2

@@ -788,7 +788,7 @@ try' t1 t2 proofSearch

788788 recoverableErr (ProofSearchFail _) = False

789789 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

790790 recoverableErr (At _ e) = recoverableErr e

791− recoverableErr (ElabDebug _ _ _) = False

791+ recoverableErr (ElabScriptDebug _ _ _) = False

792792 recoverableErr _ = True

793793

794794tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

@@ -872,7 +872,7 @@ debugElaborator msg = do ps <- fmap proof get

872872 hs <- get_holes

873873 holeInfo <- mapM getHoleInfo hs

874874 loadState

875− lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) holeInfo

875+ lift . Error $ ElabScriptDebug msg (getProofTerm (pterm ps)) holeInfo

876876 where getHoleInfo :: Name -> Elab' aux (Name, Type, [(Name, Binder Type)])

877877 getHoleInfo h = do focus h

878878 g <- goal

src/Idris/Core/TT.hs+2−1

@@ -180,8 +180,9 @@ data Err' t

180180 | LoadingFailed String (Err' t)

181181 | ReflectionError [[ErrorReportPart]] (Err' t)

182182 | ReflectionFailed String (Err' t)

183− | ElabDebug (Maybe String) t [(Name, t, [(Name, Binder t)])]

183+ | ElabScriptDebug (Maybe String) t [(Name, t, [(Name, Binder t)])]

184184 -- ^ User-specified message, proof term, goals with context (first goal is focused)

185+ | ElabScriptStuck t

185186 deriving (Eq, Functor, Data, Typeable)

186187

187188type Err = Err' Term

src/Idris/Delaborate.hs+4−1

@@ -380,7 +380,7 @@ pprintErr' i (ReflectionFailed msg err) =

380380 text "When attempting to perform error reflection, the following internal error occurred:" <>

381381 indented (pprintErr' i err) <>

382382 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

383−pprintErr' i (ElabDebug msg tm holes) =

383+pprintErr' i (ElabScriptDebug msg tm holes) =

384384 text "Elaboration halted." <>

385385 maybe empty (indented . text) msg <> line <>

386386 text "Term: " <> indented (pprintTT [] tm) <> line <>

@@ -401,6 +401,9 @@ pprintErr' i (ElabDebug msg tm holes) =

401401 pprintTT ns (binderTy b) <>

402402 line <>

403403 ppAssumptions (n:ns) rest

404+pprintErr' i (ElabScriptStuck tm) =

405+ text "Can't run" <+> pprintTT [] tm <+> text "as an elaborator script." <$>

406+ text "Is it a stuck term?"

404407

405408-- | Make sure the machine invented names are shown helpfully to the user, so

406409-- that any names which differ internally also differ visibly

src/Idris/Elab/Term.hs+1−1

@@ -1818,7 +1818,7 @@ runTactical fc env tm = do tm' <- eval tm

18181818 Nothing -> debugElaborator Nothing

18191819 Just (Constant (Str m)) -> debugElaborator (Just m)

18201820 Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x

1821− runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1821+ runTacTm x = lift . tfail $ ElabScriptStuck x

18221822

18231823-- Running tactics directly

18241824-- if a tactic adds unification problems, return an error