Stream: Coq users

Topic: ✔ Definition of string notation

Julin S (Jan 01 2022 at 17:38):

I was trying to understand the way strings are represented (string type) in coq.

Where is the notation that allows strings to made like

Check "hello%string.
Check "a"%string.

defined?

Is it a normal notation or is it something special?

Was wondering about this as the Notation command itself uses quotes.

I tried glancing through here and here, but couldn't spot the notation definition.

Couldn't figure out how to use the Locate command properly for that either.. :grimacing:

Tried just

Locate "".

But there is no way to escape the quotes, is there?

Lessness (Jan 01 2022 at 17:58):

Require Import String.

Check "hello"%string.
Check """"%string.

I believe that the second string is one quote symbol (escaped), but I will search for definite answer in documentation.

Julin S (Jan 01 2022 at 18:07):

That does seem to be a single quote (").

It comes down to

(Ascii.Ascii false true false false false true false false)

which is for ".

I guess there's some rule that I'm yet to find out.

Julin S (Jan 01 2022 at 18:10):

But doing

Locate " """" """" "%string.
(* Unknown notation *)

to find the definition of the string notation didn't work.

I thought maybe """" can be used instead of " here. I guess not.

Li-yao (Jan 01 2022 at 18:33):

I don't think you can look it up, it's not definable with the Notation system.

Karl Palmskog (Jan 01 2022 at 18:41):

from the last time I looked, I think string notations are a plugin, so defined at the OCaml level (where one can in principle come up with any crazy syntax)

Julin S (Jan 01 2022 at 18:57):

Oh.. okay..

I couldn't understand much of it, but is this that plugin?

Karl Palmskog (Jan 01 2022 at 18:58):

yes, that's one of the source files. The interface between OCaml and Coq is here.

Julin S (Jan 01 2022 at 18:59):

And how was " 'escaped' (not sure if that' the right word :sweat_smile: ) in """"%string?

Can we escape other characters as well using something similar? Like newline (\n).

Karl Palmskog (Jan 01 2022 at 19:14):

a plugin can directly hook into Coq's parser and lexer, so it can do that, sure

Julin S (Jan 01 2022 at 20:34):

Thanks, guys.

Notification Bot (Jan 01 2022 at 20:34):

Ju-sh has marked this topic as resolved.

Pierre Roux (Jan 02 2022 at 10:41):

It's no longer OCaml defined for quite some time, look for String Notation (both in the manual and in Init/Byte.v, String/Ascii.v and String/String.v)

Julin S (Jan 02 2022 at 12:41):

@Pierre Roux Is this same as the String Notation mentioned here? https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#string-notations

Julin S (Jan 02 2022 at 12:53):

And what could the stuff here be doing? Is it for implementing String Notation syntax itself or something?

Pierre Roux (Jan 02 2022 at 16:47):

yes and yes

Last updated: Apr 18 2024 at 12:01 UTC