1  #!/usr/bin/python3
 2  import sys
 3  import os
 4  import argparse
 5  
 6  def get_block(l, h):
 7      i = l.index('.' + h)
 8      j = l.index('----', i+1)
 9      k = l.index('----', j+1)
10      return j+1, l[j+1:k]
11  
12  def convert(fn, args):
13      with open(fn) as f:
14          lines = [line.rstrip() for line in f]
15          imp_line, implementation = get_block(lines, args.imarker)
16          proof_line, proof = get_block(lines, args.pmarker)
17  
18      basename = os.path.splitext(os.path.basename(fn))[0]
19      header = os.path.join(args.destdir, basename + '.h')
20      guard = 'HD2E_%s' % basename.upper()
21      if not args.proof_only:
22          with open(header, 'w') as f:
23              print('#ifndef %s' % guard, file=f)
24              print('#define %s' % guard, file=f)
25              for line in implementation:
26                  print(line, file=f)
27              print('#endif', file=f)
28  
29      proof_cc = os.path.join(args.destdir, basename + '.cc')
30      if not args.header_only:
31          with open(proof_cc, 'w') as f:
32              print('#include "proof_common.h"', file=f)
33              print('#line %d "%s"' % (imp_line+1, fn), file=f)
34              for line in implementation:
35                  print(line, file=f)
36              print('#line %d "%s"' % (proof_line+1, fn), file=f)
37              for line in proof:
38                  print(line, file=f)
39  
40  parser = argparse.ArgumentParser()
41  parser.add_argument("--imarker", help="marker for implementation",
42      default="Implementation")
43  parser.add_argument("--pmarker", help="marker for proof", default="Proof")
44  parser.add_argument("--destdir", help="destination directory")
45  parser.add_argument("--proof-only", help="only create proof program", action='store_true')
46  parser.add_argument("--header-only", help="only create header", action='store_true')
47  parser.add_argument("filename", nargs="+")
48  args = parser.parse_args()
49  
50  try:
51      os.makedirs(args.destdir)
52  except os.error:
53      pass
54  
55  
56  for fn in args.filename: convert(fn, args)