"""CoqHammer on the eight held-out tasks (statements only; symbolic, no model)."""
import json, os, re, sys
sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..', 'pilot'))
import importlib.util
spec = importlib.util.spec_from_file_location('pilot', os.path.join(os.path.dirname(__file__), '..', 'pilot', 'pilot.py'))
pilot = importlib.util.module_from_spec(spec); spec.loader.exec_module(pilot)
import hammer_eval as H
UNF = "unfold MP001, MP002, MP003, MP008, OP001, OP006, SP001, OfItself, ThroughAnother, Necessary, Possible, InUniverse, DependsOn in *"
HEAD = pilot.PREAMBLE.replace("From Stdlib Require Import Classical Relations.", "From Stdlib Require Import Classical Relations.\nFrom Hammer Require Import Hammer Tactics.") + "\nSet Hammer ATPLimit 60.\nSet Hammer ReconstrLimit 30.\n"
def f(stmt, tac, check=False):
    return f"{HEAD}\nTheorem problem : {stmt}.\nProof.\n{tac}\nQed.\nEnd Pilot.\n" + ("Print Assumptions problem.\n" if check else "")
ATT = [("hammer", "intros; hammer."), ("hammer+unfold", f"{UNF}; intros; hammer."), ("hammer+classical", f"{UNF}; intros; apply NNPP; intro; hammer.")]
out = open('results/hammer_heldout.jsonl', 'w')
for k, stmt in pilot.TASKS.items():
    res = 'not proved'
    for name, tac in ATT:
        code, o = H.compile_(f(stmt, tac), timeout=300)
        if code == 0:
            m = re.search(r'Replace the hammer tactic with:\s*(.+?)\s*$', o, re.M)
            if not m: continue
            final = tac.replace('hammer.', m.group(1).strip().rstrip('.') + '.')
            c2, o2 = H.compile_(f(stmt, final, True), timeout=300)
            if c2 == 0: res = name; out.write(json.dumps({'id': k, 'method': name, 'script': final, 'check': o2[-300:]}) + '\n'); break
    if res == 'not proved': out.write(json.dumps({'id': k, 'method': None}) + '\n')
    out.flush(); print(k, res, flush=True)