From c62821e02a13691aeb03e7bfa77a9fe2f162c2d6 Mon Sep 17 00:00:00 2001 From: microproofs Date: Thu, 11 Jan 2024 14:44:51 -0500 Subject: [PATCH] continue porting over knights example --- .../lib/benchmarks/knights/chess_set.ak | 19 ++++- .../lib/benchmarks/knights/heuristic.ak | 81 +++++++++++++++++-- .../lib/benchmarks/knights/types.ak | 2 +- 3 files changed, 92 insertions(+), 10 deletions(-) diff --git a/examples/benchmarks/lib/benchmarks/knights/chess_set.ak b/examples/benchmarks/lib/benchmarks/knights/chess_set.ak index 4ff445e4..465758e7 100644 --- a/examples/benchmarks/lib/benchmarks/knights/chess_set.ak +++ b/examples/benchmarks/lib/benchmarks/knights/chess_set.ak @@ -26,14 +26,19 @@ pub fn first_piece(board: ChessSet) -> Tile { } pub fn delete_first(board: ChessSet) -> ChessSet { - let visited = board.visited + let ChessSet { move_number, visited, .. } = board expect Some(deleted_first) = list.init(visited) - ChessSet { ..board, start: second_last(visited), visited: deleted_first } + ChessSet { + ..board, + move_number: move_number - 1, + start: second_last(visited), + visited: deleted_first, + } } -pub fn second_last(visited: List) -> Option { +fn second_last(visited: List) -> Option { when visited is { [] -> None [_, ..rest] -> { @@ -51,6 +56,14 @@ pub fn second_last(visited: List) -> Option { } } } + +pub fn is_square_free(board: ChessSet, tile: Tile) -> Bool { + not_in(board.visited, tile) +} + +pub fn not_in(tiles: List, tile: a) -> Bool { + !list.has(tiles, tile) +} // {-# INLINABLE createBoard #-} // createBoard :: Integer -> Tile -> ChessSet // createBoard x t = Board x 1 (Just t) [t] diff --git a/examples/benchmarks/lib/benchmarks/knights/heuristic.ak b/examples/benchmarks/lib/benchmarks/knights/heuristic.ak index f736cd32..37d27f22 100644 --- a/examples/benchmarks/lib/benchmarks/knights/heuristic.ak +++ b/examples/benchmarks/lib/benchmarks/knights/heuristic.ak @@ -1,9 +1,37 @@ use aiken/builtin use aiken/list -use benchmarks/knights/chess_set.{add_piece, create_board, first_piece} +use benchmarks/knights/chess_set.{ + add_piece, create_board, delete_first, first_piece, is_square_free, +} use benchmarks/knights/sort.{quick_sort} use benchmarks/knights/types.{ChessSet, Tile} +type Direction { + UL + UR + DL + DR + LU + LD + RU + RD +} + +fn move(direction: Direction, tile: Tile) -> Tile { + let (x, y) = tile + + when direction is { + UL -> (x - 1, y - 2) + UR -> (x + 1, y - 2) + DL -> (x - 1, y + 2) + DR -> (x + 1, y + 2) + LU -> (x - 2, y - 1) + LD -> (x - 2, y + 1) + RU -> (x + 2, y - 1) + RD -> (x + 2, y + 1) + } +} + pub fn start_tour(st: Tile, size: Int) -> ChessSet { expect 0 = builtin.remainder_integer(size, 2) @@ -20,7 +48,8 @@ pub fn descendants(board: ChessSet) -> List { if and { can_jump_first(board), board - |> add_piece(first_piece(board)) + |> first_piece + |> add_piece(board, _) |> dead_end, } { [] @@ -37,22 +66,62 @@ pub fn descendants(board: ChessSet) -> List { } pub fn can_jump_first(board: ChessSet) -> Bool { - todo + can_move_to(delete_first(board), first_piece(board)) } pub fn dead_end(board: ChessSet) -> Bool { - todo + board |> possible_moves |> builtin.null_list } pub fn single_descend(board: ChessSet) -> List { - todo + let descendants_and_moves = desc_and_no(board) + list.filter_map( + descendants_and_moves, + fn(item) { + let (moves, board) = item + if moves == 1 { + Some(board) + } else { + None + } + }, + ) } pub fn desc_and_no(board: ChessSet) -> List<(Int, ChessSet)> { - todo + board + |> all_descend + |> list.map( + fn(item) { + (item |> delete_first |> possible_moves |> list.length, item) + }, + ) } pub fn can_move_to(board: ChessSet, tile: Tile) -> Bool { + let (x, y) = tile + let size = board.size + + and { + x >= 1, + x <= size, + y >= 1, + y <= size, + is_square_free(board, tile), + } +} + +pub fn all_descend(board: ChessSet) -> List { + board + |> possible_moves + |> list.map(fn(direction) { move_knight(board, direction) }) +} + +fn move_knight(board: ChessSet, direction: Direction) -> ChessSet { + todo +} + +fn possible_moves(board: ChessSet) -> List { todo } // data Direction = UL | UR | DL |DR | LU | LD | RU | RD diff --git a/examples/benchmarks/lib/benchmarks/knights/types.ak b/examples/benchmarks/lib/benchmarks/knights/types.ak index 75449ffb..fc293456 100644 --- a/examples/benchmarks/lib/benchmarks/knights/types.ak +++ b/examples/benchmarks/lib/benchmarks/knights/types.ak @@ -2,9 +2,9 @@ pub type Tile = (Int, Int) pub type ChessSet { + size: Int, move_number: Int, visited: List, - size: Int, start: Option, }