From dcd59f1363835373a69689698eb2f3dec9437e49 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 23:00:11 +0100
Subject: [PATCH] Pattern matching notation for monadic binds.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This gets rid of the old hack to have specific notations for pairs
up to a fixed arity, and moreover allows to do fancy things like:

```
Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.
```
---
 theories/base.v      | 25 +++++++------------------
 theories/gmultiset.v |  2 +-
 theories/numbers.v   |  9 +++++----
 3 files changed, 13 insertions(+), 23 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index b74ca055..1295da6a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -887,25 +887,14 @@ Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
 Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
 
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
-  (at level 100, only parsing, right associativity) : stdpp_scope.
+  (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.
 
 Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
 
-Notation "' ( x1 , x2 ) ← y ; z" :=
-  (y ≫= (λ x : _, let ' (x1, x2) := x in z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
-  (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
-  (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
-  (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "' ( x1 , x2 , x3  , x4 , x5 , x6 ) ← y ; z" :=
-  (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
-  (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.
 
@@ -918,9 +907,9 @@ Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
 Arguments mguard _ _ _ !_ _ _ / : assert.
 Notation "'guard' P ; z" := (mguard P (λ _, z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
+  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
 Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
-  (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
+  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
 
 (** * Operations on maps *)
 (** In this section we define operational type classes for the operations
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 8d84b49e..a3ed60e8 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -27,7 +27,7 @@ Section definitions.
     multiplicity x X ≤ multiplicity x Y.
 
   Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
-    let (X) := X in '(x,n) ← map_to_list X; replicate (S n) x.
+    let (X) := X in ''(x,n) ← map_to_list X; replicate (S n) x.
   Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
 
   Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
diff --git a/theories/numbers.v b/theories/numbers.v
index 80975a32..dff4886c 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -534,11 +534,12 @@ Definition Qp_minus (x y : Qp) : option Qp :=
   match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
 Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
 Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
-Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / ('y)%Z) _.  
+
+Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
 Next Obligation.
-  intros x y. assert (0 < ('y)%Z)%Qc.
-  { apply (Z2Qc_inj_lt 0%Z (' y)), Pos2Z.is_pos. }
-  by rewrite (Qcmult_lt_mono_pos_r _ _ ('y)%Z), Qcmult_0_l,
+  intros x y. assert (0 < Zpos y)%Qc.
+  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
+  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
     <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
 Qed.
 
-- 
GitLab