#!/usr/bin/env python3
"""
Search a file containing a list of space separated (proof, term) entries, as
generated by dtrie.py, for comparison with proofs in a list of proofs, as
generated by pmsubtrees.py

This reports "DISCOVERY!" when a proof in the (proof, term) entries is found
to be smaller than the corresponding proof in the list of proofs.
"""

import dproof
import gzip
import sys

def main(args):
    pmsubtrees, proofs = args
    terms = {}
    with open(pmsubtrees) as f:
        for line in f:
            proof = line.rstrip("\n")
            term = dproof.check(proof)
            if term in terms:
                if len(proof) != len(terms[term][0]):
                    print(term, ":", terms[term][0], proof)
                    raise ValueError("different proof sizes")
            terms[term] = [proof, None]

    open_file = gzip.open if proofs.endswith(".gz") else open
    with open_file(proofs) as f:
        for line in f:
            if proofs.endswith(".gz"):
                line = line.decode("ascii")
            proof, term = line.rstrip("\n").split(" ", 1)
            if term in terms:
                if terms[term][1] is None:
                    terms[term][1] = proof
                elif len(proof) < len(terms[term][1]):
                    terms[term][1] = proof

    for (term, (o, n)) in terms.items():
        prefix = ""
        if (n is not None) and (len(n) < len(o)):
            prefix = "DISCOVERY! "
        print(prefix + "%s:%s %s" % (len(o), len(n or "") or "?", n or o))

if __name__ == "__main__":
    main(sys.argv[1:])
