[Agda-dev] Debugging non-TCM code

[Andreas Abel]

Dear Jesper,

I have thought about this problem before, but never implemented the 
solution.  It is similar to benchmarking non-TCM code.

   Agda.Utils.Benchmark

There is a monad

   MonadBench

that lets us access benchmark-related information.

   Agda.Benchmarking

This stores the benchmarkint-related information in an IORef and 
implements MonadBench accordingly.
It provides recording of benchmarking data in pure code using 
unsafePerformIO.

   Agda.TypeChecking.Monad.Benchmark

This implements benchmarking in the TCM, in particular, to communicate 
with the IORef.

I think I now remember what stopped me from doing it for debugging as 
well.  The debug printing in interaction mode goes into the emacs buffer:

   displayDebugMessage n s = liftTCM $
     appInteractionOutputCallback (Resp_RunningInfo n s)

See Agda.Interaction.Response

   type InteractionOutputCallback = Response -> TCM ()

The emacs mode does

     setInteractionOutputCallback $
         liftIO . mapM_ print <=< lispifyResponse

It feels like somehow this could be refactored to happen in the IO 
instead of the TCM, using tricks with IORefs and unsafePerformIO.

It would be great if you got this to work, having debug info in 
functional or ReduceM code would be a major improvement for the 
development process.

Best,
Andreas

On 12.07.2017 18:11, Jesper Cockx wrote:
> 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
> 
> 
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
> 

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/