From dc62799ea1dd8d32f5c8a92fc1f71baf34750fe4 Mon Sep 17 00:00:00 2001 From: dianne Date: Fri, 28 Dec 2018 15:27:08 -0800 Subject: [PATCH] make the definition of Neighboring more generic this requires moving a few things around but it greatly simplifies further developments --- Minesweeper/Board.agda | 4 ++-- Minesweeper/Moves.agda | 12 ++---------- Minesweeper/Reasoning.agda | 6 +++--- Minesweeper/Rules.agda | 33 ++++++++++++++++++++++++--------- 4 files changed, 31 insertions(+), 24 deletions(-) diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda index 02fa982..f53832a 100644 --- a/Minesweeper/Board.agda +++ b/Minesweeper/Board.agda @@ -15,5 +15,5 @@ lookup (x , y) grid = Vec.lookup x (Vec.lookup y grid) _[_]≔_ : ∀ {A bounds} → Board A bounds → Coords bounds → A → Board A bounds grid [ (x , y) ]≔ value = grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ value) -_Neighboring_on_ : ∀ {A bounds} → A → Coords bounds → Board A bounds → Set -tile Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] tile ≡ lookup (proj₁ neighbor) grid +_Neighboring_on_ : ∀ {A bounds} → (A → Set) → Coords bounds → Board A bounds → Set +P Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] P (lookup (proj₁ neighbor) grid) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index a9f7b6a..2b4f11b 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -10,10 +10,6 @@ data Tile : Set where known : KnownTile → Tile unknown : Tile -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 @@ -23,17 +19,13 @@ data _↝▣_ : Tile → KnownTile → Set where _↝⊞_ : ∀ {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: 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′ → grid′ ✓ → - guess ↝⚐ lookup coords grid′ + guess ⚐✓ lookup coords grid′ -- solvable boards: a board is solvable when there is a rule-respecting way to fill its unfilled tiles record Solvable {bounds} (unsolved : Board Tile bounds) : Set where @@ -45,5 +37,5 @@ record Solvable {bounds} (unsolved : Board Tile bounds) : Set where -- "play" a valid move on a solvable board, giving evidence that it holds in the provided solution play : ∀ {bounds grid} (coords : Coords bounds) {guess} → grid [ coords ]↝✓ guess → (solved : Solvable grid) → - guess ↝⚐ lookup coords (Solvable.solution solved) + guess ⚐✓ lookup coords (Solvable.solution solved) play coords move solved = move (Solvable.solution solved) (Solvable.relevance solved) (Solvable.validity solved) diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda index 45a8386..a8d12a1 100644 --- a/Minesweeper/Reasoning.agda +++ b/Minesweeper/Reasoning.agda @@ -36,18 +36,18 @@ Many_neighboring★_on_excluding_ guess neighbor grid exclude = Neighbors★ gri data _[_]↝★_ {bounds} grid coords where -- known tiles already have a proven identity - known★ : ∀ tile guess → lookup coords grid ≡ known tile → guess ↝⚐ tile → grid [ coords ]↝★ guess + known★ : ∀ tile guess → lookup coords grid ≡ known tile → guess ⚐✓ tile → grid [ coords ]↝★ guess -- a tile is safe if an adjacent safe tile already has as many adjacent mines as it can safe★ : ∀ neighborMineCount - (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid) + (safeNeighbor : (known (safe neighborMineCount) ≡_) Neighboring coords on grid) (neighborMines : Many mine⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) → List.length (Neighbors★.list neighborMines) ≡ neighborMineCount → grid [ coords ]↝★ safe⚐ -- a tile is a mine if an adjacent safe tile already has as many adjacent safe tiles as it can mine★ : ∀ neighborMineCount - (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid) + (safeNeighbor : (known (safe neighborMineCount) ≡_) Neighboring coords on grid) (neighborSafes : Many safe⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) → List.length (Neighbors★.list neighborSafes) + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeNeighbor)))) → grid [ coords ]↝★ mine⚐ diff --git a/Minesweeper/Rules.agda b/Minesweeper/Rules.agda index 539c1f3..cd93171 100644 --- a/Minesweeper/Rules.agda +++ b/Minesweeper/Rules.agda @@ -7,8 +7,7 @@ open import Data.Product open import Data.Nat as ℕ using (ℕ) open import Data.List hiding (lookup) open import Relation.Binary.PropositionalEquality -open import Relation.Binary using () renaming (Decidable to Decidable₂) -open import Relation.Unary using () renaming (Decidable to Decidable₁) +open import Relation.Binary open import Relation.Nullary open import Minesweeper.Coords @@ -19,26 +18,42 @@ data KnownTile : Set where mine : KnownTile safe : ℕ → KnownTile +data Guess : Set where + mine⚐ : Guess + safe⚐ : Guess + +-- 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 + + -- 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) +... | 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 λ { () } +_⚐✓?_ : Decidable (_⚐✓_) +mine⚐ ⚐✓? mine = yes ⚐✓mine +mine⚐ ⚐✓? safe _ = no λ { () } +safe⚐ ⚐✓? mine = no λ { () } +safe⚐ ⚐✓? safe n = yes (⚐✓safe n) + +⚐✓-irrelevance : Irrelevant _⚐✓_ +⚐✓-irrelevance ⚐✓mine ⚐✓mine = refl +⚐✓-irrelevance (⚐✓safe n) (⚐✓safe .n) = refl -neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords bounds) → Enumeration (mine Neighboring coords on grid) -neighboringMines grid coords = Enum.filter ≡-irrelevance (λ { (neighbor , _) → mine? (lookup neighbor grid) }) (neighbors coords) +neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords bounds) → Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) +neighboringMines grid coords = Enum.filter ⚐✓-irrelevance (λ { (neighbor , _) → mine⚐ ⚐✓? (lookup neighbor grid) }) (neighbors coords) -_[_]✓? : ∀ {bounds} → Decidable₂ (_[_]✓ {bounds}) +_[_]✓? : ∀ {bounds} → Decidable (_[_]✓ {bounds}) _[_]✓? {bounds} grid coords with lookup coords grid ... | mine = yes tt ... | safe n with n ℕ.≟ length (Enumeration.list (neighboringMines grid coords))