[Agda] Expose more of Agda to reflection?

[Martin Stone Davis]

By "expose aggsy", I guess I mean that there would be a new function, agsy
: Term → TC ⊤. Or maybe Term → TC Term. I'd rather not pursue this,
however, as I think a much stronger case could be made for exposing
"rewrite" than for agsy.

I've taken a look at checkRHS, as Jesper suggested and I see now that
there's a more fundamental problem than exposing "rewrite": there is no way
to define a function without explicitly-stated patterns. E.g., in the Agda
language, one can define:

  foo : ∀ {X : Set} → {a b : X} → (a≡b : a ≡ b) → Set
  foo refl = {!!}

and Agda fills-in the implicit patterns as

  foo {X} {a} {.a} refl = {!!}

Using reflection's defineFun, one must specify all of the implicit
patterns, as in the second form. I believe that checkRHS uses the ability
of the typechecker to fill-in these implicit patterns. I suppose this could
also be done via reflection, simply by trying every combination of dot and
(var "_") patterns. Without recreating typechecking in Agda, is there a
more straightforward way to do this?

--
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 Tue, Feb 2, 2016 at 7:31 AM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> I am not sure what you mean by “expose agsy”? Wouldn’t it make more sense
> to rewrite agsy in Agda?
>
> Cheers,
> Thorsten
>
> From: Martin Stone Davis <martin.stone.davis at gmail.com>
> Date: Sunday, 31 January 2016 19:53
> To: agda <agda at lists.chalmers.se>
> Subject: [Agda] Expose more of Agda to reflection?
>
> Via reflection, it currently isn't straightforward to construct an agda
> function that invokes a rewrite. Exposing Agda's rewriting machinery to
> reflection would make this much easier. (Another neat idea is to expose
> agsy!) On the other hand, the exact same algorithms could be reproduced in
> the Agda language and it might be advisable to keep the reflection
> interface clean, especially considering that work done by "rewrite" or agsy
> might change in the future.
>
> Am I correct that Agda.TypeChecking.Rewriting can now be exactly
> reproduced in Agda? I'm studying the algorithm and would love to know that
> the path ahead of me is clear.
> --
> 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
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160202/b92ed75c/attachment-0001.html