下記のプログラムは編集して実行できます。

-- -- -- 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 -- <<<<<<< HEAD def pattern twin (pat1 : Tile) (pat2 : [Tile]) : [Tile] := ($pat & ~pat1) :: #pat :: ~pat2 def pattern shuntsu (pat1 : Tile) (pat2 : [Tile]) : [Tile] := (num $s $n & ~pat1) :: num #s #(n + 1) :: num #s #(n + 2) :: ~pat2 -- (num $s $n & ~pat1) :: num #s #(i.+ n 1) :: num #s #(i.+ n 2) :: ~pat2 def pattern kohtsu (pat1 : Tile) (pat2 : [Tile]) : [Tile] := ($pat & ~pat1) :: #pat :: #pat :: ~pat2 ======= 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 >>>>>>> cbd50c069e9b0791268a2a6bf136ea17f7f995fb -- -- A function that determines whether the hand is completed or not. -- def complete? : [Tile] -> Bool := \match as multiset tile with <<<<<<< HEAD | twin $th_1 (shuntsu $sh_1 (shuntsu $sh_2 (shuntsu $sh_3 (shuntsu $sh_4 [] | kohtsu $kh_1 []) | kohtsu $kh_1 (kohtsu $kh_2 [])) | kohtsu $kh_1 (kohtsu $kh_2 (kohtsu $kh_3 []))) | kohtsu $kh_1 (kohtsu $kh_2 (kohtsu $kh_3 (kohtsu $kh_4 [])))) | (twin $th_2 (twin $th_3 (twin $th_4 (twin $th_5 (twin $th_6 (twin $th_7 [])))))) -> True ======= -- 1 pair (eyes) + 4 sequences | pair $th_1 (sequence $sh_1 (sequence $sh_2 (sequence $sh_3 (sequence $sh_4 [])))) -> True -- 1 pair + 3 sequences + 1 triplet | pair $th_1 (sequence $sh_1 (sequence $sh_2 (sequence $sh_3 (triplet $kh_1 [])))) -> True -- 1 pair + 2 sequences + 2 triplets | pair $th_1 (sequence $sh_1 (sequence $sh_2 (triplet $kh_1 (triplet $kh_2 [])))) -> True -- 1 pair + 1 sequence + 3 triplets | pair $th_1 (sequence $sh_1 (triplet $kh_1 (triplet $kh_2 (triplet $kh_3 [])))) -> True -- 1 pair + 4 triplets | pair $th_1 (triplet $kh_1 (triplet $kh_2 (triplet $kh_3 (triplet $kh_4 [])))) -> True -- 7 pairs (seven-pairs hand) | pair $th_1 (pair $th_2 (pair $th_3 (pair $th_4 (pair $th_5 (pair $th_6 (pair $th_7 [])))))) -> True >>>>>>> cbd50c069e9b0791268a2a6bf136ea17f7f995fb | _ -> 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 実行

次に見てほしいもの...

次のデモンストレーション トップに戻る