Last active
February 20, 2021 17:26
-
-
Save Feni/d819f120a7d179bc472c94df9471e600 to your computer and use it in GitHub Desktop.
Knight's tour example
This file contains 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
// Knight's tour: Find the sequence of moves of a knight on a chessboard such that the knight visits every square exactly once. | |
// A move is an array of 2 numbers indicating how many [rows, columns] a piece travels. | |
type Move: [Integer, 2] | |
// <static type> identifier : (<dependent types>) = <value> | |
let knightMoves: [Move] = [[2, 1], [1, 2], [-1, 2], [-2, 1], [-2, -1], [-1, -2], [1, -2], [2, -1]] | |
// A Position is a 2 element array indicating [row, column] index (in range 0 to 8) on the board. | |
type Position: [Integer 0...8, 2] | |
// Check whether a move from start to end is a valid knight's move. start-end does elementwise subtraction. | |
fn isKnightMove(start: Position, end: Position) Boolean : start - end in knightMoves // start-end does an elementwise subtraction | |
fn knightsMoves(positions: [Position]) Boolean : all(map(isKnightMove, pairwise(positions))) | |
fn distinctMoves(positions: [Position]) Boolean : set(positions).length == positions.length | |
type Tour: [Position] knightsMoves distinctMoves | |
// Now that we know how to check whether a tour is valid, we can ask the runtime to generate a valid tour starting from 0, 0 | |
// The types encode the logic and relationship between elements and are enumerable. | |
let tour: Tour = [[0, 0], ...] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment