list.dats

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)

list.sats

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

search.dats

#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 () }

search.sats

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