-
Notifications
You must be signed in to change notification settings - Fork 0
/
proof2ref.py
200 lines (141 loc) · 6.05 KB
/
proof2ref.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
# -*- coding: utf-8 -*-
# proof2ref.py v0.2
# Date: 20.09.2011r
# Author: Piotr Tynecki <[email protected]>
import sys
import os
import linecache
import subprocess
# Set Mizar directory path
mizarPath = "/usr/local/share/mizar/"
copyright = "proof2ref v0.2\nCopyright (C) 2011 by Piotr Tynecki <[email protected]>"
try:
from lxml import etree
except ImportError:
print "%s\n\nError:\n\tNo module named lxml. Download from: http://lxml.de/" % copyright
sys.exit(0)
def runMizf(path):
""" Generates required files based on the miz file """
subprocess.call(["accom", path])
subprocess.call(["verifier", "-q", "-a", path])
def repairXML(path):
""" Repairs XML file """
newline = linecache.getline(path, 2)
newline = newline.replace('mizfiles="%s"' % mizarPath, 'mizfiles="%s"' % mizarPath.replace("/", "/"))
f = open(path, "rb")
source = f.readlines()
f.close()
f = open(path, "wb")
source[1] = newline
f.writelines(source)
f.close()
def getAllLineNumberFromErrFile(path):
""" Parses err file """
path = path.replace("xml", "err")
f = open(path, "rb")
source = f.readlines()
f.close()
return [x.split()[0] for x in source]
def cleanup():
""" Removes all files from text directory without miz files """
currentDirectory = os.listdir("text")
tempfiles = [x for x in currentDirectory if x.split(".")[1] == "miz"]
[currentDirectory.remove(x) for x in tempfiles]
[os.remove("text/%s" % x) for x in currentDirectory]
def replaceProof2Ref(path, XMLpath):
""" Replaces proofs with references """
numberOfChanges = [0, []]
for x, th in enumerate([x for x in etree.parse(XMLpath).findall("JustifiedTheorem")]):
if x:
runMizf(path)
if th.find("SkippedProof") is None:
proposition = th.find("Proposition")
nr = proposition.get("nr")
vid = proposition.get("vid")
# List of line/col numbers of each proof
proofsBlock = []
XML = etree.parse(XMLpath)
theorems = [theorem for theorem in XML.findall("JustifiedTheorem")]
mode = 0
for y in theorems[x + 1:]:
if y.find("SkippedProof") is None:
proof = y.find("Proof")
if proof is not None:
subProposition = y.find("Proposition")
line = subProposition.get("line")
col = subProposition.get("col")
endProof = proof.find("EndPosition")
proofsBlock.append("d%s %d %s %s\niby Th%d\n" % (proof.get("line"), int(proof.get("col")) - 4, endProof.get("line"), endProof.get("col"), x + 1))
y.remove(proof)
by = etree.Element("By", line = line, col = col)
by.append(etree.Element("Ref", nr = nr, vid = vid, line = line, col = col))
y.append(by)
XML.write(XMLpath, xml_declaration = True, method = "xml")
repairXML(XMLpath)
mode = 1
if mode:
subprocess.call(["nice", "-n", "19", "verifier", "-q", "-c", XMLpath])
# Correct references list
correctRef = [x for x in proofsBlock if x.split()[0][1:] not in getAllLineNumberFromErrFile(XMLpath)]
if correctRef:
numberOfChanges[0] += len(correctRef)
numberOfChanges[1].append(correctRef)
for numbers in correctRef:
edt = open(XMLpath.replace("xml", "edt"), "ab")
edt.write(numbers)
edt.close()
# Calls the process which updates miz file
subprocess.call(["accom", "-p", path])
subprocess.call(["edtfile", path])
subprocess.call(["mv", "-f", "%s$-$" % path[:-3], path])
cleanup()
return numberOfChanges
def createReport(score):
""" Creates report of changes about each miz file """
for x in score:
if x[1][0] > 0:
r = open("report.txt", "ab")
r.write("Filename: %s\nNumber of changes: %s\n" % (x[0], x[1][0]))
for y in x[1][1]:
r.write("\t%s\n" % y[0][:-1].replace("\n", "\n\t"))
r.write("\n")
r.close()
def main(score, path, XMLpath):
""" Runs the main procedures """
runMizf(path)
score.append((path.split("/")[-1], replaceProof2Ref(path, XMLpath)))
cleanup()
if __name__=="__main__":
argcount = len(sys.argv)
score = []
os.system("clear")
# For a single *.miz file
if argcount > 2 and sys.argv[1] == "-f":
try:
path = "%s.miz" % sys.argv[2]
XMLpath = path.replace("miz", "xml")
if not os.path.exists(path):
raise IOError
main(score, path, XMLpath)
except IOError:
print "%s\n\nError:\n\tFile %s is corrupted or doesn't exist" % (copyright, sys.argv[2])
finally:
os.system("clear")
# For all the *.miz files from a text directory
elif argcount > 2 and sys.argv[1] == "-d":
try:
directory = os.listdir(sys.argv[2])
for x in directory:
path = "%s/%s" % (sys.argv[2], x)
XMLpath = path.replace("miz", "xml")
main(score, path, XMLpath)
except OSError:
print "%s\n\nError:\n\tDirectory %s doesn't exist" % (copyright, sys.argv[2])
except IOError:
print "%s\n\nError:\n\tFile %s is corrupted or doesn't exist" % (copyright, path)
finally:
os.system("clear")
else:
print "%s\n\nExamples:\n\tpython proof2ref.py -f text/filename\n\tpython proof2ref.py -d text\n\nExtras:\n\tCreates report of changes about single/each miz file\n\tpython proof2ref.py -f text/filename -r\n\tpython proof2ref.py -d text -r" % copyright
if argcount > 3 and sys.argv[3] == "-r":
createReport(score)