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.
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.
so you suggest picking up a different syntax for simplicity ?
It's typically simpler to pick unambiguous symbols. Unicode characters can help with that. Combinations of existing characters can also work...
but if you create new "keywords", you modify lexing, which can also break existing code.
alright maybe I will use v [[st ..end ]]
then. But do you have any tips for picking good level ?
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.
this syntax makes [[
into a new token (or keyword), so it prevents parsing [[
as two [
.
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.
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.
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.
For instance ++
and !!
make sense on vectors; you can test if the combination works as expected, or if you need unexpected parentheses.
Is there a way to debug why parsing fail ?
so I did something like that ?
Notation "v '[[' st '..' en ']]'" := (vec_slice v en st) (at level 90, left associativity): vector_scope.
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]).
when I manually replace the notation with the vec_slice thing, it works correctly.
I was concerned that it could be a ..
confusion so I replaced it with ...
but coq gave the same error
sounds like st
is being bound to 1 .. 2
at least, that's one of the possible reasons
mmm but then coq does not allow typed notations I guess which would make things complex.
I guess there is no escape from reading about Camlp5 then.
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 ]].
what does it mean, it does not allow "typed notations"?
But yes, the parsing happens before name resolution and typechecking.
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.
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!
it doesn't know about those types while parsing.
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!
Print Notation
is also now around on master (not 8.15)
Well I will have to wait for a while then xD
building coq master can be easier (and more valuable?) than using notations. You can even install it in parallel, in a separate opam switch...
Until, Print Grammar constr
at least has the right info (together with lots more).
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.
mixing them is indeed a bad idea. I prefer to uninstall distro packages for languages I develop in.
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: Oct 13 2024 at 01:02 UTC