[Agda] inferType yields a metavariable

[Ulf Norell]

The infrastructure of that would be a little bit messy. Instead I added
commitTC
that commits any changes to the current state. If you call that after
forceFun things
work out. I also added blockOnMeta! to agda-prelude which calls commitTC
before
blocking.

A caveat is that commitTC can't be called after declareDef or defineFun.

Please try it out. I'll add some test cases and documentation later.

/ Ulf

On Fri, Feb 26, 2016 at 10:14 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> What if there were a continueAfterMeta : (xs : List Meta) → (tc : TC A) →
> TC A, which would run tc after any one of the xs were solved?
>
> --
> 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 Fri, Feb 26, 2016 at 12:03 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> Hmm, that's trickier. It's the forceFun that makes it possible to solve
>> the target type, but when you blockOnMeta you lose that work. Not sure
>> what's needed to make this work.
>>
>> / Ulf
>>
>> On Fri, Feb 26, 2016 at 8:40 AM, Martin Stone Davis <
>> martin.stone.davis at gmail.com> wrote:
>>
>>> Thanks, that worked. But how about this slightly-more-complicated
>>> example? If I remove "id", the goal gets reported as _n → Set, which is
>>> fine for me, since I just care about seeing that it's 'Set'. However, with
>>> "id", it's _n → _m. I'm not finding that blockOnMeta helps here.
>>>
>>>     open import Prelude
>>>     open import Tactic.Reflection
>>>
>>>     macro
>>>       infer-the-goal₂ : Tactic
>>>       infer-the-goal₂ hole = do
>>>         goal ← forceFun =<< inferType hole -|
>>>         typeError [ termErr goal ]
>>>
>>>     foo₂ : Set
>>>     foo₂ = id (infer-the-goal₂ {!!})
>>>
>>>
>>> --
>>> 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 Thu, Feb 25, 2016 at 9:41 PM, Ulf Norell <ulf.norell at gmail.com>
>>> wrote:
>>>
>>>> Try blockOnMeta if it comes back a meta.
>>>>
>>>> / Ulf
>>>> On Fri, 26 Feb 2016 at 06:38, Martin Stone Davis <
>>>> martin.stone.davis at gmail.com> wrote:
>>>>
>>>>> Is there some way to infer-the-goal as 'Set' in foo (below)? I mean to
>>>>> do this within the tactic, not by providing implicits to id. Currently,
>>>>> infer-the-goal reports the goal as _n (some metavariable).
>>>>>
>>>>>   open import Prelude
>>>>>   open import Builtin.Reflection
>>>>>
>>>>>   macro
>>>>>     infer-the-goal : Tactic
>>>>>     infer-the-goal hole = inferType hole >>= λ goal → typeError
>>>>> (termErr goal ∷ [])
>>>>>
>>>>>   foo : Set
>>>>>   foo = id infer-the-goal
>>>>>
>>>>> --
>>>>> 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/20160226/45590675/attachment.html