Library iris.chan_lang.notation
From iris.chan_lang Require Export derived.
Export chan_lang.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion Var : string >-> expr.
Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder.
Notation "≠" := BAnon : binder_scope.
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : cexpr_scope.
Export chan_lang.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion Var : string >-> expr.
Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder.
Notation "≠" := BAnon : binder_scope.
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : cexpr_scope.
Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first.
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : cexpr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%bind e1 x2%bind e2)
(e0, x1, e1, x2, e2 at level 200) : cexpr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : cexpr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Recv e%C) (at level 9, right associativity) : cexpr_scope.
Notation "'newch'" := (Alloc%C)
(at level 30, right associativity) : cexpr_scope.
Notation "'ch_case:' e0 'with' 'left' => e1 | 'right' => e2 'end'" :=
(RCase e0 e1 e2)
(e0, e1, e2 at level 200, only parsing) : cexpr_scope.
Notation "'ch_case:' e0 'with' 'right' => e1 | 'left' => e2 'end'" :=
(RCase e0 e2 e1)
(e0, e1, e2 at level 200, only parsing) : cexpr_scope.
Notation "- e" := (UnOp MinusUnOp e%C)
(at level 35, right associativity) : cexpr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%C e2%C)
(at level 50, left associativity) : cexpr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%C e2%C)
(at level 50, left associativity) : cexpr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "e1 < e2" := (BinOp LtOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "~ e" := (UnOp NegOp e%C) (at level 75, right associativity) : cexpr_scope.
Notation "e1 <- e2" := (Send e1%C e2%C) (at level 80) : cexpr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%C)
(at level 102, f at level 1, x at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%C)
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%C e2%C e3%C)
(at level 200, e1, e2, e3 at level 200) : cexpr_scope.
Notation "'letp:' x y := e1 'in' e2" := (Letp x%bind y%bind e1%C e2%C)
(at level 102, x at level 1, y at level 1, e1, e2 at level 200) : cexpr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%bind e1 x2%bind e2)
(e0, x1, e1, x2, e2 at level 200) : cexpr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : cexpr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Recv e%C) (at level 9, right associativity) : cexpr_scope.
Notation "'newch'" := (Alloc%C)
(at level 30, right associativity) : cexpr_scope.
Notation "'ch_case:' e0 'with' 'left' => e1 | 'right' => e2 'end'" :=
(RCase e0 e1 e2)
(e0, e1, e2 at level 200, only parsing) : cexpr_scope.
Notation "'ch_case:' e0 'with' 'right' => e1 | 'left' => e2 'end'" :=
(RCase e0 e2 e1)
(e0, e1, e2 at level 200, only parsing) : cexpr_scope.
Notation "- e" := (UnOp MinusUnOp e%C)
(at level 35, right associativity) : cexpr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%C e2%C)
(at level 50, left associativity) : cexpr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%C e2%C)
(at level 50, left associativity) : cexpr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "e1 < e2" := (BinOp LtOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%C e2%C) (at level 70) : cexpr_scope.
Notation "~ e" := (UnOp NegOp e%C) (at level 75, right associativity) : cexpr_scope.
Notation "e1 <- e2" := (Send e1%C e2%C) (at level 80) : cexpr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%C)
(at level 102, f at level 1, x at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%C)
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%C e2%C e3%C)
(at level 200, e1, e2, e3 at level 200) : cexpr_scope.
Notation "'letp:' x y := e1 'in' e2" := (Letp x%bind y%bind e1%C e2%C)
(at level 102, x at level 1, y at level 1, e1, e2 at level 200) : cexpr_scope.
Derived notions, in order of declaration. The notations for let and seq
are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly.
Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%C))
(at level 102, f, x, y at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%C))
(at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x , e" := (Lam x%bind e%C)
(at level 102, x at level 1, e at level 200) : cexpr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, x, y, z at level 1, e at level 200) : cexpr_scope.
Notation "λ: x , e" := (LamV x%bind e%C)
(at level 102, x at level 1, e at level 200) : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%C) .. ))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%C e1%C)
(at level 102, x at level 1, e1, e2 at level 200) : cexpr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%C e1%C)
(at level 100, e2 at level 200, format "e1 ;; e2") : cexpr_scope.
Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%C e1%C)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%C e1%C)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
(at level 102, f, x, y at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%C))
(at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : cexpr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x , e" := (Lam x%bind e%C)
(at level 102, x at level 1, e at level 200) : cexpr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%C) ..))
(at level 102, x, y, z at level 1, e at level 200) : cexpr_scope.
Notation "λ: x , e" := (LamV x%bind e%C)
(at level 102, x at level 1, e at level 200) : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%C) .. ))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%C e1%C)
(at level 102, x at level 1, e1, e2 at level 200) : cexpr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%C e1%C)
(at level 100, e2 at level 200, format "e1 ;; e2") : cexpr_scope.
Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%C e1%C)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%C e1%C)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.