git.iko.soy/Idris-dev
on master help sign in
Show hole context and goals in elaborator debug
75a9c8fDavid Raymond Christiansen
src/Idris/Core/Elaborate.hs+10−1
compare with master
unifiedsplit
@@ -842,7 +842,16 @@ prunStateT pmax zok ps x s
842
842
843debugElaborator :: Maybe String -> Elab' aux a
843debugElaborator :: Maybe String -> Elab' aux a
844debugElaborator msg = do ps <- fmap proof get
844debugElaborator msg = do ps <- fmap proof get
845+ saveState -- so we don't need to remember the hole order
846+ hs <- get_holes
847+ holeInfo <- mapM getHoleInfo hs
848+ loadState
845− lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) [] -- TODO hole info
849+ lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) holeInfo
850+ where getHoleInfo :: Name -> Elab' aux (Name, Type, [(Name, Binder Type)])
851+ getHoleInfo h = do focus h
852+ g <- goal
853+ env <- get_env
854+ return (h, g, env)
846
855
847qshow :: Fails -> String
856qshow :: Fails -> String
848qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)
857qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)
src/Idris/Delaborate.hs+9−4
@@ -339,11 +339,16 @@ pprintErr' i (ReflectionFailed msg err) =
339 text "When attempting to perform error reflection, the following internal error occurred:" <>
339 text "When attempting to perform error reflection, the following internal error occurred:" <>
340 indented (pprintErr' i err) <>
340 indented (pprintErr' i err) <>
341 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
341 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
342−pprintErr' i (ElabDebug mstr tm holes) =
342+pprintErr' i (ElabDebug msg tm holes) =
343 text "Elaboration halted." <>
343 text "Elaboration halted." <>
344− maybe empty (indented . text) mstr <>
344+ maybe empty (indented . text) msg <> line <>
345− text "Term: TODO PRINT TERM" <>
345+ text "Term: " <> pprintTerm' i [] (delab i tm) <> line <>
346− text "Holes: TODO PRINT AND PRESERVE"
346+ text "Holes:" <>
347+ (indented . vsep . flip map holes)
348+ (\(hn, goal, env) ->
349+ vsep (flip map env (\(n, b) -> annName' n (show n) <+> text ":" <+> pprintTerm' i [] (delab i (binderTy b)))) <> -- TODO: nested binders
350+ line <> text "----------------------------------" <> line <>
351+ annName' hn (show hn) <+> text ":" <+> pprintTerm' i (zip (map fst env) (repeat True)) (delab i goal) <> line)
347
352
348-- | Make sure the machine invented names are shown helpfully to the user, so
353-- | Make sure the machine invented names are shown helpfully to the user, so
349-- that any names which differ internally also differ visibly
354-- that any names which differ internally also differ visibly