forked from mmaroti/prover9-mace4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
utilities.py
90 lines (79 loc) · 2.42 KB
/
utilities.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
# Copyright (C) 2007 William McCune
#
# This file is part of the LADR Deduction Library.
#
# The LADR Deduction Library is free software; you can redistribute it
# and/or modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; either version 2 of the
# License, or (at your option) any later version.
#
# The LADR Deduction Library is distributed in the hope that it will be
# useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with the LADR Deduction Library; if not, write to the Free Software
# Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
#
import re
def grep(pattern, lines):
result = []
for line in lines:
if re.search(pattern, line):
result.append(line)
return result
def grep_last(pattern, lines):
result = None
for line in lines:
if re.search(pattern, line):
result = line
return result
def pattern_spans(pattern, string):
r = re.compile(pattern)
spans = []
m = r.search(string, 0)
while m:
spans.append(m.span())
m = r.search(string, m.end())
return spans
def comment_spans(s):
i = 0
spans = []
length = len(s)
while i < length:
if s[i] == '%':
start = i
if s[i:i+6] == '%BEGIN':
# block comment
while i <= length and s[i-4:i] != 'END%':
i += 1
end = min(i,length)
else:
# line comment
while i < length and s[i] != '\n':
i += 1
end = i # ok if string ends without \n
spans.append((start,end))
else:
i += 1
return spans
def member(x, b):
if b == []:
return False
elif x == b[0]:
return True
else:
return member(x, b[1:])
def intersect(a, b):
if a == []:
return []
elif member(a[0], b):
return [a[0]] + intersect(a[1:], b)
else:
return intersect(a[1:], b)
def remove_reg_exprs(exprs, str):
pat = '|'.join(exprs)
r = re.compile(pat)
str = r.sub('', str)
return str