postprocess.py

import os
import lmdb
from progressbar import ProgressBar
import json
from glob import glob
import pdb


def merge_lmdbs():
    "merge all the LMDB databases in data/ into one"
    db_path = "sexp_cache"
    dst_db = lmdb.open(db_path, map_size=1e11, writemap=True, readahead=False)
    files = glob("data/**/*sexp_cache", recursive=True)

    bar = ProgressBar(max_value=len(files))
    for i, db_path in enumerate(files):
        print(db_path)
        try:
            src_db = lmdb.open(
                db_path, map_size=1e11, readonly=True, readahead=True, lock=False
            )
        except lmdb.Error as ex:
            print(ex)
            continue
        with src_db.begin() as txn1:
            cursor = txn1.cursor()
            for key, value in cursor:
                with dst_db.begin(write=True) as txn2:
                    txn2.put(key, value, dupdata=False, overwrite=False)
        src_db.close()
        os.system('rm -r "%s"' % db_path)
        bar.update(i)

    dst_db.close()


def env_diff(new_env, old_env):
    add = {
        "constants": [
            json.loads(const)
            for const in new_env["constants"]
            if const not in old_env["constants"]
        ],
        "inductives": [
            json.loads(induct)
            for induct in new_env["inductives"]
            if induct not in old_env["inductives"]
        ],
    }
    subtract = {
        "constants": [
            json.loads(const)
            for const in old_env["constants"]
            if const not in new_env["constants"]
        ],
        "inductives": [
            json.loads(induct)
            for induct in old_env["inductives"]
            if induct not in new_env["inductives"]
        ],
    }
    env_delta = {"add": add, "subtract": subtract}
    return env_delta


def merge_proofs():
    files = [f for f in glob("data/**/*.json", recursive=True) if "PROOFS" not in f]

    bar = ProgressBar(max_value=len(files))
    for i, f in enumerate(files):
        file_data = json.load(open(f))
        proofs = []
        env = {"constants": [], "inductives": []}

        # merge the files for the human proofs
        for proof_name in file_data["proofs"]:
            proof_file = f[:-5] + "-PROOFS/" + proof_name + ".json"
            if not os.path.exists(proof_file):
                continue
            proof_data = json.load(open(proof_file))
            for j, const in enumerate(proof_data["env"]["constants"]):
                proof_data["env"]["constants"][j] = json.dumps(
                    proof_data["env"]["constants"][j]
                )
            for j, const in enumerate(proof_data["env"]["inductives"]):
                proof_data["env"]["inductives"][j] = json.dumps(
                    proof_data["env"]["inductives"][j]
                )

            env_delta = env_diff(proof_data["env"], env)
            env = proof_data["env"]

            proofs.append(
                {
                    "name": proof_name,
                    "line_nb": proof_data["line_nb"],
                    "env_delta": env_delta,
                    "steps": proof_data["steps"],
                    "goals": proof_data["goals"],
                    "proof_tree": proof_data["proof_tree"],
                }
            )

        # merge the synthetic proofs
        synthetic_proofs = {}
        for sf in glob(f[:-5] + "-SUBPROOFS/*.json"):
            proof_name = sf.split("/")[-1][:-5]
            subprf_data = json.load(open(sf))
            synthetic_proofs[proof_name] = subprf_data

        file_data["proofs"] = proofs
        file_data["synthetic_proofs"] = synthetic_proofs
        if proofs != []:
            json.dump(file_data, open(f, "wt"))
        os.system("rm -r " + f[:-5] + "-*PROOFS")

        bar.update(i)


def merge_synthetic_proofs():
    dirnames = glob("data/**/*-SUBPROOFS", recursive=True)

    bar = ProgressBar(max_value=len(dirnames))
    for i, d in enumerate(dirnames):
        filename = d[:-10] + ".json"
        if not os.path.exists(filename):
            continue
        file_data = json.load(open(filename))
        file_data["synthetic_proofs"] = {}
        for f in glob(os.path.join(d, "*.json")):
            proof_name = f.split("/")[-1][:-5]
            subprf_data = json.load(open(f))
            file_data["synthetic_proofs"][proof_name] = subprf_data
        json.dump(file_data, open(filename, "wt"))
        os.system("rm %s/*.json" % d)
        bar.update(i)


if __name__ == "__main__":
    print("merging the LMDB files..")
    merge_lmdbs()
    print("merging the proof files..")
    merge_proofs()