Skip to content

Commit

Permalink
more benchmark work
Browse files Browse the repository at this point in the history
  • Loading branch information
MicroProofs committed Jan 13, 2024
1 parent 271de33 commit 8bff441
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 161 deletions.
4 changes: 2 additions & 2 deletions examples/benchmarks/lib/benchmarks/knights.ak
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,11 @@ use benchmarks/queue.{
}

test run_knights0() {
run_knights(0, 0) == []
run_knights(100, 0) == []
}

test run_knights1() {
run_knights(2, 2) == []
run_knights(100, 2) == []
}

fn run_knights(depth: Int, board_size: Int) -> Solution {
Expand Down
82 changes: 12 additions & 70 deletions examples/benchmarks/lib/benchmarks/knights/chess_set.ak
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,18 @@ pub fn first_piece(board: ChessSet) -> Tile {
tile
}

// {-# INLINABLE lastPiece #-}
// lastPiece :: ChessSet -> Tile
// lastPiece (Board _ _ _ (t:_)) = t
// lastPiece _ = Tx.error ()

pub fn last_piece(board: ChessSet) -> Tile {
when board.visited is {
[] -> fail
[x, ..] -> x
}
}

pub fn delete_first(board: ChessSet) -> ChessSet {
let ChessSet { move_number, visited, .. } = board

Expand Down Expand Up @@ -64,71 +76,10 @@ pub fn is_square_free(board: ChessSet, tile: Tile) -> Bool {
pub fn not_in(tiles: List<a>, tile: a) -> Bool {
!list.has(tiles, tile)
}
// {-# INLINABLE createBoard #-}
// createBoard :: Integer -> Tile -> ChessSet
// createBoard x t = Board x 1 (Just t) [t]

// {-# INLINABLE sizeBoard #-}
// sizeBoard :: ChessSet -> Integer
// sizeBoard (Board s _ _ _) = s

// {-# INLINABLE noPieces #-}
// noPieces :: ChessSet -> Integer
// noPieces (Board _ n _ _) = n

// {-# INLINABLE addPiece #-}
// addPiece :: Tile -> ChessSet -> ChessSet
// addPiece t (Board s n f ts) = Board s (n+1) f (t:ts)

// -- % Remove the last element from a list
// {-# INLINABLE init #-}
// init :: [a] -> [a]
// init l = case reverse l of
// _:as -> reverse as
// [] -> Tx.error ()

// {-# INLINABLE secondLast #-}
// secondLast :: [a] -> Maybe a
// secondLast l =
// case reverse l of
// [] -> Tx.error ()
// [_] -> Nothing
// _:a:_ -> Just a

// {-% Note [deleteFirst].
// deleteFirst removes the first position from the tour.
// Since the sequence of positions (ts) is stored in reverse this involves
// deleting the last element of ts and also storing the second-last element of
// ts as the new starting position. In the strict world this will *fail* if the
// length of ts is 1. The lazy version got away with this because the starting
// position is never examined in that case (possibly just through luck: with
// enough backtracking that might still happen). To solve this we have to store
// the starting position as a Maybe value, deferring any error until we actually
// look at it.
// %-}

// {-# INLINABLE deleteFirst #-}
// deleteFirst :: ChessSet -> ChessSet
// deleteFirst (Board s n _ ts) =
// Board s (n-1) f' ts'
// where ts' = init ts
// f' = secondLast ts

// {-# INLINABLE positionPiece #-}
// positionPiece :: Integer -> ChessSet -> Tile
// positionPiece x (Board _ n _ ts) = ts Tx.!! (n - x)

// {-# INLINABLE lastPiece #-}
// lastPiece :: ChessSet -> Tile
// lastPiece (Board _ _ _ (t:_)) = t
// lastPiece _ = Tx.error ()

// {-# INLINABLE firstPiece #-}
// firstPiece :: ChessSet -> Tile
// firstPiece (Board _ _ f _) =
// case f of Just tile -> tile
// Nothing -> Tx.error ()

// {-# INLINABLE pieceAtTile #-}
// pieceAtTile :: Tile -> ChessSet -> Integer
// pieceAtTile x0 (Board _ _ _ ts)
Expand All @@ -139,15 +90,6 @@ pub fn not_in(tiles: List<a>, tile: a) -> Bool {
// | x == y = 1 + Tx.length xs
// | otherwise = findPiece x xs

// {-# INLINABLE notIn #-}
// notIn :: Eq a => a -> [a] -> Bool
// notIn _ [] = True
// notIn x (a:as) = (x /= a) && (notIn x as)

// {-# INLINABLE isSquareFree #-}
// isSquareFree :: Tile -> ChessSet -> Bool
// isSquareFree x (Board _ _ _ ts) = notIn x ts

// -- % Everything below here is only needed for printing boards.
// -- % This is useful for debugging.

Expand Down
101 changes: 12 additions & 89 deletions examples/benchmarks/lib/benchmarks/knights/heuristic.ak
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use aiken/builtin
use aiken/list
use benchmarks/knights/chess_set.{
add_piece, create_board, delete_first, first_piece, is_square_free,
add_piece, create_board, delete_first, first_piece, is_square_free, last_piece,
}
use benchmarks/knights/sort.{quick_sort}
use benchmarks/knights/types.{ChessSet, Tile}
Expand All @@ -17,6 +17,10 @@ type Direction {
RD
}

fn direction_list() {
[UL, UR, DL, DR, LU, LD, RU, RD]
}

fn move(direction: Direction, tile: Tile) -> Tile {
let (x, y) = tile

Expand Down Expand Up @@ -111,101 +115,20 @@ pub fn can_move_to(board: ChessSet, tile: Tile) -> Bool {
}
}

fn can_move(board: ChessSet, direction: Direction) -> Bool {
board |> can_move_to(move(direction, last_piece(board)))
}

pub fn all_descend(board: ChessSet) -> List<ChessSet> {
board
|> possible_moves
|> list.map(fn(direction) { move_knight(board, direction) })
}

fn move_knight(board: ChessSet, direction: Direction) -> ChessSet {
todo
add_piece(board, move(direction, last_piece(board)))
}

fn possible_moves(board: ChessSet) -> List<Direction> {
todo
}
// data Direction = UL | UR | DL |DR | LU | LD | RU | RD

// {-# INLINABLE move #-}
// move :: Direction -> Tile -> Tile
// move UL (x,y) = (x-1,y-2)
// move UR (x,y) = (x+1,y-2)
// move DL (x,y) = (x-1,y+2)
// move DR (x,y) = (x+1,y+2)
// move LU (x,y) = (x-2,y-1)
// move LD (x,y) = (x-2,y+1)
// move RU (x,y) = (x+2,y-1)
// move RD (x,y) = (x+2,y+1)

// {-# INLINABLE startTour #-}
// startTour :: Tile -> Integer -> ChessSet
// startTour st size
// | (size `Tx.remainder` 2) == 0 = createBoard size st
// | otherwise = {-Tx.trace "startTour" $ -} Tx.error ()

// {-# INLINABLE moveKnight #-}
// moveKnight :: ChessSet -> Direction -> ChessSet
// moveKnight board dir
// = addPiece (move dir (lastPiece board)) board

// {-# INLINABLE canMove #-}
// canMove :: ChessSet -> Direction -> Bool
// canMove board dir
// = canMoveTo (move dir (lastPiece board)) board

// {-# INLINABLE canMoveTo #-}
// canMoveTo :: Tile -> ChessSet -> Bool
// canMoveTo t@(x,y) board
// = (x Tx.>= 1) && (x Tx.<= sze) &&
// (y Tx.>= 1) && (y Tx.<= sze) &&
// isSquareFree t board
// where
// sze = sizeBoard board

// {-# INLINABLE descendents #-}
// descendents :: ChessSet -> [ChessSet]
// descendents board =
// if (canJumpFirst board) && (deadEnd (addPiece (firstPiece board) board))
// then []
// else
// let l = Tx.length singles in
// if l == 0 then map snd (quickSort (descAndNo board))
// else if l == 1 then singles
// else [] -- Going to be dead end
// where
// singles = singleDescend board

// {-# INLINABLE singleDescend #-}
// singleDescend :: ChessSet -> [ChessSet]
// singleDescend board =[x | (y,x) <- descAndNo board, y==1]

// {-# INLINABLE descAndNo #-}
// descAndNo :: ChessSet -> [(Integer,ChessSet)]
// descAndNo board
// = [(Tx.length (possibleMoves (deleteFirst x)),x) | x <- allDescend board]

// {-# INLINABLE allDescend #-}
// allDescend :: ChessSet -> [ChessSet]
// allDescend board
// = map (moveKnight board) (possibleMoves board)

// {-# INLINABLE possibleMoves #-}
// possibleMoves :: ChessSet -> [Direction]
// possibleMoves board
// =[x | x <- [UL,UR,DL,DR,LU,LD,RU,RD], (canMove board x)]

// {-# INLINABLE deadEnd #-}
// deadEnd :: ChessSet -> Bool
// deadEnd board = (Tx.length (possibleMoves board)) == 0

// {-# INLINABLE canJumpFirst #-}
// canJumpFirst :: ChessSet -> Bool
// canJumpFirst board
// = canMoveTo (firstPiece board) (deleteFirst board)

// {-# INLINABLE tourFinished #-}
// tourFinished :: ChessSet -> Bool
// tourFinished board
// = (noPieces board == (sze*sze)) && (canJumpFirst board)
// where
// sze = sizeBoard board
direction_list() |> list.filter(fn(direction) { can_move(board, direction) })
}

0 comments on commit 8bff441

Please sign in to comment.