[opentheory-users] quoted strings

[Ramana Kumar]

I think actually it looks more like this.
My object datatype includes a constructor OName of string, but should really be

type name_rep = string
OName :  name_rep -> object

then when reading an article, I get a string surrounded by quotes.
by stripping the quotes I am left with a name_rep, since I am using
the same representation of names as articles do, right?
So I go ahead and push OName (trimquotes line) onto the stack.
Then I have to define a function to get a name back from an object

fun object_to_name (OName s) = name_rep_to_name s

and I think we have:

fun name_rep_to_name s = valOf(String.fromString)

which would possibly explain why you have a restrictive regular
expression for the articles: they need to be representations that
won't make fromString return NONE?
On Mon, Jan 10, 2011 at 8:36 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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
>>
>