blob: 212c467bf02c96363a787907cf41ab992a0abb42 [file] [log] [blame] [edit]
#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#
#
'''
Basic pre-processor for Isabelle theory files. Feel free to extend this with
passes you'd like to make available, but avoid doing anything more complicated
than sed-style manipulations here. Anything more complicated needs a proper
semantic understanding of Isabelle theories.
'''
import argparse, re, subprocess, sys, textwrap
class Pass(object):
'''A line-wise pre-processor pass. Extend this to specify a line
transformation.'''
def __init__(self, arg, default=False, help=''):
self.arg = arg # Long form command line argument
self.option = arg.replace('-', '_')
self.default = default # Enabled by default?
self.help = help # Command line help string
def __call__(self, line, properties):
'''This function accepts the current line and should return the
transformed line, or None to indicate this line should be omitted.'''
raise NotImplementedError
def notify(self, properties):
return None
class RemoveDuplicateNewlines(Pass):
def __init__(self):
super(RemoveDuplicateNewlines, self).__init__(
'remove-duplicate-newlines', True,
'turn adjacent empty lines into a single empty line')
self.lastempty = False
def __call__(self, line, *_):
if line.strip() == '':
if self.lastempty:
return None
else:
self.lastempty = True
else:
self.lastempty = False
return line
class Rstrip(Pass):
def __init__(self):
super(Rstrip, self).__init__('rstrip', True,
'strip trailing whitespace')
def __call__(self, line, *_):
return line.rstrip()
class DropLeadingBlankLines(Pass):
def __init__(self):
super(DropLeadingBlankLines, self).__init__('drop-leading-blank-lines',
True,
'remove any blank lines at the start of the file')
self.initial = True
def __call__(self, line, *_):
if not self.initial:
return line
if not line.strip():
return None
self.initial = False
return line
class Condense(Pass):
def __init__(self):
super(Condense, self).__init__('condense', True,
'drop all blank lines in sections where the property ' \
'\'condense\' is True')
def __call__(self, line, properties):
if properties.get('condense', False) and not line.strip():
return None
return line
class LockIndent(Pass):
def __init__(self):
super(LockIndent, self).__init__('lock-indent', True,
'fix indentation level of statements when the \'lock_indent\' is ' \
'defined to the number of spaces it specifies')
def __call__(self, line, properties):
if not line.strip():
return line
indentation = properties.get('lock_indent', None)
if indentation is not None:
line = '%s%s' % (indentation * ' ', line.lstrip())
return line
class Cowsay(Pass):
def __init__(self):
super(Cowsay, self).__init__('cowsay', False, 'try it and see...')
def __call__(self, line, properties):
cowsay = properties.get('cowsay')
if cowsay is not None:
p = subprocess.Popen('cowsay %s' % cowsay, shell=True,
stdin=subprocess.PIPE, stdout=subprocess.PIPE,
stderr=subprocess.PIPE, universal_newlines=True)
stdout, stderr = p.communicate(line)
if stderr:
sys.stderr.write('cowsay: %s\n' % stderr)
del properties['cowsay']
return stdout
return line
class Accumulate(Pass):
def __init__(self):
super(Accumulate, self).__init__('accumulate', True,
'allow accumulation of multiple lines when the \'accumulate\' ' \
'property is set to True')
self.accumulated = None
def __call__(self, line, properties):
if properties.get('accumulate', False):
if self.accumulated is None:
if not line.strip():
# Don't begin accumulating nothing.
return None
self.accumulated = '%s ' % line
else:
self.accumulated += '%s ' % line.strip()
return None
assert self.accumulated is None
return line
def notify(self, properties):
if not properties.get('accumulate', False) and self.accumulated is not None:
l = self.accumulated.rstrip()
ls = textwrap.wrap(l, 80,
subsequent_indent=(' ' * (len(l) - len(l.lstrip()) + 2)))
self.accumulated = None
return ls
return None
class CompressBrackets(Pass):
sub1 = re.compile(r'([^ ]) \)')
sub2 = re.compile(r'\( ([^ ])')
def __init__(self):
super(CompressBrackets, self).__init__('compress-brackets', True,
'remove space between leading and trailing brackets')
def __call__(self, line, *_):
return self.sub1.sub(r'\1)', self.sub2.sub(r'(\1', line))
class CompressBraces(Pass):
sub1 = re.compile(r'([^ ]) \}')
sub2 = re.compile(r'\{ ([^ ])')
def __init__(self):
super(CompressBraces, self).__init__('compress-braces', True,
'remove space between leading and trailing braces')
def __call__(self, line, *_):
return self.sub1.sub(r'\1}', self.sub2.sub(r'{\1', line))
class CompressCommas(Pass):
sub1 = re.compile(r'([^ ]) ,')
def __init__(self):
super(CompressCommas, self).__init__('compress-commas', True,
'remove space before commas')
def __call__(self, line, *_):
return self.sub1.sub(r'\1,', line)
def main():
p = argparse.ArgumentParser(description='Isabelle theory pre-processor')
p.add_argument('--output', '-o', type=argparse.FileType('w'),
default=sys.stdout, help='output to a file rather than stdout')
p.add_argument('input', type=argparse.FileType('r'), nargs='?',
default=sys.stdin, help='input file')
# Add each of the processing passes.
PASSES = [
Rstrip(),
DropLeadingBlankLines(),
Condense(),
LockIndent(),
Cowsay(),
Accumulate(),
CompressBrackets(),
CompressBraces(),
CompressCommas(),
RemoveDuplicateNewlines(),
]
for i in PASSES:
p.add_argument('--f%s' % i.arg, action='store_true', default=i.default,
help=i.help, dest=i.option)
p.add_argument('--fno-%s' % i.arg, action='store_false',
help='do not %s' % i.help, dest=i.option)
# Parse the command line arguments.
options = p.parse_args()
# Directives can be provided in the input in the form:
# (** TPP: property = value *)
# We construct this regex ahead of time for performance reasons.
directive_syntax = re.compile(r'\(\*\*\s+TPP:\s*(\w+)\s*=\s*(.*)\s*\*\)$')
properties = {}
lineno = 0
buffered = []
while True:
# Each loop iteration retrieve a line we were previously returned or
# read a new line from the input.
if len(buffered) > 0:
line = buffered.pop(0)
else:
lineno += 1
try:
line = next(options.input)
except StopIteration:
break
# Strip the trailing \n to make life easier for the passes.
if line.endswith('\n'):
line = line[:-1]
directive = directive_syntax.match(line.strip())
if directive is not None:
try:
properties[directive.group(1)] = eval(directive.group(2))
except:
sys.stderr.write('%(file)s:%(lineno)d: invalid directive '
'\'%(line)s\'\n' % {
'file':options.input.name,
'lineno':lineno,
'line':line,
})
# If we received a directive, notify each enabled pass of the
# change in properties so they can push back extra lines to insert
# into the output.
for i in PASSES:
if getattr(options, i.option):
rs = i.notify(properties)
if rs is not None:
buffered += rs
continue
for i in PASSES:
if getattr(options, i.option):
# This pass is enabled.
line = i(line, properties)
# That pass instructed us to remove this line.
if line is None:
break
if line is not None:
options.output.write('%s\n' % line)
if properties.get('condense'):
sys.stderr.write('warning: condense was still enabled at end of file\n')
return 0
if __name__ == '__main__':
sys.exit(main())