forked from dcolish/Cockerel
-
Notifications
You must be signed in to change notification settings - Fork 0
/
prover.py
109 lines (89 loc) · 3.48 KB
/
prover.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
from json import JSONDecoder, JSONEncoder
from hashlib import sha1
import logging
import telnetlib
from uuid import uuid4
from flask import (
g,
Module,
url_for,
render_template,
request,
session,
)
from cockerel.models.schema import Proof, Theorem
prover = Module(__name__)
def readscript(script):
'''Chew up blank lines'''
return [x for x in script.splitlines() if not x == '']
def formatscript(script, slice):
commandlist = readscript(script)
processed = '\\n'.join(commandlist[:slice])
unprocessed = '\\n'.join(commandlist[slice:])
return processed, unprocessed, commandlist
def hash_theorem(theorem):
return sha1(theorem).hexdigest()
def ping_coqd():
pass
@prover.route('/prover', methods=['GET', 'POST'])
def editor():
proofst = None
host = g.config.get('COQD_HOST')
port = g.config.get('COQD_PORT')
lineno = 0
if request.method == 'POST':
if not session.get('id'):
session['id'] = uuid4()
if request.form.get('clear'):
command = 'quit'
proofscript = request.form.get('proofscript')
processed, unprocessed, commandlist = formatscript(proofscript, 0)
processed = None
elif request.form.get('undo'):
lineno = 0 if lineno == 0 else int(request.form.get('line')) - 1
proofscript = request.form.get('proofscript')
processed, unprocessed, commandlist = formatscript(proofscript,
lineno)
command = 'Undo.'
else:
lineno = int(request.form.get('line'))
proofscript = request.form.get('proofscript')
processed, unprocessed, commandlist = formatscript(proofscript,
lineno)
command = commandlist[lineno]
logging.debug('Sending %d : %s', lineno, command)
lineno += 1
# here is where we'll pass it to coqd
if command:
try:
tn = telnetlib.Telnet(host, port)
tn.write(JSONEncoder().encode(dict(userid=str(session['id']),
command=command)))
proofst = JSONDecoder().decode(tn.read_all())
proofst = proofst.get('response', None)
except Exception:
lineno = lineno - 1 if lineno != 0 else 0
logging.error("Connection to coqd failed")
return render_template('prover/prover.html',
prover_url=url_for('editor'),
processed=processed,
unprocessed=unprocessed,
proofst=proofst,
lineno=lineno)
else:
# new proof session so set it up
unprocessed = request.args.get('theorem', "")
theorem = Theorem.query.filter_by(id=unprocessed).one()
if theorem:
text = theorem.text.rstrip()
proof = Proof.query.filter_by(theorem=theorem).first()
if not proof:
proof = ""
else:
theorem = proof = ""
return render_template('prover/prover.html',
prover_url=url_for('editor'),
proofst=proofst,
processed=None,
unprocessed=''.join([text,proof]),
lineno=lineno)