From 80f67e2fac7ce72ed3fd03ba101ac90bfae1d080 Mon Sep 17 00:00:00 2001
From: dianne <diannes.gm@gmail.com>
Date: Mon, 20 Aug 2018 13:31:16 -0700
Subject: [PATCH] a couple high-level comments

---
 Enumeration.agda | 6 ++++++
 Moves.agda       | 5 ++++-
 Rules.agda       | 4 ++++
 3 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/Enumeration.agda b/Enumeration.agda
index c76fc45..241ec5f 100644
--- a/Enumeration.agda
+++ b/Enumeration.agda
@@ -25,6 +25,12 @@ open import Data.Sum as Sum
 open import Category.Monad
 import Level
 
+-- in order to talk about the number of mines adjacent to a tile, we define Enumeration:
+-- a list of all the elements of a type, with each appearing once.
+-- our goal here is to develop the necessary machinery to do that. specifically, we need
+-- that all Enumerations of a type have the same length (they're unique up to bag equality),
+-- and we need to be able to be able to enumerate the adjacent mines of a tile, (which we
+-- get by enumerating any m×n grid and filtering by a predicate)
 record Enumeration A : Set where
   field
     list : List A
diff --git a/Moves.agda b/Moves.agda
index fcd1b8f..4331c53 100644
--- a/Moves.agda
+++ b/Moves.agda
@@ -12,18 +12,21 @@ data Guess : Set where
   mine⚐ : Guess
   safe⚐ : Guess
 
+-- tile filling: an unknown tile can be filled with anything
 data _↝▣_ : Tile → KnownTile → Set where
   ↝▣known   : ∀ s → known s ↝▣ s
   ↝▣unknown : ∀ s → unknown ↝▣ s
 
+-- board filling: can a fully filled board be reached by filling in the unknown tiles of a partial board?
 _↝⊞_ : ∀ {bounds} → Board Tile bounds → Board KnownTile bounds → Set
 holey ↝⊞ filled = ∀ coords → lookup coords holey ↝▣ lookup coords filled
 
+-- guessing: is a guess of a tile's type valid for that tile?
 data _↝⚐_ : Guess → KnownTile → Set where
   ↝⚐mine : mine⚐ ↝⚐ mine
   ↝⚐safe : ∀ n → safe⚐ ↝⚐ safe n
 
--- move validity relation: a guess is valid when it holds in every rule-respecting way to fill the board's unfilled tiles
+-- move validity: a guess as to a tile's identity on a board is valid when it holds in every rule-respecting way to fill the board's unfilled tiles
 _[_]↝✓_ : ∀ {bounds} → Board Tile bounds → Coords bounds → Guess → Set
 grid [ coords ]↝✓ guess = ∀ grid′ →
   grid ↝⊞ grid′ →
diff --git a/Rules.agda b/Rules.agda
index b7726cb..d15b178 100644
--- a/Rules.agda
+++ b/Rules.agda
@@ -17,14 +17,18 @@ data KnownTile : Set where
   mine : KnownTile
   safe : ℕ → KnownTile
 
+-- a numbered tile is good if the number on it matches the number of mines adjacent to it.
+-- since all Enumerations of a type have the same length, it's sufficient to provide only one as evidence
 _[_]✓ : ∀ {bounds} → Board KnownTile bounds → Coords bounds → Set
 _[_]✓ {bounds} grid coords with lookup coords grid
 ... | mine = ⊤
 ... | safe n = Σ[ neighboringMines ∈ Enumeration (mine Neighboring coords on grid) ] n ≡ length (Enumeration.list neighboringMines)
 
+-- a board is good if all positions on it are good
 _✓ : ∀ {bounds} → Board KnownTile bounds → Set
 _✓ {bounds} grid = ∀ coords → grid [ coords ]✓
 
+
 mine? : Decidable₁ (_≡_ mine)
 mine? mine     = yes refl
 mine? (safe _) = no  λ { () }