<commit_before>#! /usr/bin/env python

##################################################################################
#
#   The Reverse Mathematics Zoo Updater
#   by <NAME>
#   - Version 1.0 started August, 2010
#   - Version 2.0 started August, 2013
#   Revised by <NAME>
#   - Version 3.0 - 29 May 2016
#   - Version 4.0 - started 30 May 2016
#   Documentation and support: http://rmzoo.uconn.edu
#
##################################################################################

from __future__ import print_function

import sys
import time
from codecs import open
from collections import defaultdict

if sys.version_info < (3,):
    import cPickle as pickle
else:
    import pickle

def eprint(*args, **kwargs):
    print(*args, file=sys.stderr, **kwargs)

Error = False
def warning(s):
    global Error
    Error = True
    eprint(s)

def error(s):    # Throw exception
    raise Exception(s)

Date = '30 May 2016'
Version = '4.0'

from rmBitmasks import *

implies = defaultdict(noReduction)
notImplies = defaultdict(noReduction)

def addReduction(a,reduction,b):
    implies[(a,b)] |= Reduction.weaker(reduction)

def addNonReduction(a,reduction,b):
    notImplies[(a,b)] |= Reduction.stronger(reduction)

conservative = defaultdict(noForm)
nonConservative = defaultdict(noForm)

def addConservative(a,frm,b):
    conservative[(a,b)] |= Form.weaker(frm)

def addNonConservative(a,frm,b):
    nonConservative[(a,b)] |= Form.stronger(frm)

form = defaultdict(noForm)

primary = set()
primaryIndex = []

justify = {}

justMarker = '*@'
def indentJust(jst):
    return jst.replace('*@','*@@')

def justReference(a, op, b):
    return justMarker + '{0} {1} {2}: '.format(a, printOp(op), b) + indentJust(justify[(a,op,b)])

def printJust(a):
    a = a.replace('@','    ')
    a = a.replace('*','\n')
    return a

principles = set(['RCA'])

def addPrinciple(a):
    setA = set(a.split('+'))
    a = '+'.join(sorted(setA))
    principles.add(a)
    principles.update(setA)
    return a

def printOp(op):
    if op[1] == 'nc':
        return 'n{0}c'.format(op[0])
    else:
        return '{0}{1}'.format(*op)

def addUnjustified(a, op, b):
    error('The fact "{0} {1} {2}" is not justified.'.format(a, printOp(op), b))

def addJustification(a, op, b, jst):
    if (a, op, b) not in justify:
        justify[(a, op, b)] = jst

def addFact(a, op, b, jst):
    addJustification(a, op, b, jst)
    justRef = justMarker + u'{0} {1} {2}: {3}'.format(a, printOp(op), b, justify[(a, op, b)])
    
    if op[1] == '->': # reduction
        r = Reduction.fromString(op[0])
        if Reduction.isPresent(r, implies[(a,b)]):
            return
        addReduction(a, r, b)
        for x in Reduction.iterate(Reduction.weaker(r)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, notImplies[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}-> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'->'),b)]) + '\n\n' + 
                        '{0} {1}-|> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'-|>'),b)]))
    elif op[1] == '-|>': # non-reduction
        r = Reduction.fromString(op[0])
        if Reduction.isPresent(r, notImplies[(a,b)]):
            return
        addNonReduction(a, r, b)
        for x in Reduction.iterate(Reduction.stronger(r)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, implies[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}-> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'->'),b)]) + '\n\n' + 
                        '{0} {1}-|> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'-|>'),b)]))
    elif op[1] == '<->': # equivalence
        r = Reduction.fromString(op[0])
        if not Reduction.isPresent(r, implies[(a,b)]):
            addFact(a, (op[0], '->'), b, justRef)
        if not Reduction.isPresent(r, implies[(b,a)]):
            addFact(b, (op[0], '->'), a, justRef)
    elif op[1] == 'c': # conservation
        frm = Form.fromString(op[0])
        if Form.isPresent(frm, conservative[(a,b)]):
            return
        addConservative(a, frm, b)
        for x in Form.iterate(Form.weaker(frm)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, nonConservative[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'c'),b)]) + '\n\n' + 
                        '{0} n{1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'nc'),b)]))
    elif op[1] == 'nc': # non-conservation
        frm = Form.fromString(op[0])
        if Form.isPresent(frm, nonConservative[(a,b)]):
            return
        addNonConservative(a, frm, b)
        for x in Form.iterate(Form.stronger(frm)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, conservative[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'c'),b)]) + '\n\n' + 
                        '{0} n{1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'nc'),b)]))
    else:
        error('Unrecognized operator {0}'.format(op))

def addForm(a, frm):
    form[a] |= Form.weaker(frm)

def addPrimary(a):
    primary.add(a)
    primaryIndex.append(a)

from pyparsing import *
def parseDatabase(databaseString):
    start = time.clock()
    eprint('Parsing database...')
    # Name parsed strings
    name = Word( alphas+"_+^{}\\$", alphanums+"_+^{}$\\").setParseAction(lambda s,l,t: addPrinciple(t[0]))

    parenth = Literal('"')
    justification = QuotedString('"""',multiline=True) | quotedString.setParseAction(removeQuotes)

    _reductionName = NoMatch()
    for r in Reduction:
        if r != Reduction.none:
            _reductionName |= Literal(r.name)
    reductionName = Optional(_reductionName, default=Reduction.RCA.name)

    reduction = (reductionName + Literal("->")) | (Literal("<=") + Optional(Suppress(Literal("_")) + _reductionName, default=Reduction.RCA.name)).setParseAction(lambda s,l,t: [t[1], "->"])
    nonReduction = reductionName + Literal("-|>")
    equivalence = reductionName + Literal("<->")<commit_msg>Fixed an rmupdater.py logic bug!<commit_after>#! /usr/bin/env python

##################################################################################
#
#   The Reverse Mathematics Zoo Updater
#   by <NAME>
#   - Version 1.0 started August, 2010
#   - Version 2.0 started August, 2013
#   Revised by <NAME>
#   - Version 3.0 - 29 May 2016
#   - Version 4.0 - started 30 May 2016
#   Documentation and support: http://rmzoo.uconn.edu
#
##################################################################################

from __future__ import print_function

import sys
import time
from codecs import open
from collections import defaultdict

if sys.version_info < (3,):
    import cPickle as pickle
else:
    import pickle

def eprint(*args, **kwargs):
    print(*args, file=sys.stderr, **kwargs)

Error = False
def warning(s):
    global Error
    Error = True
    eprint(s)

def error(s):    # Throw exception
    raise Exception(s)

Date = '30 May 2016'
Version = '4.0'

from rmBitmasks import *

implies = defaultdict(noReduction)
notImplies = defaultdict(noReduction)

def addReduction(a,reduction,b):
    implies[(a,b)] |= Reduction.weaker(reduction)

def addNonReduction(a,reduction,b):
    notImplies[(a,b)] |= Reduction.stronger(reduction)

conservative = defaultdict(noForm)
nonConservative = defaultdict(noForm)

def addConservative(a,frm,b):
    conservative[(a,b)] |= Form.weaker(frm)

def addNonConservative(a,frm,b):
    nonConservative[(a,b)] |= Form.stronger(frm)

form = defaultdict(noForm)

primary = set()
primaryIndex = []

justify = {}

justMarker = '*@'
def indentJust(jst):
    return jst.replace('*@','*@@')

def justReference(a, op, b):
    return justMarker + '{0} {1} {2}: '.format(a, printOp(op), b) + indentJust(justify[(a,op,b)])

def printJust(a):
    a = a.replace('@','    ')
    a = a.replace('*','\n')
    return a

principles = set(['RCA'])

def addPrinciple(a):
    setA = set(a.split('+'))
    a = '+'.join(sorted(setA))
    principles.add(a)
    principles.update(setA)
    return a

def printOp(op):
    if op[1] == 'nc':
        return 'n{0}c'.format(op[0])
    else:
        return '{0}{1}'.format(*op)

def addUnjustified(a, op, b):
    error('The fact "{0} {1} {2}" is not justified.'.format(a, printOp(op), b))

def addJustification(a, op, b, jst):
    if (a, op, b) not in justify:
        justify[(a, op, b)] = jst

def addFact(a, op, b, jst):
    addJustification(a, op, b, jst)
    justRef = justMarker + u'{0} {1} {2}: {3}'.format(a, printOp(op), b, justify[(a, op, b)])
    
    if op[1] == '->': # reduction
        r = Reduction.fromString(op[0])
        if Reduction.isPresent(r, implies[(a,b)]):
            return
        addReduction(a, r, b)
        for x in Reduction.iterate(Reduction.weaker(r)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, notImplies[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}-> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'->'),b)]) + '\n\n' + 
                        '{0} {1}-|> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'-|>'),b)]))
    elif op[1] == '-|>': # non-reduction
        r = Reduction.fromString(op[0])
        if Reduction.isPresent(r, notImplies[(a,b)]):
            return
        addNonReduction(a, r, b)
        for x in Reduction.iterate(Reduction.stronger(r)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, implies[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}-> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'->'),b)]) + '\n\n' + 
                        '{0} {1}-|> {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'-|>'),b)]))
    elif op[1] == '<->': # equivalence
        r = Reduction.fromString(op[0])
        if not Reduction.isPresent(r, implies[(a,b)]):
            addFact(a, (op[0], '->'), b, justRef)
        if not Reduction.isPresent(r, implies[(b,a)]):
            addFact(b, (op[0], '->'), a, justRef)
    elif op[1] == 'c': # conservation
        frm = Form.fromString(op[0])
        if Form.isPresent(frm, conservative[(a,b)]):
            return
        addConservative(a, frm, b)
        for x in Form.iterate(Form.weaker(frm)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, nonConservative[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'c'),b)]) + '\n\n' + 
                        '{0} n{1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'nc'),b)]))
    elif op[1] == 'nc': # non-conservation
        frm = Form.fromString(op[0])
        if Form.isPresent(frm, nonConservative[(a,b)]):
            return
        addNonConservative(a, frm, b)
        for x in Form.iterate(Form.stronger(frm)):
            addJustification(a, (x.name, op[1]), b, justRef)
            if Reduction.isPresent(x, conservative[(a,b)]):
                error('The following facts are contradictory.\n\n' + 
                        '{0} {1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'c'),b)]) + '\n\n' + 
                        '{0} n{1}c {2}: '.format(a, x.name, b) + printJust(justify[(a,(x.name,'nc'),b)]))
    else:
        error('Unrecognized operator {0}'.format(op))

def addForm(a, frm):
    form[a] |= Form.stronger(frm)

def addPrimary(a):
    primary.add(a)
    primaryIndex.append(a)

from pyparsing import *
def parseDatabase(databaseString):
    start = time.clock()
    eprint('Parsing database...')
    # Name parsed strings
    name = Word( alphas+"_+^{}\\$", alphanums+"_+^{}$\\").setParseAction(lambda s,l,t: addPrinciple(t[0]))

    parenth = Literal('"')
    justification = QuotedString('"""',multiline=True) | quotedString.setParseAction(removeQuotes)

    _reductionName = NoMatch()
    for r in Reduction:
        if r != Reduction.none:
            _reductionName |= Literal(r.name)
    reductionName = Optional(_reductionName, default=Reduction.RCA.name)

    reduction = (reductionName + Literal("->")) | (Literal("<=") + Optional(Suppress(Literal("_")) + _reductionName, default=Reduction.RCA.name)).setParseAction(lambda s,l,t: [t[1], "->"])
    nonReduction = reductionName + Literal("-|>")
    equivalence = reductionName + Literal("<->")
{'fraction_non_alphanumeric': 0.20891601637951016, 'fraction_numerical': 0.014679749671637179, 'mean_word_length': 2.946341463414634, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3250032', 'n_tokens_mistral': 4692, 'n_tokens_neox': 4506, 'n_words': 975}