Bump Iris.

opam

@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-04-24.0.d2f8b689") | (= "dev") }
+  "coq-iris" { (= "dev.2019-04-25.0.3a0ab5e6") | (= "dev") }
 ]

theories/lang/lang.v

 From iris.program_logic Require Export language ectx_language ectxi_language.
-From stdpp Require Export strings.
+From stdpp Require Export strings binders.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
@@ -20,39 +20,13 @@ Inductive bin_op : Set :=
 Inductive order : Set :=
 | ScOrd | Na1Ord | Na2Ord.
 
-Inductive binder := BAnon | BNamed : string → binder.
-Delimit Scope lrust_binder_scope with RustB.
-Bind Scope lrust_binder_scope with binder.
-
-Notation "[ ]" := (@nil binder) : lrust_binder_scope.
-Notation "a :: b" := (@cons binder a%RustB b%RustB)
-  (at level 60, right associativity) : lrust_binder_scope.
+Notation "[ ]" := (@nil binder) : binder_scope.
+Notation "a :: b" := (@cons binder a%binder b%binder)
+  (at level 60, right associativity) : binder_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=
-  (@cons binder x1%RustB (@cons binder x2%RustB
-        (..(@cons binder xn%RustB (@nil binder))..))) : lrust_binder_scope.
-Notation "[ x ]" := (@cons binder x%RustB (@nil binder)) : lrust_binder_scope.
-
-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).
-Fixpoint app_binder (mxl : list binder) (X : list string) : list string :=
-  match mxl with [] => X | b :: mxl => b :b: app_binder mxl X end.
-Infix "+b+" := app_binder (at level 60, right associativity).
-Instance binder_dec_eq : EqDecision binder.
-Proof. solve_decision. Defined.
-
-Instance set_unfold_cons_binder x mx X P :
-  SetUnfoldElemOf x X P → SetUnfoldElemOf 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.
-Instance set_unfold_app_binder x mxl X P :
-  SetUnfoldElemOf x X P → SetUnfoldElemOf x (mxl +b+ X) (BNamed x ∈ mxl ∨ P).
-Proof.
-  constructor. rewrite -(set_unfold (x ∈ X) P).
-  induction mxl as [|?? IH]; set_solver.
-Qed.
+  (@cons binder x1%binder (@cons binder x2%binder
+        (..(@cons binder xn%binder (@nil binder))..))) : binder_scope.
+Notation "[ x ]" := (@cons binder x%binder (@nil binder)) : binder_scope.
 
 Inductive expr :=
 | Var (x : string)
@@ -176,12 +150,12 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
   | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
-Arguments subst_l _%RustB _ _%E.
+Arguments subst_l _%binder _ _%E.
 
 Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                    (e : expr) : expr :=
   Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
-Arguments subst_v _%RustB _ _%E.
+Arguments subst_v _%binder _ _%E.
 
 Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
   Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.

theories/lang/notation.v

@@ -9,9 +9,6 @@ Coercion of_val : val >-> expr.
 
 Coercion Var : string >-> expr.
 
-Coercion BNamed : string >-> binder.
-Notation "<>" := BAnon : lrust_binder_scope.
-
 Notation "[ ]" := (@nil expr) : expr_scope.
 Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=
@@ -45,9 +42,9 @@ Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
   (at level 80) : expr_scope.
 Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
   (at level 80) : expr_scope.
-Notation "'rec:' f xl := e" := (Rec f%RustB xl%RustB e%E)
+Notation "'rec:' f xl := e" := (Rec f%binder xl%binder e%E)
   (at level 102, f, xl at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f xl := e" := (locked (RecV f%RustB xl%RustB e%E))
+Notation "'rec:' f xl := e" := (locked (RecV f%binder xl%binder e%E))
   (at level 102, f, xl at level 1, e at level 200) : val_scope.
 Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
@@ -57,9 +54,9 @@ 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 "λ: xl , e" := (Lam xl%RustB e%E)
+Notation "λ: xl , e" := (Lam xl%binder e%E)
   (at level 102, xl at level 1, e at level 200) : expr_scope.
-Notation "λ: xl , e" := (locked (LamV xl%RustB e%E))
+Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
   (at level 102, xl at level 1, e at level 200) : val_scope.
 
 Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
@@ -69,22 +66,22 @@ Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
 Notation "'return:'" := "return" : expr_scope.
 
 Notation "'let:' x := e1 'in' e2" :=
-  ((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
+  ((Lam (@cons binder x%binder nil) e2%E) (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
 Notation "e1 ;; e2" := (let: <> := e1 in e2)%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 (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
+  (LamV (@cons binder x%binder nil) e2%E (@cons expr e1%E nil))
   (at level 102, x at level 1, e1, e2 at level 150) : val_scope.
 Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
 
 Notation "'letcont:' k xl := e1 'in' e2" :=
-  ((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
+  ((Lam (@cons binder k%binder nil) e2%E) [Rec k%binder xl%binder e1%E])
   (at level 102, k, xl at level 1, e1, e2 at level 150) : expr_scope.
 Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
-  ((Lam (@cons binder k1%RustB nil) e1%E) [Rec k2%RustB ((fun _ : eq k1%RustB k2%RustB => xl%RustB) eq_refl) e2%E])
+  ((Lam (@cons binder k1%binder nil) e1%E) [Rec k2%binder ((fun _ : eq k1%binder k2%binder => xl%binder) eq_refl) e2%E])
   (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
 
 Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E