"""Check that the served drawings encode the certified runs, then build the Lean certificates and record axioms.
The theorem does not cover the browser's canvas drawing.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
"""
import argparse
import importlib.util
import json
import re
import subprocess
import sys
from collections import Counter
from pathlib import Path

HERE = Path(__file__).resolve().parent
GRAPHICS = HERE.parent
DIST = HERE.parents[1] / 'dist'
KERNEL_ONLY = ['Growth.Run.reached', 'Growth.tiny_valid', 'Growth.notTight_rejected', 'Growth.overBudget_rejected',
               'Growth.heldTwice_rejected', 'Growth.overlong_rejected', 'Growth.misplacedMeeting_rejected', 'Growth.offSlot_rejected']
KINDS = {'laK7-n': 'points', 'laK7-r': 'origins', 'laK7-g': 'crossings', 'laK7-e': 'branches', 'laK7-b': 'meetings'}


def classes(cls, prefix):
    found = re.findall(prefix + r'(\d+)', cls)
    return int(found[0]) if found else None


def parse_markup(html):
    """Multisets of drawn dots (point, start, tone, fade) and link halves (segment, start, span, fade) per kind."""
    drawn = {kind: Counter() for kind in KINDS.values()}
    for cls, d in re.findall(r'<path class="(laK7-[^"]*)" d="([^"]*)"', html):
        kind, start, fade = KINDS[cls.split()[0]], classes(cls, 'laK7-o'), classes(cls, 'laK7-x')
        if kind in ('points', 'origins'):
            for x, y in re.findall(r'M(-?\d+),(-?\d+)h0', d):
                drawn[kind][((int(x), int(y)), start, classes(cls, 'laK7-t'), fade)] += 1
        else:
            (x1, y1, x2, y2), = re.findall(r'^M(-?\d+),(-?\d+)L(-?\d+),(-?\d+)$', d)
            drawn[kind][(((int(x1), int(y1)), (int(x2), int(y2))), start, classes(cls, 'laK7-d'), fade)] += 1
    return drawn


def expected(data, tones, along):
    """The same multisets derived from certified data: a half starts at its claim's step and is drawn until its
    doubled end; an unconnected tree's drawing starts fading `hold` after its end."""
    pts, pace = [tuple(p) for p in data['points']], data['pace']
    claims, trees = data['claims'], data['trees']
    weight = {}
    for a, b, w in data['edges']:
        weight[(a, b)] = weight[(b, a)] = w
    fade = lambda t: None if trees[t][2] is None else (trees[t][2] + data['hold']) // pace
    drawn = {kind: Counter() for kind in KINDS.values()}
    for i, (v, t, d, p) in enumerate(claims):
        origin = p == i
        drawn['origins' if origin else 'points'][(pts[v], d // pace, None if origin else tones[v], fade(t))] += 1
    for c, y, end2, kind in data['halves']:
        v, t, d, _ = claims[c]
        if end2 > 2 * d:
            segment = (pts[v], along(pts[v], pts[y], d, weight[(v, y)], end2))
            drawn[['crossings', 'branches', 'meetings'][kind]][(segment, d // pace, end2 // (2 * pace) - d // pace, fade(t))] += 1
    return drawn


def network(data):
    """Every point ends held by a tree whose wave met another's."""
    final = {}
    for v, t, _, _ in data['claims']:
        final[v] = t
    return len(final) == len(data['points']) and all(data['trees'][t][3] is not None for t in final.values())


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--source-only', action='store_true', help='Check the render sources and Lean project without the built pages; print the report without replacing it.')
    args = parser.parse_args()
    spec = importlib.util.spec_from_file_location('home_art_source', GRAPHICS / 'build-home-art.py')
    module = importlib.util.module_from_spec(spec)
    spec.loader.exec_module(module)
    report = {'scope': 'certified runs and their served drawings; no proof of canvas pixels', 'runs': {}, 'lean': {}}
    for name, run in module.RUNS.items():
        data = json.loads((HERE / 'runs' / f'run-{name}.json').read_text())
        assert module.lean_source(name, data) == (HERE / 'Growth' / f'Run{name.upper()}.lean').read_text(), (name, 'JSON data differs from Lean certificate input')
        tones = {i: p[2] for i, p in enumerate(module.field(module.random.Random(7000 + run)))}
        exp = expected(data, tones, module.along)
        assert parse_markup((GRAPHICS / 'components' / f'home-art-{name}.html').read_text()) == exp, (name, 'component differs from certified data')
        assert network(data), (name, 'final field is not one connected network')
        if not args.source_only:
            page = 'index.html' if name == 'a' else f'index-{name}.html'
            html = (DIST / page).read_text()
            assert '<template id="study">' in html and 'laK7-video' not in html, (page, 'template missing or recorded media present')
            assert parse_markup(html) == exp, (page, 'served drawing differs from certified data')
        trees = data['trees']
        report['runs'][name] = {'points': len(data['points']), 'links': len(data['edges']), 'origins': len(trees),
                                'connected': sum(t[3] is not None for t in trees), 'faded': sum(t[2] is not None for t in trees),
                                'claims': len(data['claims']), 'halves': len(data['halves']), 'meetings': len(data['meetings']),
                                'seeds': [data['seed'], data['origin_seed']], 'drawing_matches_certified_data': True, 'ends_as_one_network': True}
    build = subprocess.run(['lake', 'build'], cwd=HERE, capture_output=True, text=True, check=False)
    assert build.returncode == 0, build.stdout + build.stderr
    axioms = subprocess.run(['lake', 'env', 'lean', 'Growth/Axioms.lean'], cwd=HERE, capture_output=True, text=True, check=False)
    assert axioms.returncode == 0, axioms.stdout + axioms.stderr
    for entry in re.split(r"\n(?=')", axioms.stdout.strip()):
        theorem = entry.split("'")[1]
        deps = re.findall(r'\[(.*?)\]', entry.replace('\n', ' '))
        report['lean'][theorem] = [d.strip() for d in deps[0].split(',')] if deps else []
    for theorem in KERNEL_ONLY:
        assert not any('native_decide' in axiom or 'Classical' in axiom for axiom in report['lean'][theorem]), theorem
    report['lean_version'] = subprocess.run(['lean', '--version'], capture_output=True, text=True, check=True).stdout.strip()
    report['trusted'] = ['Lean kernel', 'Lean compiler for the native_decide instance checks (the per-theorem native_decide axioms listed above)',
                         'this source bridge', 'browser canvas drawing; measured separately, outside the proof']
    if args.source_only:
        print(json.dumps(report, indent=2))
        return
    (HERE / 'axioms.txt').write_text(axioms.stdout)
    (HERE / 'check-report.json').write_text(json.dumps(report, indent=2) + '\n')
    for name in ['axioms.txt', 'check-report.json']:
        (DIST / 'animation' / name).write_bytes((HERE / name).read_bytes())
    print(json.dumps({'runs': len(report['runs']), 'theorems': len(report['lean'])}))


if __name__ == '__main__':
    sys.exit(main())