1 2 3(*****************************************************************************) 4(* Simplified game of Solitaire *) 5(*****************************************************************************) 6 7(*****************************************************************************) 8(* State variables *) 9(* *) 10(* 01 02 03 *) 11(* 04 05 06 07 *) 12(* 08 09 10 11 12 *) 13(* 13 14 15 16 *) 14(* 17 18 19 *) 15(* *) 16(*****************************************************************************) 17 18(* Nice ASCII picture (rotated 90 degrees from one above) 19 20 X 21 X X 22X X X 23 X X 24X X X 25 X X 26X X X 27 X X 28 X 29 30 ____ 31 / \ 32 ____/ 12 \____ 33 / \ / \ 34 ____/ 07 \____/ 16 \____ 35 / \ / \ / \ 36 / 03 \____/ 11 \____/ 19 \ 37 \ / \ / \ / 38 \____/ 06 \____/ 15 \____/ 39 / \ / \ / \ 40 / 02 \____/ 10 \____/ 18 \ 41 \ / \ / \ / 42 \____/ 05 \____/ 14 \____/ 43 / \ / \ / \ 44 / 01 \____/ 09 \____/ 17 \ 45 \ / \ / \ / 46 \____/ 04 \____/ 13 \____/ 47 \ / \ / 48 \____/ 08 \____/ 49 \ / 50 \____/ 51 52*) 53 54 55(* 56load "HolBddLib"; 57load "PrimitiveBddRules"; 58load "ListPair"; 59*) 60 61 62open HolKernel Parse boolLib; 63infixr 3 -->; 64infix 9 by; 65infix ++; 66infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 67 68open HolBddLib; 69open bdd; 70open pairSyntax; 71open bossLib; 72 73val _ = new_theory "HexSolitaire"; 74 75val _ = Globals.priming := SOME ""; 76 77val vl = [01,02,03,04,05,06,07,08,09,10,11,12,13,14,15,16,17,18,19]; 78 79fun mk_v n = 80 if n<10 then mk_var("v0"^(int_to_string n),bool) 81 else mk_var("v"^(int_to_string n),bool); 82 83fun mk_v' n = 84 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool) 85 else mk_var("v"^(int_to_string n)^"'",bool); 86 87val s = list_mk_pair (map mk_v vl) 88and s' = list_mk_pair (map mk_v' vl); 89 90fun shuffle (l1,l2) = 91 ListPair.foldr (fn(x1,x2,l) => x1 :: x2 :: l) [] (l1,l2); 92 93fun mk_bool_var s = mk_var(s,bool); 94 95val hexsolitaire_varmap = 96 extendVarmap 97 (map mk_bool_var (shuffle(map (fst o dest_var o mk_v) vl, map (fst o dest_var o mk_v') vl))) 98 empty; 99 100val HexSolitaireInit_def = 101 bossLib.Define 102 `HexSolitaireInit ^s = 103 ^(list_mk_conj 104 (map (fn n => if n=10 then mk_neg(mk_v n) else mk_v n) vl))`; 105 106fun make_move (n1,n2,n3) = 107 let val (_,unchanged) = List.partition (fn n => mem n [n1,n2,n3]) vl 108 in 109 list_mk_conj 110 ([mk_v n1,mk_v n2,mk_neg(mk_v n3), 111 mk_neg(mk_v' n1),mk_neg(mk_v' n2),mk_v' n3] 112 @ 113 (map (fn n => mk_eq(mk_v' n,mk_v n)) unchanged)) 114 end; 115 116val moves = 117 [(01,02,03),(01,05,10),(01,04,08), 118 (02,06,11),(02,05,09), 119 (03,07,12),(03,06,10),(03,02,01), 120 (04,05,06),(04,09,14), 121 (05,06,07),(05,10,15),(05,09,13), 122 (06,11,16),(06,10,14),(06,05,04), 123 (07,11,15),(07,06,05), 124 (08,04,01),(08,09,10),(08,13,17), 125 (09,05,02),(09,10,11),(09,14,18), 126 (10,09,08),(10,05,01),(10,06,03),(10,11,12),(10,15,19),(10,14,17), 127 (11,10,09),(11,06,02),(11,15,18), 128 (12,11,10),(12,07,03),(12,16,19), 129 (13,09,05),(13,14,15), 130 (14,09,04),(14,10,06),(14,15,16), 131 (15,14,13),(15,10,05),(15,11,07), 132 (16,15,14),(16,11,06), 133 (17,13,08),(17,14,10),(17,18,19), 134 (18,14,09),(18,15,11), 135 (19,18,17),(19,15,10),(19,16,12)]; 136 137val HexSolitaireTrans_def = 138 bossLib.Define `HexSolitaireTrans(^s,^s') = 139 ^(list_mk_disj(map make_move moves))`; 140 141(*****************************************************************************) 142(* Final goal state *) 143(*****************************************************************************) 144 145val HexSolitaireFinish_def = 146 bossLib.Define 147 `HexSolitaireFinish ^s = 148 ^(list_mk_conj 149 (map (fn n => if (n=10 orelse n=18) 150 then mk_v n 151 else mk_neg(mk_v n)) vl))`; 152 153(* This has no solution 154val HexSolitaireFinish_def = 155 bossLib.Define 156 `HexSolitaireFinish ^s = 157 ^(list_mk_conj 158 (map (fn n => if (n=10) 159 then mk_v n 160 else mk_neg(mk_v n)) vl))`; 161*) 162 163val (initth,transthl,finalth) = 164 findTrace 165 hexsolitaire_varmap 166 HexSolitaireTrans_def 167 HexSolitaireInit_def 168 HexSolitaireFinish_def; 169 170(*****************************************************************************) 171(* Print out a picture of a HexSolitaire board from a tuple *) 172(* *) 173(* (c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19) *) 174(* *) 175(* where cij is T or F *) 176(* *) 177(* and the printing is *) 178(* *) 179(* X X X *) 180(* X X X X *) 181(* X X X X X *) 182(* X X X X *) 183(* X X X *) 184(*****************************************************************************) 185 186fun PrintState tm = 187 let val cl = strip_pair tm 188 fun p n = print_term(el n cl) 189 fun sp () = print " " 190 fun nl () = print"\n" 191 in 192 (print" ";p 1 ;sp();p 2 ;sp();p 3 ;nl(); 193 print" " ;p 4 ;sp();p 5 ;sp();p 6 ;sp();p 7 ;nl(); 194 print" " ;p 8 ;sp();p 9 ;sp();p 10;sp();p 11;sp();p 12;nl(); 195 print" " ;p 13;sp();p 14;sp();p 15;sp();p 16;nl(); 196 print" ";p 17;sp();p 18;sp();p 19;nl();nl()) 197 end; 198 199(*****************************************************************************) 200(* Print out a trace as found by findTrace *) 201(*****************************************************************************) 202 203val _ = 204 List.map 205 PrintState 206 (List.map (fst o dest_pair o rand o concl) transthl @ [rand(concl finalth)]); 207 208val _ = export_theory(); 209