#! /usr/bin/env python3

from pathlib import Path
import sys, shutil, glob, distutils.dir_util

import regex
from fire import Fire
import toml

import jsonpickle


import lean_game_maker
from lean_game_maker.line_reader import FileReader
from lean_game_maker.objects import (HiddenBegin, HiddenEnd, SectionBegin,
    SectionEnd, SubSectionBegin, SubSectionEnd, TextBegin, TextEnd,
    DefinitionBegin, DefinitionEnd, 
    ExampleBegin, ExampleEnd,
    LemmaBegin, LemmaEnd,
    TheoremBegin, TheoremEnd,
    ProofBegin, ProofEnd,
    ProofComment)

from lean_game_maker.interactive_loader import interactive_server

module_path = Path(lean_game_maker.__file__).parent
interactive_path = module_path.parent / 'interactive_interface'

def render_lean_project(outdir=None, debug=False):
    try:
        leanpkg_toml = toml.load('leanpkg.toml')
    except FileNotFoundError:
        print("Couldn't find a leanpkg.toml, I give up.")
        sys.exit(1)
    toolchain = leanpkg_toml['package']['lean_version']
    lean_exec_path = Path.home() / '.elan/toolchains' / toolchain / 'bin/lean'
    paths = [str(lean_exec_path.parent / '../lib/lean/library'),
             str(Path.cwd() / 'src')]

    for dep, dep_info in leanpkg_toml.get('dependencies', []).items():
        if 'git' in dep_info:
            paths.append(str(Path('_target/deps') / dep / 'src'))
        else:
            paths.append(dep_info['path'])
    lean_path = ':'.join(paths)
    if debug:
        print("Lean executable path:", lean_exec_path)
        print("LEAN_PATH:", lean_path)

    
    

    outdir = outdir or 'html'
    Path(outdir).mkdir(exist_ok=True)


    s = interactive_server(interactive_path=interactive_path, paths=paths,
                    toolchain=toolchain, source_lib='.', outdir=outdir, debug=debug)
    s.copy_server()



    lecture_reader = FileReader([HiddenBegin, HiddenEnd,
#             SectionBegin, SectionEnd, 
#             SubSectionBegin, SubSectionEnd,
             TextBegin, TextEnd, 
#             DefinitionBegin, DefinitionEnd,
             ExampleBegin, ExampleEnd,
             LemmaBegin, LemmaEnd,
             TheoremBegin, TheoremEnd,
             ProofBegin, ProofEnd, ProofComment])
    
    
    level=1
    page=1
    game_data = []
    for level in range(1, 10):
        if not Path(f'src/game/level{level}').exists():
            break
        level_data = []
        for page in range(1, 10):
            lean_file = Path(f'src/game/level{level}/page{page}.lean')
            if not lean_file.exists():
                break
            print(f"level : {level}, page : {page}")
            lecture_reader.read_file(str(lean_file))
            page_data = { 'raw_text' : lecture_reader.raw_text, 'objects' : lecture_reader.output }
            page_data = jsonpickle.loads(jsonpickle.dumps(page_data, unpicklable=True))
            level_data.append(page_data)
            lecture_reader.hard_reset()
        game_data.append(level_data)

    with open(str(Path(outdir) / 'game_data.js'), 'w') as f:
        temp = jsonpickle.encode(game_data, unpicklable=False)
        f.write("game_data = " + temp)



if __name__ == '__main__':
    Fire(render_lean_project)
