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

[Martin Stone Davis]

Thanks. I'll try that and I'll also try to come up with a simpler example
of the problem.

--
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 1:37 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/2c09c304/attachment-0001.html