<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">(Just replying to the bits of Joe's message that I can.)<br><br></div><div class="gmail_quote">On Fri, Aug 2, 2013 at 12:18 AM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Incidentally, how does your format encode lists (substituions or the<br>
list of types that are an argument to type operators)?<br></blockquote><div><br></div><div>Their Subst and Inst commands take a variable-length list of arguments (refs to terms or types).<br>So the substitution is given as part of the command itself, using a "meta-level" list.<br>


</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> How does the HOL Light<br><div>
> exporter deal with sharing (between terms)?<br>
<br>
</div>It adds every type, term and theorem to a dictionary, so each is only<br>
exported once (per theory, when the dictionaries are reset).<br>
<div><br>
> I assume for the HOL4 exporter<br>
> this is not an issue, since sharing can be observed directly. Is this<br>
> correct?<br>
<br>
</div>That's a question for Ramana, who's the maintainer of the HOL4<br>
import/export infrastructure.<br></blockquote><div><br></div><div>The HOL4 exporter doesn't do anything more sophisticated than what the HOL Light exporter does, as far as sharing is concerned.<br>In particular, I do not make use of pointer equality directly.<br>


I use HOL4's native Term.compare etc. functions, though, which may use pointer equality internally.<br></div><div>I use a dictionary to save OpenTheory objects that I've already logged, and reuse them (with the ref command) when possible.<br>


</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
> - If I want to play with the tools, i.e., export some small theorem from HOL<br>
> Light, apply some mapping (aka theory interpretation) and re-import into<br>
> HOL4... Are there any step by step instructions that I can follow?<br>
<br>
</div>This FAQ describes the steps for exporting from HOL Light:<br>
<br>
<a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light" target="_blank">http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light</a><br>
<br>
Ramana: I know I just asked you in another thread for some notes on<br>
exporting from HOL4, but if you also made notes for importing I'd<br>
create two new FAQs to put them in!<br></blockquote><div><br></div>The importer is documented in the HOL4 sources, namely in this file:<br><br></div><div class="gmail_quote">  src/opentheory/Opentheory.sig<br><br></div><div class="gmail_quote">


The main entry-point is Opentheory.read_article : string -> reader -> thm net, which takes the path of an article file and a reader record (with information about where to find constants and axioms the article might need, and how to handle things the article might define, all documented in the file above) and returns a net of theorems. (A "net" makes for efficient lookup of theorems based on their conclusion; you can easily just extract a list of the theorems if desired.)<br>

<br></div><div class="gmail_quote">Let me know if the documentation doesn't make sense, or if you want more information for the FAQ. (I'll reply about the exporter in the other thread, perhaps a bit later - it may be more complicated.)<br>


</div><div class="gmail_quote"><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div></div>