[opentheory-users] quoted strings

[Ramana Kumar]

On Mon, Jan 10, 2011 at 8:49 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> 1. What is the crazy regular expression in the article format
>> description for? Why isn't it just
>>  ["].*["]
>> ? (By that I mean any string of characters enclosed by quotation marks)
>
> Because slashes must be followed by a small set [\."] of escaped
> characters. For example, the name \c is illegal.
>
>> 2. (This is a fiddly implementation question you might choose to
>> ignore) I'd like to stick to the representation of names you
>> suggested, which is, I think, that you represent a name by the string
>> that if you would type it between quotes on an ML prompt would
>> evaluate to the name. (That is, names are strings, and they are
>> represented by similar but possibly different strings.) I think that
>> means that I should not use String.fromString on the lines I get from
>> the article, but I should convert (with String.toString) any names the
>> user passes to the read_article function to my internal representation
>> format. Sound right?
>
> I don't use these two functions myself, so I can't offer advice on how
> to use them. But what I would expect is that you would have functions:

I just want to say for the benefit of anyone else reading this that if
my previous email was correct, then there is a simpler approach of
using names to represent names (rather than a weird name_rep as in the
article), and just doing a fromString once when you read the article
line.

Hmm... could I ask one more question actually, to be sure?
You gave the example of the two names A\.b and and A.b.
Suppose I have an article that defines two different constants with these names.
Somewhere in the article file there must be lines that instruct the
virtual machine to push those names onto the stack.
What exactly would those lines look like?

>
> importName : openTheoryName -> holName
>
> exportName : holName -> openTheoryName
>
> that you would always use for converting between HOL4 names and
> OpenTheory names. Then the HOL4 user never needs to know that your
> internal representation of OpenTheory names (i.e., the type
> openTheoryName) is an ugly string filled with slashes, because
> Data.Bool./\\ is always converted to bool$/\ (or whatever it is).

Well you're right, users won't even have to provide hol names because
I intend to just have a big map that gets updated every time a theory
defines new constants in HOL4 (so whoever wrote the script file for
the theory would at some point say "add this open theory name mapping
for my new constant to the database" but that's all...)
HOL4 constant names aren't even strings :P (they are pairs of strings).

>
> In practice, I think escaping is extremely rare: I can only think of
> Boolean conjunction and disjunction that use it, and they will
> certainly be included in any mapping between HOL4 and OpenTheory
> constant names.
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>