[Agda] Refectoring Builtins

[Ulf Norell]

On Tue, Sep 14, 2010 at 12:51 PM, Simon Foster <s.foster at dcs.shef.ac.uk>wrote:

> On 13 Sep 2010, at 20:20, Ulf Norell wrote:
>
>  I'll also need an additional field to store external tool functions
>> (something like [[String] -> Term -> TCM Term]).
>>
>> Is this be for function that should be run during type checking? Can't you
>> just use primitives for those?
>>
>
> No the function isn't (as yet) run at type checking - it's run like Agsy
> during program editing. Nevertheless I could use the primitive system for
> storing these functions anyway, at least that would make the conversion to
> Haskell cleaner, provided suitable instances of FromTerm/ToTerm are
> available.


If they're only used interactively (like Agsy) you shouldn't need to store
them in the state at all. Interactive commands are just Haskell functions
after all, so any functions you need can just go in the same Haskell module
as the command.


> Ideally I'd like to be able to automatically generate Haskell data-types
> and class instances from builtin types/constructors to provide a skeleton
> for a tool integration. Might the existing code in the compiler help here?
>

This sounds more like a separate tool to help developers of external tool
connections. Is it really something that needs to be automated? Or am I
misunderstanding something?


> Incidentally, what is exact difference between builtin primitives and
> postulates?
>

Primitives evaluate during type checking.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100914/7596a7a7/attachment.html