Create a gist now

Instantly share code, notes, and snippets.

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

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