commit new example for benchmarking

This commit is contained in:
microproofs 2024-01-10 19:27:21 -05:00 committed by KtorZ
parent fe7d744946
commit 8f825f68b1
No known key found for this signature in database
GPG Key ID: 33173CB6F77F4277
14 changed files with 567 additions and 2 deletions

View File

@ -0,0 +1,20 @@
name: Tests
on:
push:
branches: ["main"]
pull_request:
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: aiken-lang/setup-aiken@v0.1.0
with:
version: v1
- run: aiken fmt --check
- run: aiken check -D
- run: aiken build

6
examples/benchmarks/.gitignore vendored Normal file
View File

@ -0,0 +1,6 @@
# Aiken compilation artifacts
artifacts/
# Aiken's project working directory
build/
# Aiken's default documentation export
docs/

View File

@ -0,0 +1,55 @@
# benchmarks
Write validators in the `validators` folder, and supporting functions in the `lib` folder using `.ak` as a file extension.
For example, as `validators/always_true.ak`
```gleam
validator {
fn spend(_datum: Data, _redeemer: Data, _context: Data) -> Bool {
True
}
}
```
## Building
```sh
aiken build
```
## Testing
You can write tests in any module using the `test` keyword. For example:
```gleam
test foo() {
1 + 1 == 2
}
```
To run all tests, simply do:
```sh
aiken check
```
To run only tests matching the string `foo`, do:
```sh
aiken check -m foo
```
## Documentation
If you're writing a library, you might want to generate an HTML documentation for it.
Use:
```sh
aiken docs
```
## Resources
Find more on the [Aiken's user manual](https://aiken-lang.org).

View File

@ -0,0 +1,15 @@
# This file was generated by Aiken
# You typically do not need to edit this file
[[requirements]]
name = "aiken-lang/stdlib"
version = "1.7.0"
source = "github"
[[packages]]
name = "aiken-lang/stdlib"
version = "1.7.0"
requirements = []
source = "github"
[etags]

View File

@ -0,0 +1,14 @@
name = "aiken/benchmarks"
version = "0.0.0"
license = "Apache-2.0"
description = "Aiken contracts for project 'aiken/benchmarks'"
[repository]
user = "aiken"
project = "benchmarks"
platform = "github"
[[dependencies]]
name = "aiken-lang/stdlib"
version = "1.7.0"
source = "github"

View File

@ -0,0 +1,71 @@
use aiken/list
use benchmarks/knights/heuristic.{descendants, finished_tour, start_tour}
use benchmarks/knights/types.{ChessSet, Solution}
use benchmarks/queue.{
Queue, append_all_front, append_front, create_queue, head, is_empty,
remove_front, to_list,
}
test run_knights0() {
run_knights(0, 0) == []
}
test run_knights1() {
run_knights(2, 2) == []
}
fn run_knights(depth: Int, board_size: Int) -> Solution {
depth_search(depth, root(board_size), grow, is_fin) |> to_list
}
fn depth_search(
depth: Int,
queue: Queue<a>,
grow_fn: fn(a) -> List<a>,
fin_fn: fn(a) -> Bool,
) -> Queue<a> {
if depth == 0 || is_empty(queue) {
create_queue()
} else if fin_fn(head(queue)) {
depth_search(depth - 1, remove_front(queue), grow_fn, fin_fn)
|> append_front(head(queue))
} else {
append_all_front(remove_front(queue), grow_fn(head(queue)))
|> depth_search(depth - 1, _, grow_fn, fin_fn)
}
}
fn root(sze: Int) -> Queue<(Int, ChessSet)> {
append_all_front(create_queue(), mk_starts(sze))
}
fn mk_starts(sze: Int) -> List<(Int, ChessSet)> {
let x_list = interval(1, sze)
let y_list = interval(1, sze)
let l = x_list |> list.map2(y_list, fn(a, b) { start_tour((a, b), sze) })
let length = list.length(l)
list.repeat(1 - length, length) |> list.zip(l)
}
fn interval(a: Int, b: Int) -> List<Int> {
if a > b {
[]
} else {
[a, ..interval(a + 1, b)]
}
}
fn grow(item: (Int, ChessSet)) -> List<(Int, ChessSet)> {
let (x, y) = item
let const_item = x + 1
descendants(y) |> list.map(fn(list_item) { (const_item, list_item) })
}
fn is_fin(item: (Int, ChessSet)) -> Bool {
let (_, y) = item
finished_tour(y)
}

View File

@ -0,0 +1,172 @@
use aiken/builtin
use aiken/list
use benchmarks/knights/types.{ChessSet, Tile}
pub fn create_board(size: Int, init_square: Tile) -> ChessSet {
ChessSet {
size,
move_number: 1,
start: Some(init_square),
visited: [init_square],
}
}
pub fn add_piece(board: ChessSet, tile: Tile) -> ChessSet {
// record update
ChessSet {
..board,
move_number: board.move_number + 1,
visited: [tile, ..board.visited],
}
}
pub fn first_piece(board: ChessSet) -> Tile {
expect Some(tile) = board.start
tile
}
pub fn delete_first(board: ChessSet) -> ChessSet {
let visited = board.visited
expect Some(deleted_first) = list.init(visited)
ChessSet { ..board, start: second_last(visited), visited: deleted_first }
}
pub fn second_last(visited: List<a>) -> Option<a> {
when visited is {
[] -> None
[_, ..rest] -> {
let value = second_last(rest)
if value == None {
if builtin.null_list(rest) {
None
} else {
Some(builtin.head_list(visited))
}
} else {
value
}
}
}
}
// {-# 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)
// = findPiece x0 ts
// where
// findPiece _ [] = Tx.error ()
// findPiece x (y:xs)
// | 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.
// instance Haskell.Show ChessSet where
// showsPrec _ (Board sze n _ ts)
// = Haskell.showString (printBoard sze sortedTrail 1)
// where sortedTrail = quickSort (assignMoveNo ts sze n)
// assignMoveNo :: [Tile] -> Integer -> Integer -> [Tile]
// assignMoveNo [] _ _
// = []
// assignMoveNo ((x,y):t) size z
// = (((y-1)*size)+x,z):assignMoveNo t size (z-1)
// printBoard :: Integer -> [Tile] -> Integer -> Haskell.String
// printBoard s [] n
// | (n > (s*s)) = ""
// | ((n `Haskell.mod` s) /=0)= "*"++(spaces (s*s) 1) ++(printBoard s [] (n+1))
// | ((n `Haskell.mod` s) ==0)= "*\n" ++(printBoard s [] (n+1))
// printBoard s trail@((i,j):xs) n
// | (i==n) &&
// ((n `Haskell.mod` s) ==0) = (Haskell.show j)++"\n"++(printBoard s xs (n+1))
// | (i==n) &&
// ((n `Haskell.mod` s) /=0)= (Haskell.show j)++(spaces (s*s) j)++(printBoard s xs (n+1))
// | ((n `Haskell.mod` s) /=0)= "*" ++(spaces (s*s) 1)++(printBoard s trail (n+1))
// | ((n `Haskell.mod` s) ==0)= "*\n" ++(printBoard s trail (n+1))
// printBoard _ _ _ = "?"
// spaces :: Integer -> Integer -> Haskell.String
// spaces s y =
// take' ((logTen s) - (logTen y) + 1) [' ',' '..]
// where
// logTen :: Integer -> Integer
// logTen 0 = 0
// logTen x = 1 + logTen (x `Haskell.div` 10)

View File

@ -0,0 +1,142 @@
use aiken/builtin
use aiken/list
use benchmarks/knights/chess_set.{add_piece, create_board, first_piece}
use benchmarks/knights/sort.{quick_sort}
use benchmarks/knights/types.{ChessSet, Tile}
pub fn start_tour(st: Tile, size: Int) -> ChessSet {
expect 0 = builtin.remainder_integer(size, 2)
create_board(size, st)
}
pub fn finished_tour(board: ChessSet) -> Bool {
let ChessSet { move_number, size, .. } = board
move_number == size * size && can_jump_first(board)
}
pub fn descendants(board: ChessSet) -> List<ChessSet> {
if and {
can_jump_first(board),
board
|> add_piece(first_piece(board))
|> dead_end,
} {
[]
} else {
let singles = single_descend(board)
when singles is {
[] -> board |> desc_and_no |> quick_sort |> list.map(builtin.snd_pair)
[_] -> singles
_ ->
[]
}
}
}
pub fn can_jump_first(board: ChessSet) -> Bool {
todo
}
pub fn dead_end(board: ChessSet) -> Bool {
todo
}
pub fn single_descend(board: ChessSet) -> List<ChessSet> {
todo
}
pub fn desc_and_no(board: ChessSet) -> List<(Int, ChessSet)> {
todo
}
pub fn can_move_to(board: ChessSet, tile: Tile) -> Bool {
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

View File

@ -0,0 +1,3 @@
pub fn quick_sort(l: List<a>) -> List<a> {
todo
}

View File

@ -0,0 +1,12 @@
pub type Tile =
(Int, Int)
pub type ChessSet {
move_number: Int,
visited: List<Tile>,
size: Int,
start: Option<Tile>,
}
pub type Solution =
List<(Int, ChessSet)>

View File

@ -0,0 +1,41 @@
use aiken/list
pub opaque type Queue<a> {
inner: List<a>,
}
pub fn create_queue() -> Queue<a> {
[] |> Queue
}
pub fn to_list(queue: Queue<a>) -> List<a> {
queue.inner
}
pub fn is_empty(queue: Queue<a>) -> Bool {
when queue.inner is {
[] -> True
_ -> False
}
}
pub fn append_front(queue: Queue<a>, item: a) -> Queue<a> {
list.push(queue.inner, item) |> Queue
}
/// Add all items from the list to the front of the queue
pub fn append_all_front(queue: Queue<a>, items: List<a>) -> Queue<a> {
list.concat(items, queue.inner) |> Queue
}
pub fn remove_front(queue: Queue<a>) -> Queue<a> {
expect [_, ..rest] = queue.inner
rest |> Queue
}
pub fn head(queue: Queue<a>) -> a {
expect [q, ..] = queue.inner
q
}

View File

@ -0,0 +1,14 @@
{
"preamble": {
"title": "aiken/benchmarks",
"description": "Aiken contracts for project 'aiken/benchmarks'",
"version": "0.0.0",
"plutusVersion": "v2",
"compiler": {
"name": "Aiken",
"version": "v1.0.21-alpha+4b04517"
},
"license": "Apache-2.0"
},
"validators": []
}

View File

@ -5,5 +5,5 @@ description = "Aiken contracts for project 'aiken-lang/hello_world'"
[[dependencies]]
name = "aiken-lang/stdlib"
version = "main"
version = "1.7.0"
source = "github"

View File

@ -6,7 +6,7 @@
"plutusVersion": "v2",
"compiler": {
"name": "Aiken",
"version": "v1.0.19-alpha+d56d518"
"version": "v1.0.21-alpha+4b04517"
}
},
"validators": [