| #!/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()) |