--
--
-- Mah-jong example
--
--

--
-- Matcher definitions
--
inductive Suit := Wan | Pin | Sou
inductive Honor := Ton | Nan | Sha | Pe | Haku | Hatsu | Chun
inductive Tile := Num Suit Integer | Hnr Honor

inductive pattern Suit :=
  | wan
  | pin
  | sou

inductive pattern Honor :=
  | ton
  | nan
  | sha
  | pe
  | haku
  | hatsu
  | chun

inductive pattern Tile :=
  | num Suit Integer
  | hnr Honor

def suit :=
  algebraicDataMatcher
    | wan
    | pin
    | sou

def honor :=
  algebraicDataMatcher
    | ton
    | nan
    | sha
    | pe
    | haku
    | hatsu
    | chun

def tile :=
  algebraicDataMatcher
    | num suit integer
    | hnr honor

--
-- Pattern modularization
--
def pattern pair (pat1 : Tile) (pat2 : [Tile]) : [Tile] := ($pat & ~pat1) :: #pat :: ~pat2

def pattern sequence (pat1 : Tile) (pat2 : [Tile]) : [Tile] :=
  (num $s $n & ~pat1) :: num #s #(n + 1) :: num #s #(n + 2) :: ~pat2

def pattern triplet (pat1 : Tile) (pat2 : [Tile]) : [Tile] := ($pat & ~pat1) :: #pat :: #pat :: ~pat2

--
-- A function that determines whether the hand is completed or not.
--
def complete? : [Tile] -> Bool :=
  \match as multiset tile with
    | pair
        $th_1
        (sequence $sh_1
           (sequence $sh_2
              (sequence $sh_3 (sequence $sh_4 [] | triplet $kh_1 [])
                | triplet $kh_1 (triplet $kh_2 []))
             | triplet $kh_1 (triplet $kh_2 (triplet $kh_3 [])))
          | triplet $kh_1 (triplet $kh_2 (triplet $kh_3 (triplet $kh_4 []))))
        | (pair $th_2 (pair $th_3 (pair $th_4 (pair $th_5 (pair $th_6 (pair $th_7 []))))))
    -> True
    | _ -> False

--
-- Demonstration code
--
assertEqual "mahjong 1"
  (complete?
     [ Hnr Haku,  Hnr Haku
     , Num Wan 3, Num Wan 4, Num Wan 5
     , Num Wan 6, Num Wan 7, Num Wan 8
     , Num Pin 2, Num Pin 3, Num Pin 4
     , Num Sou 6, Num Sou 6, Num Sou 6 ])
  True

assertEqual "mahjong 2"
  (complete?
     [ Hnr Haku,  Hnr Haku
     , Num Pin 1, Num Pin 3, Num Pin 4
     , Num Wan 6, Num Wan 7, Num Wan 8
     , Num Wan 3, Num Wan 4, Num Wan 5
     , Num Sou 6, Num Sou 6, Num Sou 6 ])
  False