-
Notifications
You must be signed in to change notification settings - Fork 0
/
cc.py
89 lines (82 loc) · 2.35 KB
/
cc.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
import sys
import os
import subprocess
from functools import reduce
def collapse(gen):
tmp = ''
for l in gen:
if l.startswith('--') or l.strip() == '':
continue
if l == l.lstrip():
if tmp != '':
yield tmp
tmp = ''
tmp = (tmp + ' ' + l.strip()).strip()
if tmp != '':
yield tmp
with open(sys.argv[1]) as f:
*prog, query = list(collapse(f.readlines()))
desugar = lambda s: (s
.replace(' where ', '__MAGIC_IMPL__')
.replace(' <== ', '__MAGIC_IMPL__')
.replace(', ', '__MAGIC_SEP__')
.replace('=', 'tEQ')
.replace('>', 'tLT')
.replace('<', 'tGT')
.replace('$', 'tDOLLAR')
.replace('+', 'tADD')
.replace('-', 'tSUB')
.replace('*', 'tMUL')
.replace(':', 'tCOLON')
.replace(' ', ':')
.replace('__MAGIC_IMPL__', ':-FUEL__@@')
.replace('__MAGIC_SEP__', ',FUEL__@@'))
unlines = lambda s: '\n'.join(s)
prog = [('s(FUEL__)@@' if 'FUEL__' in p else '_@@') + p
for l in prog
for p in [desugar(l)]]
resugar = lambda s: (s
.replace(':', ' ')
.replace('tCOLON', ':')
.replace('tMUL', '*')
.replace('tSUB', '-')
.replace('tADD', '+')
.replace('tDOLLAR', '$')
.replace('tLT', '<')
.replace('tGT', '>')
.replace('tEQ', '='))
i = query.index('?')
(fuel, *metas), query = query[:i].split(), desugar(query[i+1:].strip())
peano = lambda n: reduce(lambda x, _: f's({x})', range(n), 'z')
dump_metas_cmd = '(' + ', '.join(f"write('{x} = '), writeln({x})" for x in metas) + ')'
# commands = ',\n '.join(f'''
# writeln('depth {n}'),
# {peano(n)}@@{query},
# {dump_metas_cmd}
# ''' for n in range(int(fuel)+1))
prog = f'''
:- op(150, yfx, :).
:- op(950, xfx, @@).
:- set_prolog_flag(occurs_check, true).
% :- use_module(library(tabling)).
% :- table (@@)/2.
tEQUAL(X, X).
run_query(z, D, Query) :- write('depth '), writeln(D), D@@Query.
run_query(s(Remaining), D, Query) :-
write('depth '), writeln(D), D@@Query;
run_query(Remaining, s(D), Query).
{unlines(prog)}
:- initialization forall(run_query({peano(int(fuel))}, z, {query}), {dump_metas_cmd}).'''
with open('tmp.pl' if len(sys.argv) <= 2 else sys.argv[2], 'w') as tmp:
print(prog, file=tmp)
p = subprocess.Popen(
['prolog', '-l', 'tmp.pl', '-t', 'halt'],
stdout=subprocess.PIPE,
stderr=open(os.devnull, 'w'))
try:
while True:
l = p.stdout.readline()
if not l: break
print(resugar(l.decode().rstrip()))
except KeyboardInterrupt:
pass