From f639060d7c438a3c7e3988b4446c60ab05e42fc1 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 20 Jun 2017 19:57:05 +0100
Subject: [PATCH] restored MapsOld for purposes of comparison

---
 src/Maps.lagda    |  15 +-
 src/MapsOld.lagda | 340 ++++++++++++++++++++++++++++++++++++++++++++++
 src/Stlc.lagda    |   6 +-
 3 files changed, 350 insertions(+), 11 deletions(-)
 create mode 100644 src/MapsOld.lagda

diff --git a/src/Maps.lagda b/src/Maps.lagda
index 1cefbdc5..b0f1afd9 100644
--- a/src/Maps.lagda
+++ b/src/Maps.lagda
@@ -36,7 +36,7 @@ standard library, wherever they overlap.
 open import Data.Nat         using (ℕ)
 open import Data.Empty       using (⊥; ⊥-elim)
 open import Data.Maybe       using (Maybe; just; nothing)
-open import Data.String      using (String)
+-- open import Data.String      using (String)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
                              using (_≡_; refl; _≢_; trans; sym)
@@ -54,7 +54,8 @@ we repeat its definition here.
 
 \begin{code}
 data Id : Set where
-  id : String → Id
+  -- id : String → Id
+  id : ℕ → Id
 \end{code}
 
 We recall a standard fact of logic.
@@ -69,7 +70,7 @@ by deciding equality on the underlying strings.
 
 \begin{code}
 _≟_ : (x y : Id) → Dec (x ≡ y)
-id x ≟ id y with x Data.String.≟ y
+id x ≟ id y with x Data.Nat.≟ y -- x Data.String.≟ y
 id x ≟ id y | yes refl  =  yes refl
 id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
   where
@@ -81,9 +82,9 @@ We define some identifiers for future use.
 
 \begin{code}
 x y z : Id
-x = id "x"
-y = id "y"
-z = id "z"
+x = id 0 -- "x"
+y = id 1 -- "y"
+z = id 2 -- "z"
 \end{code}
 
 ## Total Maps
@@ -288,7 +289,6 @@ updates.
 
 <div class="hidden">
 \begin{code}
-{-
   update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
                    → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
   update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
@@ -296,7 +296,6 @@ updates.
   ... | no  x≢z | yes y≡z rewrite y≡z = {! sym (update-eq′ ρ z w)!}  
   ... | yes x≡z | no  y≢z rewrite x≡z = {! update-eq′ ρ z v!}  
   ... | no  x≢z | no  y≢z = {! trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
--}
 
 {-
 Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?
diff --git a/src/MapsOld.lagda b/src/MapsOld.lagda
new file mode 100644
index 00000000..673b6959
--- /dev/null
+++ b/src/MapsOld.lagda
@@ -0,0 +1,340 @@
+---
+title     : "Maps: Total and Partial Maps"
+layout    : page
+permalink : /Maps
+---
+
+Maps (or dictionaries) are ubiquitous data structures, both in software
+construction generally and in the theory of programming languages in particular;
+we're going to need them in many places in the coming chapters.  They also make
+a nice case study using ideas we've seen in previous chapters, including
+building data structures out of higher-order functions (from [Basics]({{
+"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use
+of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url
+}})). 
+
+We'll define two flavors of maps: _total_ maps, which include a
+"default" element to be returned when a key being looked up
+doesn't exist, and _partial_ maps, which return an `Maybe` to
+indicate success or failure.  The latter is defined in terms of
+the former, using `nothing` as the default element.
+
+## The Agda Standard Library
+
+One small digression before we start.
+
+Unlike the chapters we have seen so far, this one does not
+import the chapter before it (and, transitively, all the
+earlier chapters).  Instead, in this chapter and from now, on
+we're going to import the definitions and theorems we need
+directly from Agda's standard library stuff.  You should not notice
+much difference, though, because we've been careful to name our
+own definitions and theorems the same as their counterparts in the
+standard library, wherever they overlap.
+
+\begin{code}
+open import Function         using (_∘_)
+open import Data.Bool        using (Bool; true; false)
+open import Data.Empty       using (⊥; ⊥-elim)
+open import Data.Maybe       using (Maybe; just; nothing)
+open import Data.Nat         using (ℕ)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+\end{code}
+
+Documentation for the standard library can be found at
+<https://agda.github.io/agda-stdlib/>.
+
+## Identifiers
+
+First, we need a type for the keys that we use to index into our
+maps.  For this purpose, we again use the type Id` from the
+[Lists](sf/Lists.html) chapter.  To make this chapter self contained,
+we repeat its definition here, together with the equality comparison
+function for ids and its fundamental property.
+
+\begin{code}
+data Id : Set where
+  id : ℕ → Id
+\end{code}
+
+\begin{code}
+_≟_ : (x y : Id) → Dec (x ≡ y)
+id x ≟ id y with x Data.Nat.≟ y
+id x ≟ id y | yes x=y rewrite x=y = yes refl
+id x ≟ id y | no  x≠y = no (x≠y ∘ id-inj)
+  where
+    id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
+    id-inj refl = refl
+\end{code}
+
+## Total Maps
+
+Our main job in this chapter will be to build a definition of
+partial maps that is similar in behavior to the one we saw in the
+[Lists](sf/Lists.html) chapter, plus accompanying lemmas about their
+behavior.
+
+This time around, though, we're going to use _functions_, rather
+than lists of key-value pairs, to build maps.  The advantage of
+this representation is that it offers a more _extensional_ view of
+maps, where two maps that respond to queries in the same way will
+be represented as literally the same thing (the same function),
+rather than just "equivalent" data structures.  This, in turn,
+simplifies proofs that use maps.
+
+We build partial maps in two steps.  First, we define a type of
+_total maps_ that return a default value when we look up a key
+that is not present in the map.
+
+\begin{code}
+TotalMap : Set → Set
+TotalMap A = Id → A
+\end{code}
+
+Intuitively, a total map over anfi element type $$A$$ _is_ just a
+function that can be used to look up ids, yielding $$A$$s.
+
+\begin{code}
+module TotalMap where
+\end{code}
+
+The function `empty` yields an empty total map, given a
+default element; this map always returns the default element when
+applied to any id.
+
+\begin{code}
+  empty : ∀ {A} → A → TotalMap A
+  empty x = λ _ → x
+\end{code}
+
+More interesting is the `update` function, which (as before) takes
+a map $$m$$, a key $$x$$, and a value $$v$$ and returns a new map that
+takes $$x$$ to $$v$$ and takes every other key to whatever $$m$$ does.
+
+\begin{code}
+  update : ∀ {A} → TotalMap A -> Id -> A -> TotalMap A
+  update m x v y with x ≟ y
+  ... | yes x=y = v
+  ... | no  x≠y = m y
+\end{code}
+
+This definition is a nice example of higher-order programming.
+The `update` function takes a _function_ $$m$$ and yields a new
+function $$\lambda x'.\vdots$$ that behaves like the desired map.
+
+For example, we can build a map taking ids to bools, where `id
+3` is mapped to `true` and every other key is mapped to `false`,
+like this:
+
+\begin{code}
+  examplemap : TotalMap Bool
+  examplemap = update (update (empty false) (id 1) false) (id 3) true
+\end{code}
+
+This completes the definition of total maps.  Note that we don't
+need to define a `find` operation because it is just function
+application!
+
+\begin{code}
+  test_examplemap0 : examplemap (id 0) ≡ false
+  test_examplemap0 = refl
+
+  test_examplemap1 : examplemap (id 1) ≡ false
+  test_examplemap1 = refl
+
+  test_examplemap2 : examplemap (id 2) ≡ false
+  test_examplemap2 = refl
+
+  test_examplemap3 : examplemap (id 3) ≡ true
+  test_examplemap3 = refl
+\end{code}
+
+To use maps in later chapters, we'll need several fundamental
+facts about how they behave.  Even if you don't work the following
+exercises, make sure you thoroughly understand the statements of
+the lemmas!  (Some of the proofs require the functional
+extensionality axiom, which is discussed in the [Logic]
+chapter and included in the Agda standard library.)
+
+#### Exercise: 1 star, optional (apply-empty)
+First, the empty map returns its default element for all keys:
+
+\begin{code}
+  postulate
+    apply-empty : ∀ {A x v} → empty {A} v x ≡ v
+\end{code}
+
+<div class="hidden">
+\begin{code}
+  apply-empty′ : ∀ {A x v} → empty {A} v x ≡ v
+  apply-empty′ = refl
+\end{code}
+</div>
+
+#### Exercise: 2 stars, optional (update-eq)
+Next, if we update a map $$m$$ at a key $$x$$ with a new value $$v$$
+and then look up $$x$$ in the map resulting from the `update`, we get
+back $$v$$:
+
+\begin{code}
+  postulate
+    update-eq : ∀ {A v} (m : TotalMap A) (x : Id)
+              → (update m x v) x ≡ v
+\end{code}
+
+<div class="hidden">
+\begin{code}
+  update-eq′ : ∀ {A v} (m : TotalMap A) (x : Id)
+             → (update m x v) x ≡ v
+  update-eq′ m x with x ≟ x
+  ... | yes x=x = refl
+  ... | no  x≠x = ⊥-elim (x≠x refl)
+\end{code}
+</div>
+
+#### Exercise: 2 stars, optional (update-neq)
+On the other hand, if we update a map $$m$$ at a key $$x$$ and
+then look up a _different_ key $$y$$ in the resulting map, we get
+the same result that $$m$$ would have given:
+
+\begin{code}
+  update-neq : ∀ {A v} (m : TotalMap A) (x y : Id)
+             → x ≢ y → (update m x v) y ≡ m y
+  update-neq m x y x≠y with x ≟ y
+  ... | yes x=y = ⊥-elim (x≠y x=y)
+  ... | no  _   = refl
+\end{code}
+
+#### Exercise: 2 stars, optional (update-shadow)
+If we update a map $$m$$ at a key $$x$$ with a value $$v_1$$ and then
+update again with the same key $$x$$ and another value $$v_2$$, the
+resulting map behaves the same (gives the same result when applied
+to any key) as the simpler map obtained by performing just
+the second `update` on $$m$$:
+
+\begin{code}
+  postulate
+    update-shadow : ∀ {A v1 v2} (m : TotalMap A) (x y : Id)
+                  → (update (update m x v1) x v2) y ≡ (update m x v2) y
+\end{code}
+
+<div class="hidden">
+\begin{code}
+  update-shadow′ : ∀ {A v1 v2} (m : TotalMap A) (x y : Id)
+                 → (update (update m x v1) x v2) y ≡ (update m x v2) y
+  update-shadow′ m x y
+      with x ≟ y
+  ... | yes x=y = refl
+  ... | no  x≠y = update-neq m x y x≠y
+\end{code}
+</div>
+
+#### Exercise: 2 stars (update-same)
+Prove the following theorem, which states that if we update a map to
+assign key $$x$$ the same value as it already has in $$m$$, then the
+result is equal to $$m$$:
+
+\begin{code}
+  postulate
+    update-same : ∀ {A} (m : TotalMap A) (x y : Id)
+                → (update m x (m x)) y ≡ m y
+\end{code}
+
+<div class="hidden">
+\begin{code}
+  update-same′ : ∀ {A} (m : TotalMap A) (x y : Id)
+               → (update m x (m x)) y ≡ m y
+  update-same′ m x y
+    with x ≟ y
+  ... | yes x=y rewrite x=y = refl
+  ... | no  x≠y = refl
+\end{code}
+</div>
+
+#### Exercise: 3 stars, recommended (update-permute)
+Prove one final property of the `update` function: If we update a map
+$$m$$ at two distinct keys, it doesn't matter in which order we do the
+updates.
+
+\begin{code}
+  postulate
+    update-permute : ∀ {A v1 v2} (m : TotalMap A) (x1 x2 y : Id)
+                   → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+                             ≡ (update (update m x1 v1) x2 v2) y
+\end{code}
+
+<div class="hidden">
+\begin{code}
+  update-permute′ : ∀ {A v1 v2} (m : TotalMap A) (x1 x2 y : Id)
+                  → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+                            ≡ (update (update m x1 v1) x2 v2) y
+  update-permute′ {A} {v1} {v2} m x1 x2 y x1≠x2
+    with x1 ≟ y | x2 ≟ y
+  ... | yes x1=y | yes x2=y = ⊥-elim (x1≠x2 (trans x1=y (sym x2=y)))
+  ... | no  x1≠y | yes x2=y rewrite x2=y = update-eq′ m y 
+  ... | yes x1=y | no  x2≠y rewrite x1=y = sym (update-eq′ m y)
+  ... | no  x1≠y | no  x2≠y =
+    trans (update-neq m x2 y x2≠y) (sym (update-neq m x1 y x1≠y))
+\end{code}
+</div>
+
+## Partial maps
+
+Finally, we define _partial maps_ on top of total maps.  A partial
+map with elements of type `A` is simply a total map with elements
+of type `Maybe A` and default element `nothing`.
+
+\begin{code}
+PartialMap : Set → Set
+PartialMap A = TotalMap (Maybe A)
+\end{code}
+
+\begin{code}
+module PartialMap where
+\end{code}
+
+\begin{code}
+  empty : ∀ {A} → PartialMap A
+  empty = TotalMap.empty nothing
+\end{code}
+
+\begin{code}
+  update : ∀ {A} (m : PartialMap A) (x : Id) (v : A) → PartialMap A
+  update m x v = TotalMap.update m x (just v)
+\end{code}
+
+We can now lift all of the basic lemmas about total maps to
+partial maps.
+
+\begin{code}
+  update-eq : ∀ {A v} (m : PartialMap A) (x : Id)
+            → (update m x v) x ≡ just v
+  update-eq m x = TotalMap.update-eq m x
+\end{code}
+
+\begin{code}
+  update-neq : ∀ {A v} (m : PartialMap A) (x y : Id)
+             → x ≢ y → (update m x v) y ≡ m y
+  update-neq m x y x≠y = TotalMap.update-neq m x y x≠y
+\end{code}
+
+\begin{code}
+  update-shadow : ∀ {A v1 v2} (m : PartialMap A) (x y : Id)
+                → (update (update m x v1) x v2) y ≡ (update m x v2) y
+  update-shadow m x y = TotalMap.update-shadow m x y
+\end{code}
+
+\begin{code}
+  update-same : ∀ {A v} (m : PartialMap A) (x y : Id)
+              → m x ≡ just v
+              → (update m x v) y ≡ m y
+  update-same m x y mx=v rewrite sym mx=v = TotalMap.update-same m x y
+\end{code}
+
+\begin{code}
+  update-permute : ∀ {A v1 v2} (m : PartialMap A) (x1 x2 y : Id)
+                 → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+                           ≡ (update (update m x1 v1) x2 v2) y
+  update-permute m x1 x2 y x1≠x2 = TotalMap.update-permute m x1 x2 y x1≠x2
+\end{code}
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index dcfa86bc..c96bc0d7 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -45,9 +45,9 @@ data Term : Set where
 Some examples.
 \begin{code}
 f x y : Id
-f  =  id "f"
-x  =  id "x"
-y  =  id "y"
+f  =  id 0 -- "f"
+x  =  id 1 -- "x"
+y  =  id 2 -- "y"
 
 I[𝔹] I[𝔹⇒𝔹] K[𝔹][𝔹] not[𝔹] : Term 
 I[𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (varᵀ x))