HoTT/HoTT — pull request #632 by JasonGross (2014-12-03 19:51:44+00:00)
Title: Normalize variable declarations

We no longer need to separate [Variable foo : PreCategory] onto multiple
lines to separate universes.

This change made by invoking

git ls-files '*.v' | xargs python combine_variables.py

on

```python
#!/usr/bin/env python
from __future__ import with_statement
import re, sys

REG = re.compile(r'^(\s*)Variables?\s+([^:]+):([^\.]+)\.\s*$')
def groups_to_string(indent, variables, types):
variable_list = [i for i in variables.split(' ') if i]
var = ('Variables' if len(variable_list) > 1 else 'Variable')
return '%s%s %s : %s.' % (indent,
var,
' '.join(variable_list),
types.strip())
def fix_file(contents):
ret = []
prev_groups = tuple()
for line in contents.split('\n'):
next_groups = REG.findall(line)
if prev_groups:
indent, variables, types = prev_groups
if next_groups:
new_indent, new_variables, new_types = next_groups[0]
if new_indent == indent and types.strip() == new_types.strip():
prev_groups = (indent, variables + ' ' + new_variables, types)
else:
ret.append(groups_to_string(indent, variables, types))
prev_groups = (new_indent, new_variables, new_types)
else:
ret.append(groups_to_string(indent, variables, types))
ret.append(line)
prev_groups = tuple()
elif next_groups:
prev_groups = next_groups[0]
else:
ret.append(line)
if prev_groups:
ret.append(groups_to_string(*prev_groups))
return '\n'.join(ret)

if __name__ == '__main__':
if len(sys.argv) == 1 or '--help' in sys.argv or '-h' in sys.argv:
print('Usage: %s FILE_NAME [FILE_NAME ..]' % sys.argv[0])
print('Replaces [Variable X : T. Variable Y : T.] with [Variables X Y : T.]')
sys.exit(0)
for i in sys.argv[1:]:
with open(i, 'r') as f:
contents = f.read()
new_contents = fix_file(contents)
if new_contents != contents:
with open(i, 'w') as f:
f.write(new_contents)
```