-- Data type declarations
inductive Suit := Spade | Heart | Club | Diamond
inductive Card := Card Suit Integer | Joker

-- Pattern constructor declarations
inductive pattern Suit :=
  | spade
  | heart
  | club
  | diamond

inductive pattern Card :=
  | card Suit Integer
  | joker

-- Matcher definitions
def suit {a} : Matcher Suit := algebraicDataMatcher
  | spade
  | heart
  | club
  | diamond

def card {a, b} : Matcher Card := matcher
  | card $ $ as (suit, mod 13) with
    | Card $x $y -> [(x, y)]
    | Joker -> matchAll ([Spade, Heart, Club, Diamond], [1..13]) as (set something, set something) with
               | ($s :: _, $n :: _) -> (s, n)
  | $ as something with
    | $tgt -> [tgt]

def poker (cs: [Card]) : String :=
  match cs as multiset card with
  | card $s $n :: card #s #(n - 1) :: card #s #(n - 2) :: card #s #(n - 3) :: card #s #(n - 4) :: _
    -> "Straight flush"
  | card _ $n :: card _ #n :: card _ #n :: card _ #n :: _ :: []
    -> "Four of a kind"
  | card _ $m :: card _ #m :: card _ #m :: card _ $n :: card _ #n :: []
    -> "Full house"
  | card $s _ :: card #s _ :: card #s _ :: card #s _ :: card #s _ :: []
    -> "Flush"
  | card _ $n :: card _ #(n - 1) :: card _ #(n - 2) :: card _ #(n - 3) :: card _ #(n - 4) :: []
    -> "Straight"
  | card _ $n :: card _ #n :: card _ #n :: _ :: _ :: []
    -> "Three of a kind"
  | card _ $m :: card _ #m :: card _ $n :: card _ #n :: _ :: []
    -> "Two pair"
  | card _ $n :: card _ #n :: _ :: _ :: _ :: []
    -> "One pair"
  | _ :: _ :: _ :: _ :: _ :: [] -> "Nothing"

assertEqual "poker hand 1"
  (poker [Card Spade 5, Card Spade 6, Joker, Card Spade 8, Card Spade 9])
  "Straight flush"

assertEqual "poker hand 2"
  (poker [Card Spade 5, Card Diamond 5, Card Spade 7, Joker, Card Heart 5])
  "Four of a kind"

assertEqual "poker hand 3"
  (poker [Card Spade 5, Joker, Card Spade 7, Card Spade 13, Card Spade 9])
  "Flush"

assertEqual "poker hand 4"
  (poker [Card Spade 5, Card Club 6, Joker, Card Spade 8, Card Spade 9])
  "Straight"

assertEqual "poker hand 5"
  (poker [Card Spade 5, Card Diamond 5, Card Spade 7, Joker, Card Heart 8])
  "Three of a kind"

assertEqual "poker hand 6"
  (poker [Card Spade 5, Card Diamond 10, Card Spade 7, Joker, Card Heart 8])
  "One pair"