Commit 64a3d258 authored by Robbert Krebbers's avatar Robbert Krebbers

Play with printing boxes to improve pretty printing.

parent 2dcc2a40
...@@ -36,15 +36,11 @@ Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)). ...@@ -36,15 +36,11 @@ Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%bind e1 x2%bind e2) (Match e0 x1%bind e1 x2%bind e2)
(e0, x1, e1, x2, e2 at level 200, (e0, x1, e1, x2, e2 at level 200,
format "'[' 'match:' e0 'with' '/' '[hv' 'InjL' x1 => '[' e1 ']' '/' | 'InjR' x2 => '[' e2 ']' '/' 'end' ']' ']'") : expr_scope. format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1) (Match e0 x2%bind e2 x1%bind e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "'case:' e0 'of' 'InjL' => e1 | 'InjR' => e2 'end'" :=
(Case e0 e1 e2)
(e0, e1, e2 at level 200) : expr_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E) Notation "'ref' e" := (Alloc e%E)
(at level 30, right associativity) : expr_scope. (at level 30, right associativity) : expr_scope.
...@@ -60,19 +56,33 @@ Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope. ...@@ -60,19 +56,33 @@ Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope.
(* The unicode is already part of the notation "_ ← _; _" for bind. *) (* The unicode is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E) Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : expr_scope. (at level 102, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E)) Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope. (at level 102, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
(at level 102, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope.
Notation "λ: x , e" := (Lam x%bind e%E) Notation "λ: x , e" := (Lam x%bind e%E)
(at level 102, x at level 1, e at level 200) : expr_scope. (at level 102, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..)) Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, x, y, z at level 1, e at level 200) : expr_scope. (at level 102, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (locked (LamV x%bind e%E)) Notation "λ: x , e" := (locked (LamV x%bind e%E))
(at level 102, x at level 1, e at level 200) : val_scope. (at level 102, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))) Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
(at level 102, x, y, z at level 1, e at level 200) : val_scope. (at level 102, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope. (at level 200, e1, e2, e3 at level 200) : expr_scope.
...@@ -86,7 +96,8 @@ Notation "'Λ:' e" := (TLamV e%E) ...@@ -86,7 +96,8 @@ Notation "'Λ:' e" := (TLamV e%E)
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E) Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200, (at level 102, x at level 1, e1, e2 at level 200,
format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : expr_scope. format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope. (at level 100, e2 at level 200,
format "'[' '[' e1 ']' ;; '/' e2 ']'") : expr_scope.
...@@ -22,9 +22,9 @@ Definition CG_locked_push : val := λ: "st" "l" "x", ...@@ -22,9 +22,9 @@ Definition CG_locked_push : val := λ: "st" "l" "x",
| cons y ys => s <- ys ;; InjR y | cons y ys => s <- ys ;; InjR y
end *) end *)
Definition CG_pop : val := λ: "st" <>, Definition CG_pop : val := λ: "st" <>,
case: Unfold !"st" of match: Unfold !"st" with
InjL => λ: <>, InjL #() InjL <> => InjL #()
| InjR => λ: "y", "st" <- (Snd "y");; InjR (Fst "y") | InjR "y" => "st" <- (Snd "y");; InjR (Fst "y")
end. end.
...@@ -40,9 +40,9 @@ Definition CG_snap : val := λ: "st" "l" <>, ...@@ -40,9 +40,9 @@ Definition CG_snap : val := λ: "st" "l" <>,
| cons x xs => (f x) ;; iter f xs | cons x xs => (f x) ;; iter f xs
end *) end *)
Definition CG_iter : val := rec: "iter" "f" := λ: "s", Definition CG_iter : val := rec: "iter" "f" := λ: "s",
case: (Unfold "s") of match: (Unfold "s") with
InjL => λ: <>, #() InjL <> => #()
| InjR => λ: "x", "f" (Fst "x");; "iter" "f" (Snd "x") | InjR "x" => "f" (Fst "x");; "iter" "f" (Snd "x")
end. end.
(* snap_iter st l := λ f. iter f (snap st l #()) *) (* snap_iter st l := λ f. iter f (snap st l #()) *)
......
...@@ -27,12 +27,12 @@ Definition FG_push : val := rec: "push" "st" := λ: "x", ...@@ -27,12 +27,12 @@ Definition FG_push : val := rec: "push" "st" := λ: "x",
Definition FG_pop : val := rec: "pop" "st" := λ: <>, Definition FG_pop : val := rec: "pop" "st" := λ: <>,
let: "stv" := !"st" in let: "stv" := !"st" in
let: "x" := !(Unfold "stv") in let: "x" := !(Unfold "stv") in
case: "x" of match: "x" with
InjL => λ: <>, InjL #() InjL <> => InjL #()
| InjR => λ: "x", let: "y" := Fst "x" in let: "ys" := Snd "x" in | InjR "x" => let: "y" := Fst "x" in let: "ys" := Snd "x" in
if: (CAS "st" "stv" "ys") if: (CAS "st" "stv" "ys")
then (InjR "y") then (InjR "y")
else "pop" "st" #() else "pop" "st" #()
end. end.
(* iter f = λ st. (* iter f = λ st.
...@@ -40,9 +40,9 @@ Definition FG_pop : val := rec: "pop" "st" := λ: <>, ...@@ -40,9 +40,9 @@ Definition FG_pop : val := rec: "pop" "st" := λ: <>,
| nil => #() | nil => #()
| cons y ys => f y ;; iter f ys *) | cons y ys => f y ;; iter f ys *)
Definition FG_iter : val := rec: "iter" "f" := λ: "st", Definition FG_iter : val := rec: "iter" "f" := λ: "st",
case: !(Unfold "st") of match: !(Unfold "st") with
InjL => λ: <>, #() InjL <> => #()
| InjR => λ: "x", | InjR "x" =>
let: "y" := Fst "x" in let: "y" := Fst "x" in
let: "ys" := Snd "x" in let: "ys" := Snd "x" in
"f" "y";; "iter" "f" "ys" "f" "y";; "iter" "f" "ys"
......
...@@ -35,13 +35,17 @@ End bin_log_def. ...@@ -35,13 +35,17 @@ End bin_log_def.
Notation "⟦ Γ ⟧*" := (interp_env Γ). Notation "⟦ Γ ⟧*" := (interp_env Γ).
Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" := Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
(bin_log_related E1 E2 Δ Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level, (bin_log_related E1 E2 Δ Γ e%E e'%E τ)
format "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ"). (at level 74, E1,E2, e, e', τ at next level,
format "'[hv' '{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'").
Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" := Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I (at level 74, E1,E2, e, e', τ at next level). ( Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I
(at level 74, E1,E2, e, e', τ at next level,
format "'[hv' '{' E1 ',' E2 ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'").
Notation "Γ ⊨ e '≤log≤' e' : τ" := Notation "Γ ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level, ( Δ, bin_log_related Δ Γ e%E e'%E τ)%I
format "Γ ⊨ e '≤log≤' e' : τ"). (at level 74, e, e', τ at next level,
format "'[hv' Γ ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'").
(** [interp_env] properties *) (** [interp_env] properties *)
Section interp_env_facts. Section interp_env_facts.
......
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