[Agda] Refectoring Builtins

[Simon Foster]

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. 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?

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

Thanks,

-Si.