Commit 30d997f5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent d0fc0118
Pipeline #16260 failed with stage
in 18 minutes and 35 seconds
......@@ -30,7 +30,6 @@ theories/algebra/updates.v
theories/algebra/local_updates.v
theories/algebra/gset.v
theories/algebra/coPset.v
theories/program_logic/binders.v
theories/program_logic/model.v
theories/program_logic/adequacy.v
theories/program_logic/adequacy_inf.v
......
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-03-16.0.6aed7177") | (= "dev") }
"coq-iris" { (= "dev.2019-04-25.0.3a0ab5e6") | (= "dev") }
]
From fri.program_logic Require Export ectx_language ectxi_language binders.
From fri.program_logic Require Export ectx_language ectxi_language.
From fri.algebra Require Export ofe.
From stdpp Require Export strings.
From stdpp Require Export strings binders.
From stdpp Require Import gmap.
(* Same as the heap lang, but we replace the heap with channels for
......
......@@ -29,9 +29,6 @@ Coercion App : expr >-> Funclass.
Coercion Var : string >-> expr.
Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope.
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
......@@ -42,10 +39,10 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : cexpr_scope.
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)
(Match e0 x1%binder e1 x2%binder 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)
(Match e0 x2%binder e2 x1%binder 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.
......@@ -69,43 +66,43 @@ 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.
(* The unicode is already part of the notation "_ ← _; _" for bind. *)
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)
Notation "'rec:' f x := e" := (Rec f%binder x%binder 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)
Notation "'rec:' f x := e" := (RecV f%binder x%binder 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)
Notation "'letp:' x y := e1 'in' e2" := (Letp x%binder y%binder 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))
Notation "'rec:' f x y := e" := (Rec f%binder x%binder (Lam y%binder 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))
Notation "'rec:' f x y := e" := (RecV f%binder x%binder (Lam y%binder 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) ..))
Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder 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) ..))
Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder 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)
Notation "λ: x , e" := (Lam x%binder 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) ..))
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder 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)
Notation "λ: x , e" := (LamV x%binder 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) .. ))
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder 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)
Notation "'let:' x := e1 'in' e2" := (Lam x%binder 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.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%C e1%C)
Notation "'let:' x := e1 'in' e2" := (LamV x%binder 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.
......
From fri.chan_lang Require Export lang tactics.
From stdpp Require Import list.
From stdpp Require Import list gmap.
Import chan_lang.
(* Substitution of closed terms for different variables commutes *)
......
From fri.program_logic Require Export ectx_language ectxi_language binders.
From fri.program_logic Require Export ectx_language ectxi_language.
From fri.algebra Require Export ofe.
From stdpp Require Export strings.
From stdpp Require Export strings binders.
From stdpp Require Import gmap.
Module heap_lang.
......
......@@ -26,9 +26,6 @@ Coercion of_val : val >-> expr.
Coercion Var : string >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope.
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
......@@ -39,10 +36,10 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_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)
(Match e0 x1%binder e1 x2%binder e2)
(e0, x1, e1, x2, e2 at level 200) : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1)
(Match e0 x2%binder e2 x1%binder e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
......@@ -61,43 +58,43 @@ Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
(* The unicode is already part of the notation "_ ← _; _" for bind. *)
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%binder x%binder e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E)
(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%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "'letp:' x y := e1 'in' e2" := (Letp x%bind y%bind e1%E e2%E)
Notation "'letp:' x y := e1 'in' e2" := (Letp x%binder y%binder e1%E e2%E)
(at level 102, x at level 1, y at level 1, e1, e2 at level 200) : expr_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%E))
Notation "'rec:' f x y := e" := (Rec f%binder x%binder (Lam y%binder e%E))
(at level 102, f, x, y at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
Notation "'rec:' f x y := e" := (RecV f%binder x%binder (Lam y%binder e%E))
(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%E) ..))
Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x , e" := (Lam x%bind e%E)
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 102, x at level 1, e at level 200) : 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%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 102, x, y, z at level 1, e at level 200) : expr_scope.
Notation "λ: x , e" := (LamV x%bind e%E)
Notation "λ: x , e" := (LamV x%binder e%E)
(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%E) .. ))
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
(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%E e1%E)
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E)
Notation "'let:' x := e1 'in' e2" := (LamV x%binder e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
......@@ -114,8 +111,8 @@ Notation NONEV := (InjLV #()).
Notation SOMEV x := (InjRV x).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
From fri.heap_lang Require Export lang tactics.
From stdpp Require Import list.
From stdpp Require Import list gmap.
Import heap_lang.
(* Substitution of closed terms for different variables commutes *)
......
From stdpp Require Export strings gmap.
From fri.program_logic Require Import ectxi_language.
Inductive binder := BAnon | BNamed : string binder.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof. solve_decision. Defined.
Instance set_unfold_cons_binder x mx X P :
SetUnfold (x X) P SetUnfold (x mx :b: X) (BNamed x = mx P).
Proof.
constructor. rewrite -(set_unfold (x X) P).
destruct mx; rewrite /= ?elem_of_cons; naive_solver.
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