Commit d557cfbf authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent d6fb3aae
Pipeline #16261 failed with stage
in 12 minutes and 48 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2019-04-24.0.d2f8b689") | (= "dev") }
"coq-iris" { (= "dev.2019-04-25.0.3a0ab5e6") | (= "dev") }
]
......@@ -7,7 +7,7 @@ This file is mostly a copy of [heap_lang/lang] in the Iris repository. The only
change is the addition of the [Free] operator. *)
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.algebra Require Export ofe.
From stdpp Require Export strings.
From stdpp Require Export strings binders.
From stdpp Require Import gmap gmultiset.
Set Default Proof Using "Type".
......@@ -28,22 +28,6 @@ Inductive bin_op : Set :=
| ShiftLOp | ShiftROp (* Shifts *)
| LeOp | LtOp | EqOp. (* Relations *)
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_eq_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.
Inductive expr :=
(* Base lambda calculus *)
| Var (x : string)
......@@ -177,11 +161,6 @@ Proof.
| 10 => LeOp | 11 => LtOp | _ => EqOp
end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
(λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
set (enc := fix go e :=
......
......@@ -16,9 +16,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").
......@@ -52,11 +49,11 @@ Moreover, if the branches do not fit on a single line, it will be printed as:
end
*)
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,
format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : 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.
......@@ -84,10 +81,10 @@ Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
(* The breaking point '/ ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
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 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
Notation "'rec:' f x := e" := (locked (RecV f%binder x%binder e%E))
(at level 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
......@@ -97,19 +94,19 @@ Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
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 .. 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 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
Notation "'rec:' f x y .. z := e" := (locked (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..)))
(at level 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope.
(* The breaking point '/ ' makes sure that the body of the λ: is indented
by two spaces in case the whole λ: does not fit on a single line. *)
Notation "λ: x , e" := (Lam x%bind e%E)
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : 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 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
......@@ -119,20 +116,20 @@ appear as part of compound expressions, in which case we want them to be pretty
printed too. We achieve that by first defining the non-locked notation, and then
the locked notation. Both will be used for pretty-printing, but only the last
will be used for parsing. *)
Notation "λ: x , e" := (LamV x%bind e%E)
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x , e" := (locked (LamV x%bind e%E))
Notation "λ: x , e" := (locked (LamV x%binder e%E))
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : 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 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
Notation "λ: x y .. z , e" := (locked (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. )))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : 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 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
......@@ -153,8 +150,8 @@ Notation NONEV := (InjLV #()) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).
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, only parsing) : 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.
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