#!/usr/bin/env python3

# Reduces a file "XMaster.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[:-6]
  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} of {1}" \
          .format(line_number, name))
      else:
        in_fails = True
        outp.write(b"/-\n")
    elif l.startswith(b"sliaf-/"):
      if not in_fails:
        print("WARNING: missing /-fails on line {0} of {1}" \
          .format(line_number, name))
      else:
        in_fails = False
        outp.write(b"-/\n")
    elif l.startswith(b"--quo ") or l.rstrip(b"\n\r") == b"--quo":
      if in_quo:
        print("WARNING: missing --ouq on line {0} of {1}" \
          .format(line_number, name))
      else:
        in_quo = True
    elif l.startswith(b"--ouq"):
      if not in_quo:
        print("WARNING: missing --quo on line {0} of {1}" \
          .format(line_number, name))
      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"_DemoMaster", b"_Demo")
         .replace(b"_Exercise", b"_ExerciseSheet")
        )
    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])
