final model a4

[ar1516.git] / a2 / src / 4 / print4.py

diff --git a/a2/src/4/print4.py b/a2/src/4/print4.py
index c0fcfdd..e3eed1f 100644 (file)
--- a/a2/src/4/print4.py
+++ b/a2/src/4/print4.py
@@ -6,16 +6,50 @@ import re
 
 PAT = r'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|false)\)'
 
-def print_board(data, tofile):
+def print_board(previous, data, tofile):
     """Prints a peg solitaire board"""
-    for yco in range(8):
-        for xco in range(8):
-            pos = [d for d in data if d[0] == xco and d[1] == yco]
+    tofile.write('$\\xymatrix@=1.2pt@M=1.2pt{')
+    begin = None
+    if data is not None:
+        end = None
+        begin = []
+        for yco in range(7):
+            for xco in range(7):
+                pos = [d for d in data if d[0] == xco and d[1] == yco]
+                poso = [d for d in previous if d[0] == xco and d[1] == yco]
+                if pos and poso:
+                    if pos[0][2] and not poso[0][2]:
+                        end = pos[0]
+                    elif pos[0][2] != poso[0][2]:
+                        begin.append(pos[0])
+        if begin and end:
+            if begin[0][0] < end[0]:
+                direction = 'rr'
+                begin = min(begin, key=lambda x: x[0])
+            elif begin[0][0] > end[0]:
+                direction = 'll'
+                begin = max(begin, key=lambda x: x[0])
+            elif begin[0][1] < end[1]:
+                direction = 'dd'
+                begin = min(begin, key=lambda x: x[1])
+            elif begin[0][1] > end[1]:
+                direction = 'uu'
+                begin = max(begin, key=lambda x: x[1])
+            else:
+                direction = None
+
+    for yco in range(7):
+        for xco in range(7):
+            pos = [d for d in previous if d[0] == xco and d[1] == yco]
             if not pos:
-                tofile.write(' ')
+                tofile.write('&')
             else:
-                tofile.write('.' if pos[0][2] else 'o')
-        tofile.write('\n')
+                tofile.write('\\circ ' if pos[0][2] else '\\times ')
+                if begin and pos[0][0] == begin[0] and pos[0][1] == begin[1]:
+                    tofile.write('\\ar@{{-)}}[{}]'.format(direction))
+                tofile.write('&')
+        tofile.write('\\\\\n')
+    tofile.write('}$\n')
 
 def parse(lines, output):
     """Parse the model from yices"""
@@ -29,9 +63,19 @@ def parse(lines, output):
                 data[ite] = []
             data[ite].append((int(match.group('x')), int(match.group('y')),
                               match.group('v') == 'true'))
-    for _, dat in sorted(data.items()):
-        print_board(dat, output)
-
+    output.write('\\begin{tabular}{cccccc}\n')
+    prev = None
+    for i, (_, dat) in enumerate(sorted(data.items())):
+        if prev is None:
+            prev = dat
+        else:
+            print_board(prev, dat, output)
+            prev = dat
+            output.write(' & ')
+            if i % 5 == 0:
+                output.write('\\\\\\\\')
+    print_board(prev, None, output)
+    output.write('\\end{tabular}\n')
 
 if __name__ == '__main__':
     if len(sys.argv) == 1: