[opentheory-users] quoted strings

[Ramana Kumar]

I'm starting to understand what you mean...

Two questions:

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)

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?
On Mon, Jan 10, 2011 at 8:14 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> If you stick to the *representation* of names that I suggest, with the
> slashes left in, you will get the right properties of name equality.
> Any representation that gives you the same equality property is fine
> with me: indeed, OpenTheory uses a different one based on lists of
> strings.
>
> Removing slashes, so that
>
> A\.b
>
> and
>
> A.b
>
> have the same representation, will give you the wrong equality
> relation on names, so beware.
>
> Cheers,
>
> Joe
>
> On Mon, Jan 10, 2011 at 11:58 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> On Mon, Jan 10, 2011 at 7:37 PM, Joe Hurd <joe at gilith.com> wrote:
>>> Hi Ramana,
>>>
>>>> First of all, what does it mean to obtain a string by matching a
>>>> regular expression?
>>>
>>> Good question: I've tightened up the language to
>>>
>>> "A name command is a string that matches the following regular expression:"
>>>
>>>> And then you're left with the string, you discard the quotes, but what
>>>> about the slashes inside the string?
>>>
>>> You leave the slashes in the string. The most important property here
>>
>> Leave the slashes in the string?
>> But bool.art uses Data.Bool./\\, but I think the intention is for the
>> name to be Data.Bool./\, no?
>> I'm at the moment using String.fromString on the line I get back from
>> TextIO.inputLine - I can't keep track of where all these functions
>> (including whatever's printing things out to my terminal) add and
>> remove slashes. Would you expect to have to use fromString on a line
>> from an article, or should the line itself be right?
>> If the extra slash in bool.art is wrong, perhaps you got caught by an
>> SML printer that was trying to print something it could read back in
>> to a value.
>>
>>> is that equality of names is the same as equality of the strings
>>> representing them. For example, the two names
>>>
>>> A.b
>>>
>>> and
>>>
>>> A\.b
>>>
>>> are different, so it is good that they are represented by different
>>> strings (because the slashes are left in).
>>>
>>> This is all that automatic tools for processing articles need to know.
>>> However, for the purpose of displaying names in human-readable form,
>>> the names might undergo some further processing, so A.b is actually
>>> treated as the name b in the namespace A, and A\.b is treated as the
>>> name A\.b in the global namespace, and as a result "show" tags might
>>> transform them differently.
>>>
>>> In my eyes an import tool falls into the "automatic tools" category,
>>> so I don't think you need to worry about the human readability angle.
>>>
>>> Does that help?
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>