[opentheory-users] parsing article information

[Joe Hurd]

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.

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

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

> 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