440 lines
5.7 KiB
Text
440 lines
5.7 KiB
Text
(* ****** ****** *)
|
|
//
|
|
#include
|
|
"share/atspre_staload.hats"
|
|
#include
|
|
"share/HATS/atspre_staload_libats_ML.hats"
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
abst@ype
|
|
pip_type = int
|
|
abst@ype
|
|
suit_type = int
|
|
//
|
|
abst@ype
|
|
card_type = int
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
typedef pip = pip_type
|
|
typedef suit = suit_type
|
|
|
|
(* ****** ****** *)
|
|
|
|
typedef card = card_type
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
pip_make: natLt(13) -> pip
|
|
extern
|
|
fun
|
|
pip_get_name: pip -> string
|
|
extern
|
|
fun
|
|
pip_get_value: pip -> intBtwe(1, 13)
|
|
//
|
|
extern
|
|
fun
|
|
suit_make: natLt(4) -> suit
|
|
extern
|
|
fun
|
|
suit_get_name: suit -> string
|
|
extern
|
|
fun
|
|
suit_get_value: suit -> intBtwe(1, 4)
|
|
//
|
|
overload .name with pip_get_name
|
|
overload .name with suit_get_name
|
|
overload .value with pip_get_value
|
|
overload .value with suit_get_value
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
(*
|
|
| Two | Three | Four | Five
|
|
| Six | Seven | Eight | Nine
|
|
| Ten | Jack | Queen | King | Ace
|
|
*)
|
|
//
|
|
(*
|
|
| Spade | Heart | Diamond | Club
|
|
*)
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
local
|
|
|
|
assume
|
|
pip_type = natLt(13)
|
|
|
|
in (* in-of-local *)
|
|
|
|
implement
|
|
pip_make(x) = x
|
|
implement
|
|
pip_get_value(x) = x + 1
|
|
|
|
end // end of [local]
|
|
|
|
(* ****** ****** *)
|
|
|
|
local
|
|
|
|
assume
|
|
suit_type = natLt(4)
|
|
|
|
in (* in-of-local *)
|
|
|
|
implement
|
|
suit_make(x) = x
|
|
implement
|
|
suit_get_value(x) = x + 1
|
|
|
|
end // end of [local]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
pip_get_name
|
|
(x) =
|
|
(
|
|
case+
|
|
x.value()
|
|
of // case+
|
|
| 1 => "Ace"
|
|
| 2 => "Two"
|
|
| 3 => "Three"
|
|
| 4 => "Four"
|
|
| 5 => "Five"
|
|
| 6 => "Six"
|
|
| 7 => "Seven"
|
|
| 8 => "Eight"
|
|
| 9 => "Nine"
|
|
| 10 => "Ten"
|
|
| 11 => "Jack"
|
|
| 12 => "Queen"
|
|
| 13 => "King"
|
|
)
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
implement
|
|
suit_get_name
|
|
(x) =
|
|
(
|
|
case+
|
|
x.value()
|
|
of // case+
|
|
| 1 => "S" | 2 => "H" | 3 => "D" | 4 => "C"
|
|
) (* end of [suit_get_name] *)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
card_get_pip: card -> pip
|
|
extern
|
|
fun
|
|
card_get_suit: card -> suit
|
|
//
|
|
extern
|
|
fun
|
|
card_make: natLt(52) -> card
|
|
extern
|
|
fun
|
|
card_make_suit_pip: (suit, pip) -> card
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
extern
|
|
fun
|
|
fprint_pip : fprint_type(pip)
|
|
extern
|
|
fun
|
|
fprint_suit : fprint_type(suit)
|
|
extern
|
|
fun
|
|
fprint_card : fprint_type(card)
|
|
|
|
(* ****** ****** *)
|
|
|
|
overload .pip with card_get_pip
|
|
overload .suit with card_get_suit
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
fprint_val<card> = fprint_card
|
|
|
|
(* ****** ****** *)
|
|
|
|
overload fprint with fprint_pip
|
|
overload fprint with fprint_suit
|
|
overload fprint with fprint_card
|
|
|
|
(* ****** ****** *)
|
|
|
|
local
|
|
|
|
assume
|
|
card_type = natLt(52)
|
|
|
|
in (* in-of-local *)
|
|
//
|
|
implement
|
|
card_get_pip
|
|
(x) = pip_make(nmod(x, 13))
|
|
implement
|
|
card_get_suit
|
|
(x) = suit_make(ndiv(x, 13))
|
|
//
|
|
implement
|
|
card_make(xy) = xy
|
|
//
|
|
implement
|
|
card_make_suit_pip(x, y) =
|
|
(x.value()-1) * 13 + (y.value()-1)
|
|
//
|
|
end // end of [local]
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
implement
|
|
fprint_pip(out, x) =
|
|
fprint!(out, x.name())
|
|
implement
|
|
fprint_suit(out, x) =
|
|
fprint!(out, x.name())
|
|
//
|
|
implement
|
|
fprint_card(out, c) =
|
|
fprint!(out, c.suit(), "(", c.pip(), ")")
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
absvtype
|
|
deck_vtype(n:int) = ptr
|
|
//
|
|
vtypedef deck(n:int) = deck_vtype(n)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
deck_get_size
|
|
{n:nat}(!deck(n)): int(n)
|
|
//
|
|
extern
|
|
fun
|
|
deck_is_empty
|
|
{n:nat}(!deck(n)): bool(n==0)
|
|
//
|
|
overload iseqz with deck_is_empty
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
deck_free{n:int}(deck(n)): void
|
|
//
|
|
overload .free with deck_free
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
deck_make_full((*void*)): deck(52)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
fprint_deck
|
|
{n:nat}(FILEref, !deck(n)): void
|
|
//
|
|
overload fprint with fprint_deck
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
deck_shuffle
|
|
{n:nat}(!deck(n) >> _): void
|
|
//
|
|
overload .shuffle with deck_shuffle
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun
|
|
deck_takeout_top
|
|
{n:pos}(!deck(n) >> deck(n-1)): card
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
local
|
|
//
|
|
datavtype
|
|
deck(int) =
|
|
| {n:nat}
|
|
Deck(n) of
|
|
(
|
|
int(n)
|
|
, list_vt(card, n)
|
|
) // end of [Deck]
|
|
//
|
|
assume
|
|
deck_vtype(n:int) = deck(n)
|
|
//
|
|
in (* in-of-local *)
|
|
|
|
implement
|
|
deck_get_size
|
|
(deck) =
|
|
(
|
|
let val+Deck(n, _) = deck in n end
|
|
)
|
|
|
|
implement
|
|
deck_is_empty
|
|
(deck) =
|
|
(
|
|
let val+Deck(n, _) = deck in n = 0 end
|
|
)
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
implement
|
|
deck_free(deck) =
|
|
(
|
|
let val+~Deck(n, xs) = deck in free(xs) end
|
|
) (* end of [deck_free] *)
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
deck_make_full
|
|
((*void*)) = let
|
|
//
|
|
val xys =
|
|
list_make_intrange(0, 52)
|
|
//
|
|
val cards =
|
|
list_vt_mapfree_fun<natLt(52)><card>(xys, lam xy => card_make(xy))
|
|
//
|
|
in
|
|
Deck(52, cards)
|
|
end // end of [deck_make_full]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
fprint_deck
|
|
(out, deck) = let
|
|
//
|
|
val+Deck(n, xs) = deck
|
|
//
|
|
in
|
|
//
|
|
fprint_list_vt(out, xs)
|
|
//
|
|
end // end of [fprint_deck]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
deck_shuffle
|
|
(deck) =
|
|
fold@(deck) where
|
|
{
|
|
//
|
|
val+@Deck(n, xs) = deck
|
|
//
|
|
implement
|
|
list_vt_permute$randint<>
|
|
(n) = randint(n)
|
|
//
|
|
val ((*void*)) =
|
|
(xs := list_vt_permute(xs))
|
|
//
|
|
} (* end of [deck_shuffle] *)
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
deck_takeout_top
|
|
(deck) = let
|
|
//
|
|
val+@Deck(n, xs) = deck
|
|
//
|
|
val+
|
|
~list_vt_cons(x0, xs_tl) = xs
|
|
//
|
|
val ((*void*)) = n := n - 1
|
|
val ((*void*)) = (xs := xs_tl)
|
|
//
|
|
in
|
|
fold@(deck); x0(*top*)
|
|
end // end of [deck_takeout_top]
|
|
|
|
end // end of [local]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
main0((*void*)) =
|
|
{
|
|
//
|
|
val () =
|
|
println!
|
|
(
|
|
"Hello from [Playing_cards]!"
|
|
) (* println! *)
|
|
//
|
|
val out = stdout_ref
|
|
//
|
|
val theDeck =
|
|
deck_make_full((*void*))
|
|
//
|
|
val ((*void*)) =
|
|
fprintln!(out, "theDeck = ", theDeck)
|
|
//
|
|
val ((*void*)) =
|
|
theDeck.shuffle((*void*))
|
|
//
|
|
val ((*void*)) =
|
|
fprintln!(out, "theDeck = ", theDeck)
|
|
//
|
|
val ((*void*)) =
|
|
loop_deal(theDeck) where
|
|
{
|
|
//
|
|
fun
|
|
loop_deal{n:nat}
|
|
(
|
|
deck: !deck(n) >> deck(0)
|
|
) : void =
|
|
(
|
|
if (
|
|
iseqz(deck)
|
|
) then ((*void*))
|
|
else
|
|
let
|
|
val card =
|
|
deck_takeout_top(deck)
|
|
in
|
|
fprintln!(out, card); loop_deal(deck)
|
|
end // end of [let]
|
|
// end of [else]
|
|
)
|
|
//
|
|
} (* end of [val] *)
|
|
//
|
|
val ((*freed*)) = theDeck.free()
|
|
//
|
|
} (* end of [main0] *)
|
|
|
|
(* ****** ****** *)
|