Skip to content

Instantly share code, notes, and snippets.

@steinwaywhw steinwaywhw/list.dats Secret
Last active Aug 29, 2015

Embed
What would you like to do?
staload "list.sats"
#define ATS_DYNLOADFLAG 0
implement {a} {b} map (xs, f) =
case+ xs of
| Nil () => Nil ()
| Cons (x, xs) => Cons (f (x), map (xs, f))
implement {a} filter (xs, f) =
case+ xs of
| Nil () => Nil ()
| Cons (x, xs) =>
if f(x)
then Cons (x, filter (xs, f))
else filter (xs, f)
implement {a} length (xs) =
case+ xs of
| Nil () => 0
| Cons (_, xs) => 1 + length (xs)
implement {a} min (xs, f, base) =
case+ xs of
| Nil () => base
| Cons (x, xs) =>
if f(x, min (xs, f, base)) > 0
then min (xs, f, base)
else x
implement {a} max (xs, f, base) =
case+ xs of
| Nil () => base
| Cons (x, xs) =>
if f(x, max (xs, f, base)) > 0
then x
else max (xs, f, base)
datatype list (a:t@ype) =
| Cons of (a, list (a))
| Nil of ()
fun {a:t@ype} {b:t@ype} map (list (a), (a) -<cloref1> b): list (b)
fun {a:t@ype} filter (list (a), (a) -<cloref1> bool): list (a)
fun {a:t@ype} length (list (a)): int
fun {a:t@ype} min (list (a), (a, a) -<cloref1> int, a): a
fun {a:t@ype} max (list (a), (a, a) -<cloref1> int, a): a
#include "share/atspre_staload.hats"
staload "list.sats"
staload "search.sats"
staload _ = "list.dats"
staload "libc/SATS/random.sats"
implement eq_pos_pos (p1, p2) = let
val @(x1, y1) = p1
val @(x2, y2) = p2
in
x1 = x2 && y1 = y2
end
implement neq_pos_pos (p1, p2) =
if p1 = p2 then false else true
implement eq_cell_cell (c1, c2) =
if is_empty (c1) && is_empty (c2)
then true
else case+ c1 of
| X _ => (case+ c2 of
| X _ => true
| _ => false)
| O _ => (case+ c2 of
| O _ => true
| _ => false)
| _ => false
implement is_empty (c) =
case+ c of
| E () => true
| _ => false
implement is_full (b) =
length (
filter<move> (b, lam (m) =<cloref1> ret where {
val @(_, cell) = m
val ret = is_empty (cell)
})
) = 0
implement show_board (b) = () where {
val _ = map<move><move> (b, lam (m) =<cloref1> let
val @(pos, cell) = m
val @(x, y) = pos
val () = show (cell)
val () = if y = 3 then print_newline ()
in
m
end)
}
implement show_cell (c) = case+ c of
| E () => print "_ "
| X () => print "X "
| O () => print "O "
implement make_move (b, mv) =
map<move><move> (b, lam (m) =<cloref1> ret where {
val @(pb, cb) = m
val @(pm, cm) = mv
val ret =
if pb = pm && is_empty (cb)
then mv
else m
})
implement next_moves (b, c) =
filter<board> (
map<move><board> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val ret =
if is_empty (cell)
then make_move (b, @(pos, c))
else Nil ()
}),
lam (bd) =<cloref1> case+ bd of
| Nil () => false
| _ => true
)
implement is_win (b, c) = let
fun check_col (col: int): bool = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(_, y) = pos
val ret = if y = col && cell = c then true else false
})
in
length (xs) = 3
end
fun check_row (row: int): bool = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, _) = pos
val ret = if x = row && cell = c then true else false
})
in
length (xs) = 3
end
fun check_diag (): bool = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, y) = pos
val ret = if x = y && cell = c then true else false
})
val ys = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, y) = pos
val ret = if x + y = 4 && cell = c then true else false
})
in
length (xs) = 3 || length (ys) = 3
end
fun loop_col (col: int): bool =
if col = 0
then false
else
if check_col (col)
then true
else loop_col (col - 1)
fun loop_row (row: int): bool =
if row = 0
then false
else
if check_row (row)
then true
else loop_row (row - 1)
in
check_diag () || loop_row (3) || loop_col (3)
end
implement eval (b, c) = let
fun eval_col (col: int): int = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(_, y) = pos
val ret = if y = col && (cell = c || is_empty (c)) then true else false
})
in
length (xs)
end
fun eval_row (row: int): int = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, _) = pos
val ret = if x = row && (cell = c || is_empty (c)) then true else false
})
in
length (xs)
end
fun eval_diag (): int = let
val xs = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, y) = pos
val ret = if x = y && (cell = c || is_empty (c)) then true else false
})
val ys = filter<move> (b, lam (m) =<cloref1> ret where {
val @(pos, cell) = m
val @(x, y) = pos
val ret = if x + y = 4 && (cell = c || is_empty (c)) then true else false
})
in
length (xs) + length (ys)
end
fun loop_col (col: int): int =
if col = 0
then 0
else eval_col (col) + loop_col (col - 1)
fun loop_row (row: int): int =
if row = 0
then 0
else eval_row (row) + loop_row (row - 1)
in if is_win (b, c)
then 1000
else if is_win (b, other(c))
then ~1000
else eval_diag () + loop_row (3) + loop_col (3)
end
implement other (c) = case+ c of
| X () => O ()
| O () => X ()
| E () => E ()
implement minimax_max (b, c, depth) =
if depth = 0 || is_full (b)
then T (b, Nil (), eval (b, c))
else let
val moves = next_moves (b, c)
val trees = map<board><dtree>
(moves, lam (b) =<cloref1> minimax_min (b, other (c), depth - 1))
val T (_, _, best) = max (trees, lam (t1, t2) =<cloref1> let
val T (_, _, v1) = t1
val T (_, _, v2) = t2
val v = v1 - v2
in
if v = 0 then ~(randint(1)) + randint(1) else v
end, T(Nil(), Nil(), ~10000))
in
T (b, trees, best)
end
implement minimax_min (b, c, depth) =
if depth = 0 || is_full (b)
then T (b, Nil (), eval (b, c))
else let
val moves = next_moves (b, c)
val trees = map<board><dtree>
(moves, lam (b) =<cloref1> minimax_max (b, other (c), depth - 1))
val T (_, _, best) = min (trees, lam (t1, t2) =<cloref1> let
val T (_, _, v1) = t1
val T (_, _, v2) = t2
val v = v1 - v2
in
if v = 0 then ~(randint(1)) + randint(1) else v
end, T(Nil(), Nil(), 10000))
in
T (b, trees, best)
end
implement best_move (b, c) = let
val T(_, moves, v) = minimax_max (b, c, 4)
val b = filter<dtree> (moves, lam (t) =<cloref1> let
val T(_, _, tv) = t
in
tv = v
end)
val- Cons (b, _) = b
val- T(b, _, _) = b
in
b
end
#define :: Cons
implement run () = () where {
val e = E ()
val b =
@(@(1, 1), e) :: @(@(1, 2), e) :: @(@(1, 3), e) ::
@(@(2, 1), e) :: @(@(2, 2), e) :: @(@(2, 3), e) ::
@(@(3, 1), e) :: @(@(3, 2), e) :: @(@(3, 3), e) :: Nil ()
fun loop (b: board, c: cell): void =
if is_win (b, c) || is_win (b, other (c)) || is_full (b) then ()
else let
val b = best_move (b, c)
val () = show (b)
val () = print_newline ()
in
loop (b, other (c))
end
fun test (b: board, c: cell): void = () where {
val b = make_move (b, @(@(1, 2), c))
val _ = show (b)
}
val () = loop (b, X ())
//val () = test (b, X ())
}
implement main0 () = () where { val _ = run () }
staload "list.sats"
datatype cell =
| E of ()
| X of ()
| O of ()
typedef position = @(int, int)
typedef move = @(position, cell)
typedef board = list (move)
datatype dtree =
| T of (board, list (dtree), int)
fun neq_pos_pos (position, position): bool
fun eq_pos_pos (position, position): bool
fun eq_cell_cell (cell, cell): bool
fun is_empty (cell): bool
fun is_full (board): bool
fun other (cell): cell
fun make_move (board, move): board
fun next_moves (board, cell): list (board)
fun show_board (board): void
fun show_cell (cell): void
symintr show
overload show with show_board
overload show with show_cell
overload = with eq_pos_pos
overload = with eq_cell_cell
overload != with neq_pos_pos
fun is_win (board, cell): bool
fun eval (board, cell): int
fun minimax_max (board, cell, int): dtree
fun minimax_min (board, cell, int): dtree
fun best_move (board, cell): board
fun run (): void
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.