[opentheory-users] parsing article information

[Ramana Kumar]

On Sun, Jan 9, 2011 at 7:03 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> Q1: Is this information available by a more appropriate means than
>> calling info --summary?
>
> opentheory info --summary is supposed to generate article summaries in
> a human readable form: as of now there is no machine-readable version
> of it other than the article file.

Will there be? I can probably get opentheory to spit one out by
catching it just before it prints the human-readable version and
sending whatever data structures it is using to a different printer.

>
>> Q2: The article file for bool-def-1.0, say, seems to talk about
>> constants with the prefix "Data.Bool.", but in info --summary this
>> prefix is stripped off. How should I find out that there may be a
>> prefix like this to deal with? (I saw some "show" thing in the output
>> from opentheory once - is that documented? what does it mean?)
>
> You are correct: the (as yet documented) show tags in a theory
> determines how the namespaces get transformed as names are printed. To
> see a pure version remove all show tags or just run opentheory info
> --summary directly on the article file.

If I generate the article file with opentheory, though, the namespace
information is there. How do I get a pure article file for say
bool-1.0?

>
>> Q2.1: How should I deal with the prefix? Should the article reader
>> strip it off names in the article file, so that the generated theorems
>> end up looking more like info --summary, or should I create theorems
>> with the prefix and add the prefix when parsing the summary?
>
> I would recommend creating a mapping from fully-qualified OpenTheory
> names to their HOL4 versions. The file
>
> opentheory/test/interpretations/hol-light.int
>
> is an example showing how HOL Light names map to the OpenTheory namespace.

I don't quite understand how this is all going to fit together... HOL4
already has a boolTheory with a proof script. Now the gilith repo has
one too, represented by the package (and ultimately the article),
which was presumably generated from a different (e.g. HOL-light)
script. If I try to match the constants up within HOL4, that means I
should be in a context where those constants are already defined, but
when I run the article it's going to try to redefine them. In other
words it seems like either I build the article's theory, or I build
the existing theory, and I don't need, and can't have, both, so what
sense is there in getting their names to match? (Well I can have both,
but they won't interact, in which case I wouldn't want the names to
match...)
This is perhaps worth discussing in a separate email thread... feel
free to change the subject line.

>
>> Q3: Are there any published rules or grammar for how info --summary
>> terms (and theorems) are printed?
>
> There's no documentation on this (other than the source code), but
> I'll reiterate that it's supposed to be a human-readable form of the
> summary, justifying tricks such as printing HOL numerals as decimal
> numerals.
>
>> Q4: info --summary doesn't give the arity of the required type
>> operators or the types of the required constants... I think these can
>> be figured out by actually reading the article, but by then it might
>> be too late for someone making a call to read_article who wants to
>> provide the requirements. can+should opentheory print this information
>> (maybe optionally)?
>
> This is an interesting point: right now the type of an input constant
> is not contained anywhere in the article (just types of uses of the
> constant). For now I'm going to hope that this information is known to
> the reader.
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>