(* ****** ****** *)
//
#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] *)

(* ****** ****** *)