Commit dcd59f13 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Pattern matching notation for monadic binds.

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.
```
parent 376dff25
......@@ -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
......
......@@ -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 .
......
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment