Strip literate agda down to agda

lagdastrip.py

#!/usr/bin/env python3

import sys

def get_code_lines(lines):
    in_code = False
    for line in lines:
        if line.startswith(r'\begin{code}'):
            in_code = True
            yield '--STRIP: '
        elif line.startswith(r'\end{code}'):
            in_code = False
            yield '--STRIP: '
        elif not in_code or line.startswith(r'module '):
            yield '--STRIP: '
        yield line


def strip(fname):
    assert(fname[-6:] == '.lagda')
    oname = fname[:-6] + '-stripped.agda'
    with open(fname) as f:
        lines = f.readlines()
    with open(oname, 'w') as f:
        for line in get_code_lines(lines):
            f.write(line)


if __name__ == '__main__':
    strip('Formula.lagda')
    for x in sys.argv[1:]:
        strip(x)