"""Split a generated pool into easy (automation closes it at the root) and hard."""
import json, sys, threading
from rocq_env import Coqtop, Goal
import gen_problems, htps
src, easy_out, hard_out = sys.argv[1:4]
probs = [json.loads(l) for l in open(src)]
todo, lock, res = list(probs), threading.Lock(), {}
def w():
    c = Coqtop(gen_problems.PRELUDE, gen_problems.AMBIENT, tac_timeout=2)
    while True:
        with lock:
            if not todo: return
            p = todo.pop()
        g = Goal([], p["stmt"])
        solved = any(c.apply(g, t) == ("ok", []) for t in ["intros; " + x for x in htps.closers_for(g, list(gen_problems.DEFS))])
        with lock: res[p["id"]] = solved
ts = [threading.Thread(target=w) for _ in range(7)]
[t.start() for t in ts]; [t.join() for t in ts]
with open(easy_out, "w") as e, open(hard_out, "w") as h:
    for p in probs: (e if res[p["id"]] else h).write(json.dumps(p) + "\n")
print("easy", sum(res.values()), "hard", len(res) - sum(res.values()))