Commit bfbc24d8 authored by Robbert Krebbers's avatar Robbert Krebbers

Put Lit notations in global scope.

parent cee0b0d8
...@@ -2,6 +2,8 @@ Require Export heap_lang.derived. ...@@ -2,6 +2,8 @@ Require Export heap_lang.derived.
Delimit Scope lang_scope with L. Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val. Bind Scope lang_scope with expr val.
(* What about Arguments for hoare triples?. *)
Arguments wp {_ _} _ _%L _. Arguments wp {_ _} _ _%L _.
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
...@@ -16,10 +18,11 @@ Coercion of_val : val >-> expr. ...@@ -16,10 +18,11 @@ Coercion of_val : val >-> expr.
first. *) first. *)
(* We have overlapping notation for values and expressions, with the expressions (* We have overlapping notation for values and expressions, with the expressions
coming first. This way, parsing as a value will be preferred. If an expression coming first. This way, parsing as a value will be preferred. If an expression
was needed, the coercion of_val will be called. *) was needed, the coercion of_val will be called. The notations for literals
(* What about Arguments for hoare triples?. *) are not put in any scope so as to avoid lots of annoying %L scopes while
Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope. pretty printing. *)
Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope. Notation "' l" := (Lit l%Z) (at level 8, format "' l").
Notation "' l" := (LitV l%Z) (at level 8, format "' l").
Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope. Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
Notation "'ref' e" := (Alloc e%L) Notation "'ref' e" := (Alloc e%L)
(at level 30, right associativity) : lang_scope. (at level 30, right associativity) : lang_scope.
......
...@@ -62,13 +62,12 @@ Module LiftingTests. ...@@ -62,13 +62,12 @@ Module LiftingTests.
λ: "x", if "x" '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0. λ: "x", if "x" '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
Lemma FindPred_spec n1 n2 E Q : Lemma FindPred_spec n1 n2 E Q :
( (n1 < n2) Q (LitV (n2 - 1))) wp E (FindPred 'n2 'n1)%L Q. ( (n1 < n2) Q '(n2 - 1)) wp E (FindPred 'n2 'n1)%L Q.
Proof. Proof.
(* FIXME there are some annoying scopes shown here: %Z, %L. *)
revert n1; apply löb_all_1=>n1. revert n1; apply löb_all_1=>n1.
rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?. rewrite (comm uPred_and ( _)%I) assoc; apply const_elim_r=>?.
(* first need to do the rec to get a later *) (* first need to do the rec to get a later *)
rewrite -(wp_bindi (AppLCtx _)). rewrite -(wp_bindi (AppLCtx _)) /=.
rewrite -wp_rec' // =>-/=; rewrite -wp_value' //=. rewrite -wp_rec' // =>-/=; rewrite -wp_value' //=.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *) (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
rewrite ->(later_intro (Q _)). rewrite ->(later_intro (Q _)).
...@@ -106,8 +105,7 @@ Module LiftingTests. ...@@ -106,8 +105,7 @@ Module LiftingTests.
Qed. Qed.
Goal E, Goal E,
True wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x") True wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
(λ v, v = ('40)%L).
Proof. Proof.
intros E. intros E.
rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=. rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
......
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