8073344 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

166 put t

167 put (CantMatch t) = do putWord8 35

168 put t

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

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

170− put x1

170+ put x1

171− put x2

171+ put x2

172− put x3

172+ put x3

173 put (NoEliminator s t) = do putWord8 37

174 put s

175 put t

176 put (InvalidTCArg n t) = do putWord8 38

177 put n

178 put t

179+ put (ElabScriptStuck x1) = do putWord8 39

180+ put x1

179

181

180 get = do i <- getWord8

182 get = do i <- getWord8

181 case i of

183 case i of

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

234 36 -> do x1 <- get

236 36 -> do x1 <- get

235 x2 <- get

237 x2 <- get

236 x3 <- get

238 x3 <- get

237− return (ElabDebug x1 x2 x3)

239+ return (ElabScriptDebug x1 x2 x3)

238 37 -> do x1 <- get

240 37 -> do x1 <- get

239 x2 <- get

241 x2 <- get

240 return (NoEliminator x1 x2)

242 return (NoEliminator x1 x2)

241 38 -> do x1 <- get

243 38 -> do x1 <- get

242 x2 <- get

244 x2 <- get

243 return (InvalidTCArg x1 x2)

245 return (InvalidTCArg x1 x2)

246+ 39 -> do x1 <- get

247+ return (ElabScriptStuck x1)

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

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

245----- Generated by 'derive'

249----- Generated by 'derive'

246

250

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

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

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

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

107 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` ()

109

110

110instance NFData ImplicitInfo where

111instance NFData ImplicitInfo where

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

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

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

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

788 recoverableErr (ProofSearchFail _) = False

789 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

790 recoverableErr (At _ e) = recoverableErr e

791− recoverableErr (ElabDebug _ _ _) = False

791+ recoverableErr (ElabScriptDebug _ _ _) = False

792 recoverableErr _ = True

793

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

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

872 hs <- get_holes

873 holeInfo <- mapM getHoleInfo hs

874 loadState

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

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

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

877 getHoleInfo h = do focus h

878 g <- goal

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

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

180 | LoadingFailed String (Err' t)

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

182 | ReflectionFailed String (Err' t)

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

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

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

185+ | ElabScriptStuck t

185 deriving (Eq, Functor, Data, Typeable)

186 deriving (Eq, Functor, Data, Typeable)

186

187

187type Err = Err' Term

188type Err = Err' Term

src/Idris/Delaborate.hs+4−1

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

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

381 indented (pprintErr' i err) <>

382 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) =

384 text "Elaboration halted." <>

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

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

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

401 pprintTT ns (binderTy b) <>

402 line <>

403 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?"

404

407

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

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

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

409-- 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

1818 Nothing -> debugElaborator Nothing

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

1820 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

1822

1823-- Running tactics directly

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