(poll) which monadic notation do you use?

Using Coq
1

Hi there
We are trying to evaluate the interest of adding non builtin notations into proofgeneral default indentation mechanism.
Is there some common monadic notation used by almost everyone in Coq?
I know of these two:

x <- e ;;
y <- e;;
e

and

do x <- e;
do x <- e;
e

Are these common enough to deserve being builtin in pg?

More generally are you annoyed by some other syntax not correctly indented in pg?

1 Like
2

Gregory Malechaā€™s ext-lib library, that is used quite commonly, uses the former. It also defines two other related convenient notations:

  • e;; f defined as (_ <- e;; f)
  • 'pat <- e;; f defined as bind e (fun x => match x with pat => f)

And indeed their current indentation is a recurrent pain.

2 Likes
3

I too use ext-lib, and find the lack of indentation support frustrating! I donā€™t care too much if itā€™s built in or not, but I think itā€™s important to have good support for this. Monad notations are the main pain that I have had with proof general (most other notations I have seen are used for single-line expressions and so indentation is less of a pain point there).

(I kicked off this discussion with the pull request, for transparency)

4

I use ext-lib monadic notations and would love to see then supported.

1 Like
5

stdpp uses

Notation "x ā† y ; z" := (y ā‰«= (Ī» x : _, z))
  (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.

Notation "' x1 .. xn ā† y ; z" := (y ā‰«= (Ī» x1, .. (Ī» xn, z) .. ))
  (at level 20, x1 binder, xn binder, y at level 100, z at level 200,
   only parsing, right associativity) : stdpp_scope.
Notation "x ;; z" := (x ā‰«= Ī» _, z)
  (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.

Of the top of my head, the following two indentation issues with tactic notation come to my bind:

  • ssreflect-style by (sometimes?) leads to an indentation on the next line. IIRC e.g. after something like foo; last by eauto.
  • We have some notation that involves a forall, and that screws up indentation badly: iInduction lemma as ... forall (a b c), meaning ā€œgeneralize a, b, c for the induction hypothesisā€, but then PG makes the next line indented all the way to the position of the forall, which is not at all what we want.
6

Iā€™m currently using ext-lib and indeed the indentation is a huge pain. Thanks so much for the fix! Iā€™m looking forward to it.

7

Judging by previous responses there might not be a common syntax. I can report that Mtac2 uses x <- t1; t2 for bind t1 (fun x => t2), t1;; t2 for _ <- t; t2 and also supports 'pat <- t1; t2 for irrefutable let bindings.

Mtac2 code gets mangled quite badly by the indentation algorithm in proof general. We have use a lot of keywords that also come up in coq proper (for example, mmatch ... as ... in ... return ... with ... end). Terms like those will be indented in various weird ways, probably owed to how exactly PG determines when to indent based on, I think, mostly just one isolated keyword?

I wonder if the long-term fix for this would be to query coq for the format of user-defined notation? I know this would only work for printing notation (i.e. not only parsing notation) but it would be a great help still.

Support for this would have to be added to Coq, obviously. And if we are already doing that, letā€™s keep in mind a coqfmt tool? I donā€™t mind my code looking ugly while I write it as long as there is a consistent way to format it automatically once I am done with my changes. Obviously, I am just dreaming hereā€¦

1 Like
8

I usually use either x <- e ;; e' (employed in MetaCoq notations for instance) or simply x <- e; e'. Indentation in PG has a few quirks but it somewhat work.

I have a lot of troubles combining PG and the syntax used by Equations:

Equations foo a b :=
  foo (A0 _) (B0 _ _) := branch0 ;
  foo _ _ := branch1 .

I often find myself fighting with PG to get a reasonable indentation and thatā€™s an important (and rather stupid) reason making me hesitate to use equations.

9

To be precise we have a very complex lexer that performs non trivial toekn detection (by looking around and guessing basically) and simple grammar using the smie library by Stefan Monnier. The lexer is very difficult to maintain. The grammar is simple to maintain but cannot really correspond to coqā€™s grammar because smie is based on a notion of grammar that is too simple. Anyway it is better than nothing I hope.

This idea has been in the air for a long time. It would be nice indeed. A independant stand-alone coqindent program would be perhaps be better.

10

The coq-prelude package yet to be published to Opam propose the following notation based on the recent custom entry mechanism:

Declare Custom Entry monad.

Notation "'do' p 'end'" := p (p custom monad at level 10) : prelude_scope

Notation "p ';' q" := (bind p%monad (fun _ => q%monad))
  (in custom monad at level 10, q at level 10, right associativity, only 
parsing).

Notation "'let*' a ':=' p 'in' q" := (bind p%monad (fun a => q%monad))
  (in custom monad at level 0, a ident, p constr, q at level 10, right associativity, only parsing).

Notation "'let' a ':=' p 'in' q" := (let a := p in q%monad)
  (in custom monad at level 5, a ident, p constr, q at level 10, right associativity, only parsing).

Notation "x" := x%monad (in custom monad at level 0, x constr at level 200, only parsing).

The idea is to be very analogous to OCaml monadic let.

Basically I am the only user of this notation yet, and I would be surprised to see PG support it explicitly, but eh, it exists! :smile:

2 Likes
11

I like the idea of using OCaml let* notation! Many people here using ExtLib. Perhaps to popularize them the first step is to add it to ExtLib as alternative notations.

12

I, too, like the OCaml syntax and I am planning propose it as an alternative or even the default syntax for Mtac2 soon. I just havenā€™t gotten around to writing the code yet. (I would prefer not having do .. end blocks, though.)

It might be easier to indent correctly, too.