[Agda-dev] Debugging non-TCM code

[Jesper Cockx]

Dear Agda developers,

I'm working on fixing some of the current issues with --rewriting (#2433
and #2573) but I'm running into a bit of a problem. For my fix, I needed to
generalize some functions from TCM to an arbitrary monad satisfying some
constraints, so they can also be used in ReduceM. Specifically, I have made
the following changes to the type signatures:

-getModuleParameterSub :: MonadTCM tcm => ModuleName -> tcm Substitution
+getModuleParameterSub :: (Functor m, ReadTCState m) => ModuleName -> m
Substitution

-freeVarsToApply :: QName -> TCM Args
+freeVarsToApply :: (Functor m, HasConstInfo m, ReadTCState m, MonadReader
TCEnv m) => QName -> m Args

-moduleParamsToApply :: ModuleName -> TCM Args
+moduleParamsToApply :: (Functor m, Applicative m, MonadReader TCEnv m,
ReadTCState m)
+                    => ModuleName -> m Args

However, this means these functions can no longer contain any debug
statements. For TCM we have reportSDoc and for ReduceM we have traceSDoc,
but these cannot be joined into one typeclass since they have different
calling conventions (traceSDoc takes a continuation as an additional
argument). So I'm at a loss at how to debug my code. There are also other
occasions where you're neither in TCM nor in ReduceM but you still want to
add some debug statements, but this seems to be impossible with the current
infrastructure.

Does anyone have an idea how to get out of this dilemma?

-- Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20170712/39fc868b/attachment.html>