original.name="Record_Valid_5"
======
>>> main.whiley
type nat is (int x) where x >= 0

// =======================================
// Card Definition
// =======================================

// Suites
final int HEARTS = 1
final int CLUBS = 2
final int DIAMONDS = 3
final int SPADES = 4

// Ordinals
final int TWO = 2
final int THREE = 3
final int FOUR = 4
final int FIVE = 5
final int SIX = 6
final int SEVEN = 7
final int EIGHT = 8
final int NINE = 9
final int TEN = 10
final int JACK = 11
final int QUEEN = 12
final int KING = 13
final int ACE = 14

type Card is {
    int suite,
    int ordinal
}
// Suite between hearts and clubs
where HEARTS <= suite && suite <= SPADES
// Ordinal between 2 and ACE (high)
where 2 <= ordinal && ordinal <= ACE

// Define a "comparator" for cards
property lessThan(Card c1, Card c2) -> (bool r):
    return (c1.suite == c2.suite && c1.ordinal < c2.ordinal) ||
           (c1.suite != c2.suite && c1.suite < c2.suite)

property sorted(Card[] cards) -> (bool r):
    return |cards| == 0 || all { i in 1..|cards| | lessThan(cards[i-1],cards[i]) }

// =======================================
// Card Constants
// =======================================

final Card TWO_HEARTS = { suite: HEARTS, ordinal: TWO }
final Card THREE_HEARTS = { suite: HEARTS, ordinal: THREE }
final Card FOUR_HEARTS = { suite: HEARTS, ordinal: FOUR }
final Card FIVE_HEARTS = { suite: HEARTS, ordinal: FIVE }
final Card SIX_HEARTS = { suite: HEARTS, ordinal: SIX }
final Card SEVEN_HEARTS = { suite: HEARTS, ordinal: SEVEN }
final Card EIGHT_HEARTS = { suite: HEARTS, ordinal: EIGHT }
final Card NINE_HEARTS = { suite: HEARTS, ordinal: NINE }
final Card TEN_HEARTS = { suite: HEARTS, ordinal: TEN }
final Card JACK_HEARTS = { suite: HEARTS, ordinal: JACK }
final Card QUEEN_HEARTS = { suite: HEARTS, ordinal: QUEEN }
final Card KING_HEARTS = { suite: HEARTS, ordinal: KING }
final Card ACE_HEARTS = { suite: HEARTS, ordinal: ACE }

final Card TWO_CLUBS = { suite: CLUBS, ordinal: TWO }
final Card THREE_CLUBS = { suite: CLUBS, ordinal: THREE }
final Card FOUR_CLUBS = { suite: CLUBS, ordinal: FOUR }
final Card FIVE_CLUBS = { suite: CLUBS, ordinal: FIVE }
final Card SIX_CLUBS = { suite: CLUBS, ordinal: SIX }
final Card SEVEN_CLUBS = { suite: CLUBS, ordinal: SEVEN }
final Card EIGHT_CLUBS = { suite: CLUBS, ordinal: EIGHT }
final Card NINE_CLUBS = { suite: CLUBS, ordinal: NINE }
final Card TEN_CLUBS = { suite: CLUBS, ordinal: TEN }
final Card JACK_CLUBS = { suite: CLUBS, ordinal: JACK }
final Card QUEEN_CLUBS = { suite: CLUBS, ordinal: QUEEN }
final Card KING_CLUBS = { suite: CLUBS, ordinal: KING }
final Card ACE_CLUBS = { suite: CLUBS, ordinal: ACE }

final Card TWO_DIAMONDS = { suite: DIAMONDS, ordinal: TWO }
final Card THREE_DIAMONDS = { suite: DIAMONDS, ordinal: THREE }
final Card FOUR_DIAMONDS = { suite: DIAMONDS, ordinal: FOUR }
final Card FIVE_DIAMONDS = { suite: DIAMONDS, ordinal: FIVE }
final Card SIX_DIAMONDS = { suite: DIAMONDS, ordinal: SIX }
final Card SEVEN_DIAMONDS = { suite: DIAMONDS, ordinal: SEVEN }
final Card EIGHT_DIAMONDS = { suite: DIAMONDS, ordinal: EIGHT }
final Card NINE_DIAMONDS = { suite: DIAMONDS, ordinal: NINE }
final Card TEN_DIAMONDS = { suite: DIAMONDS, ordinal: TEN }
final Card JACK_DIAMONDS = { suite: DIAMONDS, ordinal: JACK }
final Card QUEEN_DIAMONDS = { suite: DIAMONDS, ordinal: QUEEN }
final Card KING_DIAMONDS = { suite: DIAMONDS, ordinal: KING }
final Card ACE_DIAMONDS = { suite: DIAMONDS, ordinal: ACE }

final Card TWO_SPADES = { suite: SPADES, ordinal: TWO }
final Card THREE_SPADES = { suite: SPADES, ordinal: THREE }
final Card FOUR_SPADES = { suite: SPADES, ordinal: FOUR }
final Card FIVE_SPADES = { suite: SPADES, ordinal: FIVE }
final Card SIX_SPADES = { suite: SPADES, ordinal: SIX }
final Card SEVEN_SPADES = { suite: SPADES, ordinal: SEVEN }
final Card EIGHT_SPADES = { suite: SPADES, ordinal: EIGHT }
final Card NINE_SPADES = { suite: SPADES, ordinal: NINE }
final Card TEN_SPADES = { suite: SPADES, ordinal: TEN }
final Card JACK_SPADES = { suite: SPADES, ordinal: JACK }
final Card QUEEN_SPADES = { suite: SPADES, ordinal: QUEEN }
final Card KING_SPADES = { suite: SPADES, ordinal: KING }
final Card ACE_SPADES = { suite: SPADES, ordinal: ACE }

// =======================================
// Hand
// =======================================

type Hand is { Card[] cards }
// Cards in a hand should be properly arranged!!
where sorted(cards)

function Hand(Card[] cards) -> Hand
requires sorted(cards):
    //
    return {cards: cards}

// =======================================
// TEST
// =======================================

public export method test():
    //
    assume Hand([TWO_HEARTS]) == {cards: [TWO_HEARTS]}
    assume Hand([TEN_HEARTS,THREE_CLUBS]) == {cards: [TEN_HEARTS,THREE_CLUBS]}
    assume Hand([TWO_HEARTS,FOUR_CLUBS,QUEEN_SPADES]) == {cards: [TWO_HEARTS,FOUR_CLUBS,QUEEN_SPADES]}


---