Stream: Coq users

Topic: How to overload coq notation


view this post on Zulip walker (Apr 16 2022 at 21:05):

I am trying to implement a slice operator for some vector impelementation and there is this problem:

I have vector.v with like that:

Notation "v [ st ... en ]" := (vec_slice v en st) (at level 90, left associativity): vector_scope.

There are few problems here, First I would love to use two dots instead of three v [st .. en] but coq has the two dots reserved for recursive notations and I couldn't embed it so I am not sure if this is a restriction or not.

Then I cannot use this notation at all ever time I try [foo ... bar] coq says That the ... should have been a ; so I guess it is mistaking it for the lists notation.

1 more thing the level things is completely random I wonder if there is a structured pattern to figure out what level does things fit into.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:13):

v [ st ... en ] overlaps with the syntax for applying v to a list — you can only tell them apart when you get to .., but Coq's LL(1) parser can only look _1_ token ahead. Sometimes you can use the trick in https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules, but it's not trivial.

view this post on Zulip walker (Apr 16 2022 at 21:23):

so you suggest picking up a different syntax for simplicity ?

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:23):

It's typically simpler to pick unambiguous symbols. Unicode characters can help with that. Combinations of existing characters can also work...

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:24):

but if you create new "keywords", you modify lexing, which can also break existing code.

view this post on Zulip walker (Apr 16 2022 at 21:25):

alright maybe I will use v [[st ..end ]] then. But do you have any tips for picking good level ?

view this post on Zulip walker (Apr 16 2022 at 21:27):

Well what I can say .. the new syntax broke something stupid I was doing

  destruct i as [ |[|[|[|[|[|[|[|x]]]]]]]]; simpl; try lia.

I cannot imagine why But I will just add spaces to make things work for now.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:28):

this syntax makes [[ into a new token (or keyword), so it prevents parsing [[ as two [.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:28):

You can also write it this way, BTW, but this makes .. a keyword as well:

Notation "v '[[' st '..' en ']]'" :=
  (id v en st) (at level 90, left associativity): vector_scope.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:29):

this might work, and you can omit the spaces when using it:

Notation "v [ [ st . . en ] ]" :=
  (id v en st) (at level 90, left associativity): vector_scope.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:30):

re levels, I don't have better advice than looking at levels of similar notation — and figuring out what the priority should be compared to other operators that you could find next to it.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:31):

For instance ++ and !! make sense on vectors; you can test if the combination works as expected, or if you need unexpected parentheses.

view this post on Zulip walker (Apr 16 2022 at 21:34):

Is there a way to debug why parsing fail ?

view this post on Zulip walker (Apr 16 2022 at 21:34):

so I did something like that ?

Notation "v '[[' st '..' en ']]'" := (vec_slice v en st) (at level 90, left associativity): vector_scope.

view this post on Zulip walker (Apr 16 2022 at 21:35):

Then I tried

Program Definition x := [#1; 2; 3] [[ 1 .. 2 ]] .

and I got some parsing error : Syntax error: '..' expected after [term level 0] (in [term]).

view this post on Zulip walker (Apr 16 2022 at 21:35):

when I manually replace the notation with the vec_slice thing, it works correctly.

view this post on Zulip walker (Apr 16 2022 at 21:36):

I was concerned that it could be a .. confusion so I replaced it with ... but coq gave the same error

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:38):

sounds like st is being bound to 1 .. 2

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:38):

at least, that's one of the possible reasons

view this post on Zulip walker (Apr 16 2022 at 21:39):

mmm but then coq does not allow typed notations I guess which would make things complex.

view this post on Zulip walker (Apr 16 2022 at 21:40):

I guess there is no escape from reading about Camlp5 then.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:43):

oh, this is a different problem, because this seems to parse:

Notation "v '[[' st 'XX' en ']]'" := (id v en st) (at level 90, left associativity): vector_scope.
Program Definition x := ([#1; 2; 3]) [[ 1 XX 2 ]].

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:43):

what does it mean, it does not allow "typed notations"?

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:45):

But yes, the parsing happens before name resolution and typechecking.

view this post on Zulip walker (Apr 16 2022 at 21:45):

what does it mean, it does not allow "typed notations"?
I was going to expalain but i realized it is stupid because yes coq knows st has type of nat | the sigma part.

view this post on Zulip walker (Apr 16 2022 at 21:45):

I will have to sit on the issue and keep debugging for a while and I hope I learn something from there... thanks a lot for the tips though!

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:46):

it doesn't know about those types while parsing.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:48):

to be sure, st wasn't being bound to 1 .. 2, but if you picked the wrong level for st that can happen. Print Grammar constr will show the parsing tables that are generated. And be sure to check out Coq's manual on notations — good luck!

view this post on Zulip Ali Caglayan (Apr 16 2022 at 22:06):

Print Notation is also now around on master (not 8.15)

view this post on Zulip Ali Caglayan (Apr 16 2022 at 22:07):

https://coq.github.io/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Print-Notation

view this post on Zulip walker (Apr 16 2022 at 22:16):

Well I will have to wait for a while then xD

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 22:18):

building coq master can be easier (and more valuable?) than using notations. You can even install it in parallel, in a separate opam switch...

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 22:19):

Until, Print Grammar constr at least has the right info (together with lots more).

view this post on Zulip walker (Apr 16 2022 at 22:20):

I will try to get it to work but to be honest, I always had bad experience with installing anything but official ocaml/ haskell from official distro repos.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 22:22):

mixing them is indeed a bad idea. I prefer to uninstall distro packages for languages I develop in.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 22:23):

otherwise you'll need to upgrade Coq version _when your distribution decides_. Which might work for your code, but not for your dependencies.


Last updated: Jan 28 2023 at 07:30 UTC