56 lines
1.9 KiB
Python
Executable file
56 lines
1.9 KiB
Python
Executable file
#!/usr/bin/python3
|
|
import sys
|
|
import os
|
|
import argparse
|
|
|
|
def get_block(l, h):
|
|
i = l.index('.' + h)
|
|
j = l.index('----', i+1)
|
|
k = l.index('----', j+1)
|
|
return j+1, l[j+1:k]
|
|
|
|
def convert(fn, args):
|
|
with open(fn) as f:
|
|
lines = [line.rstrip() for line in f]
|
|
imp_line, implementation = get_block(lines, args.imarker)
|
|
proof_line, proof = get_block(lines, args.pmarker)
|
|
|
|
basename = os.path.splitext(os.path.basename(fn))[0]
|
|
header = os.path.join(args.destdir, basename + '.h')
|
|
guard = 'HD2E_%s' % basename.upper()
|
|
if not args.proof_only:
|
|
with open(header, 'w') as f:
|
|
print('#ifndef %s' % guard, file=f)
|
|
print('#define %s' % guard, file=f)
|
|
for line in implementation:
|
|
print(line, file=f)
|
|
print('#endif', file=f)
|
|
|
|
proof_cc = os.path.join(args.destdir, basename + '.cc')
|
|
if not args.header_only:
|
|
with open(proof_cc, 'w') as f:
|
|
print('#include "proof_common.h"', file=f)
|
|
print('#line %d "%s"' % (imp_line+1, fn), file=f)
|
|
for line in implementation:
|
|
print(line, file=f)
|
|
print('#line %d "%s"' % (proof_line+1, fn), file=f)
|
|
for line in proof:
|
|
print(line, file=f)
|
|
|
|
parser = argparse.ArgumentParser()
|
|
parser.add_argument("--imarker", help="marker for implementation",
|
|
default="Implementation")
|
|
parser.add_argument("--pmarker", help="marker for proof", default="Proof")
|
|
parser.add_argument("--destdir", help="destination directory")
|
|
parser.add_argument("--proof-only", help="only create proof program", action='store_true')
|
|
parser.add_argument("--header-only", help="only create header", action='store_true')
|
|
parser.add_argument("filename", nargs="+")
|
|
args = parser.parse_args()
|
|
|
|
try:
|
|
os.makedirs(args.destdir)
|
|
except os.error:
|
|
pass
|
|
|
|
|
|
for fn in args.filename: convert(fn, args)
|