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