diff --git a/opam b/opam
index 5e505ad7365af59c4161a716dacd4c9e901a49b6..0f251f2848e048cef046f007307518ff50112f53 100644
--- a/opam
+++ b/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") }
]
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index cf6a0bf817f1b762ce796bd9f9a48cc15c4fec55..09f0425297e1519070538623db6528e15cd2824a 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,5 +1,5 @@
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.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 588a67bee4206f5ec0c8c97aed17f18ea7803047..d4f5d697b4f140a33ebcb78810877b23756bfc57 100644
--- a/theories/lang/notation.v
+++ b/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