#!/usr/bin/env python2.7

# Reduces a file "X_master.lean" into "X.lean".
# The script searches for sections of the form
# --quo [Y]
#   [Z]
# --ouq
#
# For each of these sections, the first and the 
# last line get removed.

import os
import sys

def make_demo(name):
  (root, ext) = os.path.splitext(name)
  if root.endswith("_master"):
    root = root[:-7]
  else:
    raise Exception('Filename needs to end with "_master".')
  inp = open(name)
  outp = open(root + ext, "w")

  in_fails = False
  in_quo = False
  line_number = 1
  for l in inp:
    if l.startswith("/-fails"):
      if in_fails:
        print("WARNING: missing sliaf-/ on line {0}".format(line_number))
      else:
        in_fails = True
    elif l.startswith("sliaf-/"):
      if not in_fails:
        print("WARNING: missing /-fails on line {0}".format(line_number))
      else:
        in_fails = False
    elif l.startswith("--quo ") or l.rstrip("\n\r") == "--quo":
      if in_quo:
        print("WARNING: missing --ouq on line {0}".format(line_number))
      else:
        in_quo = True
    elif l.startswith("--ouq"):
      if not in_quo:
        print("WARNING: missing --quo on line {0}".format(line_number))
      else:
        in_quo = False
    elif l.rstrip("\n\r") == ":=":
      outp.seek(-1, os.SEEK_CUR)
      outp.write(" :=\n")
    elif l.startswith("import "):
      outp.write(
        l.replace("demo_master", "demo")
         .replace("exercise", "exercise_sheet")
         .replace("homework", "homework_sheet")
        )
    else:
      outp.write(l)
    line_number += 1

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