[ deprecate ] Relation/Binary.PropositionalEquality.inspect and README.Inspect (#1580 / #1630 / #1930 redux) (#2981)

* remove: module `README.Inspect`

* refactor: deprecate module `README.Inspect`

* refactor: introduce `Graph`; deprecate `Reveal`, `[_]`, `inspect`

* `CHANGELOG`

* fix : `README.Data.Wrap` by narrowing `import`s

Author: jamesmckinna

CHANGELOG.md

@@ -6,6 +6,13 @@ The library has been tested using Agda 2.8.0.
 Highlights
 ----------
 
+### Deprecated `Relation.Binary.PropositionalEquality.inspect`, in favour
+    of `with ... in ...` syntax (issue #1580; PRs #1630, #1930, #2934)
+
+* In `Relation.Binary.PropositionalEquality`, the record type `Reveal_·_is_`
+  and its principal mode of use, `inspect`, have been deprecated in favour of
+  the new `with ... in ...` syntax. See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/stable/language/with-abstraction.html#with-abstraction-equality).
+
 Bug-fixes
 ---------
 
@@ -131,6 +138,13 @@ Deprecated names
   decidable     ↦   _∪?_
   ```
 
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  Reveal_·_is_   ↦   Graph.View
+  inspect        ↦   Graph.view
+  pattern [_]    ↦   λ eq → record { fx≡y = eq }
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
@@ -658,6 +672,17 @@ Additions to existing modules
   ¬[x≢x] : .(x ≢ x) → Whatever
   ```
 
+* In `Relation.Binary.PropositionalEquality`, replacing `Reveal`/`inspect`:
+  ```agda
+  module Graph {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) where
+
+    record View (y : B x) : Set (a ⊔ b) where
+      field fx≡y : f x ≡ y
+
+    view : View (f x)
+    view = record { fx≡y = refl }
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η           : A → ¬ ¬ A

doc/README.agda

@@ -241,11 +241,6 @@ import README.Debug.Trace
 
 import README.Nary
 
--- Explaining the inspect idiom: use case, equivalent handwritten
--- auxiliary definitions, and implementation details.
-
-import README.Inspect
-
 -- Explaining how to use the automatic solvers
 
 import README.Tactic.MonoidSolver

doc/README/Data/Wrap.agda

@@ -108,7 +108,7 @@ module Instances where
 
 module Unification where
 
-  open import Relation.Binary.PropositionalEquality
+  open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
   module Naïve where
 

doc/README/Inspect.agda

@@ -1,19 +1,28 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Explaining how to use the inspect idiom and elaborating on the way
--- it is implemented in the standard library.
+-- This module is DEPRECATED.
+--
+-- The record type `Reveal_·_is_`, and its principal mode of use,
+-- via the `inspect` function described below, have been deprecated
+-- in favour of the `with ... in ...` syntax. See the documentation
+--
+-- https://agda.readthedocs.io/en/stable/language/with-abstraction.html#with-abstraction-equality
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Inspect where
 
+{-# WARNING_ON_IMPORT
+"README.Inspect was deprecated in v2.4."
+#-}
+
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Binary.PropositionalEquality using (inspect; [_])
+import Relation.Binary.PropositionalEquality as ≡ using (inspect; [_])
 
 ------------------------------------------------------------------------
 -- Using inspect
@@ -72,9 +81,9 @@ plus-eq-+ (suc m) n      = refl
 -- the second one is trivial.
 
 plus-eq-with : ∀ m n → Plus-eq m n (m + n)
-plus-eq-with m n with m + n | inspect (m +_) n
-... | zero  | [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
-... | suc p | [ m+n≡1+p ] = m+n≡1+p
+plus-eq-with m n with m + n | ≡.inspect (m +_) n
+... | zero  | ≡.[ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
+... | suc p | ≡.[ m+n≡1+p ] = m+n≡1+p
 
 
 ------------------------------------------------------------------------

src/Relation/Binary/PropositionalEquality.agda

@@ -62,7 +62,7 @@ naturality : ∀ {x y} {x≡y : x ≡ y} {f g : A → B}
              (f≡g : ∀ x → f x ≡ g x) →
              trans (cong f x≡y) (f≡g y) ≡ trans (f≡g x) (cong g x≡y)
 naturality {x = x} {x≡y = refl} f≡g =
-  f≡g x               ≡⟨ sym (trans-reflʳ _) ⟩
+  f≡g x               ≡⟨ trans-reflʳ _ ⟨
   trans (f≡g x) refl  ∎
   where open ≡-Reasoning
 
@@ -71,9 +71,9 @@ naturality {x = x} {x≡y = refl} f≡g =
 cong-≡id : ∀ {f : A → A} {x : A} (f≡id : ∀ x → f x ≡ x) →
            cong f (f≡id x) ≡ f≡id (f x)
 cong-≡id {f = f} {x} f≡id = begin
-  cong f fx≡x                                    ≡⟨ sym (trans-reflʳ _) ⟩
-  trans (cong f fx≡x) refl                       ≡⟨ cong (trans _) (sym (trans-symʳ fx≡x)) ⟩
-  trans (cong f fx≡x) (trans fx≡x (sym fx≡x))    ≡⟨ sym (trans-assoc (cong f fx≡x)) ⟩
+  cong f fx≡x                                    ≡⟨ trans-reflʳ _ ⟨
+  trans (cong f fx≡x) refl                       ≡⟨ cong (trans _) (trans-symʳ fx≡x) ⟨
+  trans (cong f fx≡x) (trans fx≡x (sym fx≡x))    ≡⟨ trans-assoc (cong f fx≡x) ⟨
   trans (trans (cong f fx≡x) fx≡x) (sym fx≡x)    ≡⟨ cong (λ p → trans p (sym _)) (naturality f≡id) ⟩
   trans (trans f²x≡x (cong id fx≡x)) (sym fx≡x)  ≡⟨ cong (λ p → trans (trans f²x≡x p) (sym fx≡x)) (cong-id _) ⟩
   trans (trans f²x≡x fx≡x) (sym fx≡x)            ≡⟨ trans-assoc f²x≡x ⟩
@@ -92,26 +92,15 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
 
 
 ------------------------------------------------------------------------
--- Inspect
+-- The graph view of a function
 
--- Inspect can be used when you want to pattern match on the result r
--- of some expression e, and you also need to "remember" that r ≡ e.
+module Graph {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) where
 
--- See README.Inspect for an explanation of how/why to use this.
+  record View (y : B x) : Set (a ⊔ b) where
+    field fx≡y : f x ≡ y
 
--- Normally (but not always) the new `with ... in` syntax described at
--- https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#with-abstraction-equality
--- can be used instead."
-
-record Reveal_·_is_ {A : Set a} {B : A → Set b}
-                    (f : (x : A) → B x) (x : A) (y : B x) :
-                    Set (a ⊔ b) where
-  constructor [_]
-  field eq : f x ≡ y
-
-inspect : ∀ {A : Set a} {B : A → Set b}
-          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
-inspect f x = [ refl ]
+  view : View (f x)
+  view = record { fx≡y = refl }
 
 
 ------------------------------------------------------------------------
@@ -130,3 +119,30 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
+-- Version 2.4
+
+module _ {A : Set a} {B : A → Set b} where
+
+  open Graph
+
+  Reveal_·_is_ : (f : (x : A) → B x) (x : A) (y : B x) → Set (a ⊔ b)
+  Reveal f · x is y = View f x y
+
+  inspect : (f : (x : A) → B x) (x : A) → Reveal f · x is f x
+  inspect = view
+
+  pattern [_] eq = record { fx≡y = eq }
+  {-# WARNING_ON_USAGE [_]
+  "Warning: [_] was deprecated in v2.4.
+  Please use the `with ... in eq` syntax instead. "
+  #-}
+  {-# WARNING_ON_USAGE inspect
+  "Warning: inspect was deprecated in v2.4.
+  Please use the `with ... in eq` syntax described at
+  https://agda.readthedocs.io/en/stable/language/with-abstraction.html#with-abstraction-equality instead."
+  #-}
+  {-# WARNING_ON_USAGE Reveal_·_is_
+  "Warning: Reveal_·_is_ was deprecated in v2.4.
+  Please use the `with ... in eq` syntax described at
+  https://agda.readthedocs.io/en/stable/language/with-abstraction.html#with-abstraction-equality instead."
+  #-}