[Agda] Re: [reright] debugging unsolved metas in a nested tactic

[Ulf Norell]

The sledgehammer approach to seeing behind the scenes is -v tc:100.
Actually deciphering what's going on might be a different matter.

/ Ulf

On Wed, Feb 24, 2016 at 9:58 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> A thought on how I might make progress: I'm missing information that would
> be helpful to debugging this. I suspect that the metavariable, _N, sent to
> blockOnMeta in the inner call to reright needs to then be solved somehow by
> the computation in the outer call. However, I can't see what _N is or how
> it might be connected to other metavariables, and so I can't tell why it
> isn't getting solved. Is there some way to see these behind-the-scenes
> details?
>
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578 <3106993578>
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> On Wed, Feb 24, 2016 at 12:40 AM, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> Please help me figure out why I'm getting unsolved metas here
>> <https://github.com/m0davis/agda-prelude/blob/WIP/test/Reright.agda>,
>> from my fork of agda-prelude
>> <https://github.com/m0davis/agda-prelude/commit/c013e56ac9a8b7b7d986dc27d67e24f1a614d026>
>> .
>>
>> 'reright' is intended to work just like rewrite, except it's invokable
>> from the rhs. From my extensive testing, it seems to work as one would want
>> and expect: it provides rewritten context variables and rewrites the goal
>> in a manner equivalent to 'rewrite'. However, it has trouble sometimes when
>> a reright is nested within another reright: that's where I'm getting
>> unsolved metas. Afaics, the inner reright blocksOnMeta, then the outer
>> reright completes and the computation wrt the inner reright never gets
>> restarted. Beyond that, I'm not sure why or what to do about it.
>>
>> NB, I'm aware of how horribly-written the code is. I fully intend a major
>> refactor as soon as I work through the bugs!
>> --
>> Martin Stone Davis
>>
>> Postal/Residential:
>> 1223 Ferry St
>> Apt 5
>> Eugene, OR 97401
>> Talk / Text / Voicemail: (310) 699-3578 <3106993578>
>> Electronic Mail: martin.stone.davis at gmail.com
>> Website: martinstonedavis.com
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160224/fdefb3e7/attachment.html