Merge branch 'robbert/kill_locked_value_lambdas' into 'master'

Get rid of locked value lambdas

See merge request iris/iris!223

CHANGELOG.md

@@ -103,6 +103,9 @@ Changes in Coq:
 * The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
   sets, instead of just for cofinite sets. The versions with cofinite
   sets have been renamed to use the `_cofinite` suffix.
+* Remove locked value lambdas. The value scope notations `rec: f x := e` and
+  `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
+  smarter to no longer unfold lambdas/recs that occur behind definitions.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

HeapLang.md

@@ -42,10 +42,6 @@ We define a whole lot of short-hands, such as non-recursive functions (`λ:`),
 let-bindings, sequential composition, and a more conventional `match:` that has
 binders in both branches.
 
-Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`)
-are *locked*.  This is to prevent them from being unfolded and reduced too
-eagerly.
-
 The widely used `#` is a short-hand to turn a basic literal (an integer, a
 location, a boolean literal or a unit value) into a value.  Since values coerce
 to expressions, `#` is widely used whenever a Coq value needs to be placed into
@@ -62,9 +58,10 @@ Tactics to take one or more pure program steps:
 - `wp_pure`: Perform one pure reduction step.  Pure steps are defined by the
   `PureExec` typeclass and include beta reduction, projections, constructors, as
   well as unary and binary arithmetic operators.
-- `wp_pures`: Perform as many pure reduction steps as possible.
+- `wp_pures`: Perform as many pure reduction steps as possible. This
+  tactic will **not** reduce lambdas/recs that are hidden behind a definition.
 - `wp_rec`, `wp_lam`: Perform a beta reduction.  Unlike `wp_pure`, this will
-  also reduce locked lambdas.
+  also reduce lambdas that are hidden behind a definition.
 - `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
 - `wp_proj`: Reduce a projection.
 - `wp_if_true`, `wp_if_false`, `wp_if`: Reduce a conditional expression. The
@@ -122,7 +119,7 @@ The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
 value lambda).  However, the *specification* for parallel composition should use
 value lambdas, because prior to applying it the term will be reduced as much as
 possible to achieve a normal form.  To facilitate this, we define a copy of the
-`e1 ||| e2` notation in the value scope that uses *unlocked* value lambdas.
+`e1 ||| e2` notation in the value scope that uses value lambdas.
 This is not actually a value, but we still but it in the value scope to
 differentiate from the other notation that uses expression lambdas.  (In the
 future, we might decide to add a separate scope for this.)  Then, we write the

theories/heap_lang/lib/assert.v

@@ -7,11 +7,12 @@ Set Default Proof Using "Type".
 Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
 (* just below ;; *)
-Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
+Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
+Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.
 
 Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
-  WP assert (LamV BAnon e)%V @ E [{ Φ }].
+  WP (assert: e)%V @ E [{ Φ }].
 Proof.
   iIntros "HΦ". wp_lam.
   wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
@@ -19,7 +20,7 @@ Qed.
 
 Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
-  WP assert (LamV BAnon e)%V @ E {{ Φ }}.
+  WP (assert: e)%V @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". wp_lam.
   wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.

theories/heap_lang/lib/par.v

@@ -12,7 +12,7 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
+Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".

theories/heap_lang/lifting.v

@@ -91,18 +91,26 @@ Local Ltac solve_pure_exec :=
   subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
     constructor; [solve_exec_safe | solve_exec_puredet].
 
+(** The behavior of the various [wp_] tactics with regard to lambda differs in
+the following way:
+
+- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
+- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
+
+To realize this behavior, we define the class [AsRecV v f x erec], which takes a
+value [v] as its input, and turns it into a [RecV f x erec] via the instance
+[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
+[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
+not if [v] contains a lambda/rec that is hidden behind a definition.
+
+To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
+behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
 Class AsRecV (v : val) (f x : binder) (erec : expr) :=
   as_recv : v = RecV f x erec.
-Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
-
-(* Pure reductions are automatically performed before any wp_ tactics
-   handling impure operations. Since we do not want these tactics to
-   unfold locked terms, we do not register this instance explicitely,
-   but only activate it by hand in the `wp_rec` tactic, where we
-   *actually* want it to unlock. *)
-Lemma AsRecV_recv_locked v f x e :
-  AsRecV v f x e → AsRecV (locked v) f x e.
-Proof. by unlock. Qed.
+Hint Mode AsRecV ! - - - : typeclass_instances.
+Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
+Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
+  apply AsRecV_recv : typeclass_instances.
 
 Instance pure_recc f x (erec : expr) :
   PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).

theories/heap_lang/notation.v

@@ -85,7 +85,7 @@ 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)
   (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" := (RecV f%bind x%bind 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)
@@ -98,7 +98,7 @@ 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) ..))
   (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" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind 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.
 
@@ -111,21 +111,10 @@ Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
 
-(* When parsing lambdas, we want them to be locked (so as to avoid needless
-unfolding by tactics and unification). However, unlocked lambda-values sometimes
-appear as part of compound expressions, in which case we want them to be pretty
-printed too. We achieve that by using printing only notations for the non-locked
-notation. *)
 Notation "λ: x , e" := (LamV x%bind e%E)
-  (at level 200, x at level 1, e at level 200,
-   format "'[' 'λ:'  x ,  '/  ' e ']'", only printing) : val_scope.
-Notation "λ: x , e" := (locked (LamV x%bind 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) .. ))
-  (at level 200, x, y, z at level 1, e at level 200,
-   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'", only printing) : val_scope.
-Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
 

theories/heap_lang/proofmode.v

@@ -105,17 +105,16 @@ Ltac wp_pures :=
   repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
                              magically spawns. *)
 
-(* The handling of beta-reductions with wp_rec needs special care in
-  order to allow it to unlock locked `RecV` values: We first put
-  `AsRecV_recv_locked` in the current environment so that it can be
-  used as an instance by the typeclass resolution system, then we
-  perform the reduction, and finally we clear this new hypothesis.
-
-  The reason is that we do not want impure wp_ tactics to unfold
-  locked terms, while we want them to execute arbitrary pure steps. *)
+(** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce
+lambdas/recs that are hidden behind a definition, i.e. they should use
+[AsRecV_recv] as a proper instance instead of a [Hint Extern].
+
+We achieve this by putting [AsRecV_recv] in the current environment so that it
+can be used as an instance by the typeclass resolution system. We then perform
+the reduction, and finally we clear this new hypothesis. *)
 Tactic Notation "wp_rec" :=
   let H := fresh in
-  assert (H := AsRecV_recv_locked);
+  assert (H := AsRecV_recv);
   wp_pure (App _ _);
   clear H.