[Agda] inferType yields a metavariable

[Martin Stone Davis]

Thanks. Works well so far. At the least, this seems to have solved the
trouble I had with nested 'reright's. I have more testing to do.

--
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 6:20 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/034febed/attachment-0001.html