Created
August 30, 2013 14:53
-
-
Save vituscze/6390701 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module TicTacToe where | |
open import Data.Bool | |
using (Bool; true; false; _∧_; _∨_) | |
open import Data.Empty | |
using (⊥-elim) | |
open import Data.Fin | |
using (Fin; zero; suc) | |
open import Data.Maybe | |
using (Maybe; just; nothing) | |
open import Data.Nat | |
using (ℕ; zero; suc; _<_; z≤n; s≤s) | |
open import Data.Product | |
using (Σ; Σ-syntax; ∃; _×_; _,_; ,_; map) | |
open import Relation.Binary.PropositionalEquality | |
using (_≢_; inspect; [_]) | |
data Player : Set where | |
x o : Player | |
infixl 1 _!_ | |
infix 3 _≟_ | |
infixr 4 _∷_ -∷_ | |
data SquareVec : (len : ℕ) (empty : ℕ) → Set where | |
[] : SquareVec 0 0 | |
-∷_ : ∀ {l e} → SquareVec l e → SquareVec (suc l) (suc e) | |
_∷_ : ∀ {l e} (p : Player) → SquareVec l e → SquareVec (suc l) e | |
move : ∀ {l e} → Player → SquareVec l (suc e) → Fin (suc e) → SquareVec l e | |
move p ( -∷ sqv) zero = p ∷ sqv | |
move {e = zero} p ( -∷ _ ) (suc ()) | |
move {e = suc e} p ( -∷ sqv) (suc fe) = -∷ move p sqv fe | |
move p (p′ ∷ sqv) fe = p′ ∷ move p sqv fe | |
empty : ∀ {n} → SquareVec n n | |
empty {zero} = [] | |
empty {suc _} = -∷ empty | |
data Game : ∀ {e} → SquareVec 9 e → Set where | |
start : Game empty | |
move-p : ∀ {e} {gs} p (fe : Fin (suc e)) → Game gs → Game (move p gs fe) | |
data Result : Set where | |
win : Player → Result | |
draw : Result | |
data State : Set where | |
ended : Result → State | |
going : State | |
_≟_ : (p₁ p₂ : Player) → Bool | |
x ≟ x = true | |
x ≟ o = false | |
o ≟ x = false | |
o ≟ o = true | |
_!_ : ∀ {n e} → SquareVec n e → ℕ → Maybe Player | |
[] ! n = nothing | |
-∷ _ ! zero = nothing | |
-∷ xs ! suc n = xs ! n | |
p ∷ _ ! zero = just p | |
_ ∷ xs ! suc n = xs ! n | |
check3 : ∀ {e} → Player → SquareVec 9 e → (a b c : ℕ) → Bool | |
check3 p sqv a b c = check (sqv ! a) ∧ check (sqv ! b) ∧ check (sqv ! c) | |
where | |
check : Maybe Player → Bool | |
check (just p′) = p ≟ p′ | |
check nothing = false | |
win? : ∀ {e} → Player → SquareVec 9 e → Bool | |
win? p sqv = | |
check 0 1 2 ∨ check 3 4 5 ∨ check 6 7 8 ∨ | |
check 0 3 6 ∨ check 1 4 7 ∨ check 2 5 8 ∨ | |
check 0 4 8 ∨ check 2 4 6 | |
where | |
check = check3 p sqv | |
result : ∀ {e} → SquareVec 9 e → Result | |
result sqv with win? x sqv | |
... | true = win x | |
... | false with win? o sqv | |
... | true = win o | |
... | false = draw | |
gameState : ∀ {e} {gs : SquareVec 9 e} → Game gs → State | |
gameState {zero} {gs} _ = ended (result gs) | |
gameState {suc e} {gs} _ with result gs | |
gameState {suc e} _ | win p = ended (win p) | |
gameState {suc e} _ | draw = going | |
game-ended : {gs : SquareVec 9 0} (g : Game gs) → gameState g ≢ going | |
game-ended _ () | |
AI : Set | |
AI = ∀ {e} {sqv : SquareVec 9 (suc e)} → Game sqv → Fin (suc e) | |
∃Game : Set | |
∃Game = ∃ λ e → Σ (SquareVec 9 e) Game | |
gameMaster : ∀ {e} {sqv : SquareVec 9 e} (sp : Player) | |
(x-move o-move : AI) → Game sqv → Result × ∃Game | |
gameMaster sp xAI oAI g with gameState g | inspect gameState g | |
... | ended s | _ = s , , , g | |
gameMaster {zero} sp xAI oAI g | going | [ eq ] = ⊥-elim (game-ended g eq) | |
gameMaster {suc e} x xAI oAI g | going | _ = gameMaster o xAI oAI (move-p x (xAI g) g) | |
gameMaster {suc e} o xAI oAI g | going | _ = gameMaster x xAI oAI (move-p o (oAI g) g) | |
player-lowest : AI | |
player-lowest _ = zero | |
max : ∀ {e} → Fin (suc e) | |
max {zero} = zero | |
max {suc e} = suc max | |
player-highest : AI | |
player-highest _ = max |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment