Stream: Coq users

Topic: newline in string

cdepillabout (Jan 05 2022 at 05:55):

I'm trying to play around with coq-parsec: https://github.com/liyishuai/coq-parsec

In particular, I'm trying to write code like the following:

Example parseLFExample : parse parseLF "\n" = inr ("010"%char, "").
Proof. unfold parse. simpl. reflexivity. Qed.

The call to reflexivity gives a message like the following:

Unable to unify "inr ("010"%char, "")" with
 "inl
    (Some
       (String "D"
          (String "i"
             (String "
...

My guess is that "\n" is not a legal way in Coq to write a string with a single newline character (possibly because coq doesn't know about newline escape sequences?). How would I write a string in Coq with a newline in it? For instance, in Haskell I could write something like "123\n456\n".

Relatedly, how would I write a multi-line string in Coq? For instance, in Haskell, You can't naively write:

myString :: String
myString = "hello
this
is
a
multiline
string"

(Although there are various ways of working around this limitation and getting something similar to this to work....)

How would you do something like this in Coq?

Julin Shaji (Jan 05 2022 at 06:15):

Not sure if this is exactly what you need, but for writing multiline strings, I tried

Compute "hi
hello"%string
(*
= "hi
hello"%string
     : string
*)

and the new line is showing coming up as part of the string.

cdepillabout (Jan 05 2022 at 07:44):

@Julin S Thanks! So I guess if I want to write a string with a newline, I can just literally write a string that spans over multiple lines.

Although I'm wondering why you are using %string here. Is there a difference between "hello" and "hello"%string in Coq?

Julin Shaji (Jan 05 2022 at 08:29):

It's to mention the scope for the notation. To use the notation (placing characters inside " ") to enter strings in user friendly way.

I think this is the relevant docs: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes

Strings are really represented using Ascii.ascii objects.

The notation allows us to write

"A"

instead of

String (Ascii true false false false false false true false)
         EmptyString

Paolo Giarrusso (Jan 05 2022 at 12:21):

But %string is usually not necessary

Paolo Giarrusso (Jan 05 2022 at 12:22):

(depending on your scope setup, of course)

cdepillabout (Jan 06 2022 at 01:47):

Ah okay, thanks. That makes sense.

Last updated: Oct 03 2023 at 02:34 UTC