<br>On Tue, Sep 14, 2010 at 12:51 PM, Simon Foster <span dir="ltr"><<a href="mailto:s.foster@dcs.shef.ac.uk">s.foster@dcs.shef.ac.uk</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 13 Sep 2010, at 20:20, Ulf Norell wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'll also need an additional field to store external tool functions (something like [[String] -> Term -> TCM Term]).<br>
<br>
Is this be for function that should be run during type checking? Can't you just use primitives for those?<br>
</blockquote>
<br></div>
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.</blockquote>
<div><br></div><div>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.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"> 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?<br>
</blockquote><div><br></div><div>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?</div><div> </div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Incidentally, what is exact difference between builtin primitives and postulates?<br></blockquote><div><br></div><div>
Primitives evaluate during type checking.</div><div><br></div><div>/ Ulf </div></div>