Commit a85a8e2f authored by Ralf Jung's avatar Ralf Jung

fix yet another case of broken heap_lang notation

parent 7badb484
1 subgoal
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
(* Test yet another way of importing heap_lang modules that used to break
printing *)
From iris.heap_lang Require Export lifting notation.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Section printing_tests.
Context `{heapG Σ}.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in
if: "val1" = "val2" then "val" else "val3" {{ _, True }}.
Proof.
iIntros "_". Show.
Abort.
End printing_tests.
......@@ -4,6 +4,9 @@ From stdpp Require Export strings.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Module heap_lang.
Open Scope Z_scope.
......@@ -529,3 +532,14 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
(** Define some derived forms. *)
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
Notation LamV x e := (RecV BAnon x e) (only parsing).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
......@@ -2,16 +2,8 @@ From iris.program_logic Require Import language.
From iris.heap_lang Require Export lang tactics.
Set Default Proof Using "Type".
(** Define some derived forms. Happens in the same file because the order of
this and the following notations being defined is very relevant. *)
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
......
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