#!/usr/bin/env python3

# 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, "rb")
  outp = open(root + ext, "wb")

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