#!/usr/bin/env python2.7

# Splits a file "X.lean" into "X_sheet.lean" and "X_solution.lean".
# The script searches for sections of the form
#
#     --sol [Y]
#     [Z]
#     --los
#
# For each of these sections, "X_sheet.lean" contains only [Y], whereas
# "X_solution.lean" contains only [Z].

import os
import sys

def split_lean(name):
  (root, ext) = os.path.splitext(name)
  inp = open(name)
  sheet = open(root + "_sheet" + ext, "w")
  solution = open(root + "_solution" + ext, "w")

  in_solution = False
  line_number = 1
  for l in inp:
    if l.startswith("--sol ") or l.rstrip("\n\r") == "--sol":
      if in_solution:
        print("Warning: missing --los on line {0} of {1}".format(line_number, name))
      else:
        in_solution = True
      sheet.write(l[6:])
    elif l.startswith("--los"):
      if not in_solution:
        print("Warning: missing --sol on line {0} of {1}".format(line_number, name))
      else:
        in_solution = False
    else:
      if not in_solution:
        sheet.write(l)
      solution.write(l)
    line_number += 1

if __name__ == "__main__":
    if len(sys.argv) <= 1 :
        print("Please provide the name of the file to process")
    else:
        split_lean(sys.argv[1])
