[opentheory-users] quoted strings

[Joe Hurd]

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:

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

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