git.iko.soy/Idris-dev
on master help sign in
Show hole context and goals in elaborator debug
commit75a9c8fdefcd9557601e0d9e6d8bc78b81620271 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 16 Mar 2015, 16:09 (12 years ago) parent8858c1a
2 files changed+19−5
compare with master
unifiedsplit
src/Idris/Core/Elaborate.hs+10−1 src/Idris/Delaborate.hs+9−4
src/Idris/Core/Elaborate.hs+10−1
@@ -842,7 +842,16 @@ prunStateT pmax zok ps x s
842842
843843debugElaborator :: Maybe String -> Elab' aux a
844844debugElaborator msg = do ps <- fmap proof get
845− lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) [] -- TODO hole info
845+ saveState -- so we don't need to remember the hole order
846+ hs <- get_holes
847+ holeInfo <- mapM getHoleInfo hs
848+ loadState
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)
846855
847856qshow :: Fails -> String
848857qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)
src/Idris/Delaborate.hs+9−4
@@ -339,11 +339,16 @@ pprintErr' i (ReflectionFailed msg err) =
339339 text "When attempting to perform error reflection, the following internal error occurred:" <>
340340 indented (pprintErr' i err) <>
341341 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) =
343343 text "Elaboration halted." <>
344− maybe empty (indented . text) mstr <>
345− text "Term: TODO PRINT TERM" <>
346− text "Holes: TODO PRINT AND PRESERVE"
344+ maybe empty (indented . text) msg <> line <>
345+ text "Term: " <> pprintTerm' i [] (delab i tm) <> line <>
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)
347352
348353-- | Make sure the machine invented names are shown helpfully to the user, so
349354-- that any names which differ internally also differ visibly