[opentheory-users] interpreting namespaces

[Joe Hurd]

Hi Ramana,

The "show" lines just control printing, to make fully qualified names
more palatable for humans, so I wouldn't use these. In production
theories the "interpret" lines are intended for instantiating
parametric theories, not "fixing" articles that were extracted with
non-standard names.

So that leaves the extraction process as the right place to assign
names. One option would be to modify the HOL4 extractor, as you said.
What I did in HOL Light is to extract an article with HOL Light names
(everything is inside the HOLLight namespace), and then created a
temporary theory file with lots of "interpret" lines which I ran
through the opentheory tool to generate the final article. This
article can then be used with neat theory file with no additional
"interpret" lines. However, this process is perhaps a bit of a hack,
and a proper theorem prover interface would handle the local to
OpenTheory name mapping more smoothly.

A bit of a ramble, but I hope that helps you with your design decision.

Cheers,

Joe

On Tue, Dec 6, 2011 at 9:55 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Perhaps the "show" lines already do this?
> Specifically the
>
> show "NAMESPACE" as "NAMESPACE"
>
> form.
>
> Is that appropriate to use in this situation, when packaging an
> article that is systematically using the wrong namespace?
>
> On Tue, Dec 6, 2011 at 5:46 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> The interpret lines in a theory file enable "renaming" of specific
>> constants and type operators.
>> Would it be possible to rename an entire namespace in one go?
>>
>> An example usage is extracting the lazy list theory from HOL4, which
>> is called llist, but in OpenTheory namespace might be better called
>> LazyList or Data.LazyList or something.
>> The automatic technology for extracting an article just uses the
>> theory name as the namespace by default.
>> I could extend the HOL4 extractor to allow a manual override.
>> Alternatively, I could put something in the .thy file (at the moment
>> it would be an "interpret" line for every constant/type operator
>> defined).
>> Which option is better?
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list