<commit_before>from stew.core import Sort, generator, operation
from stew.matching import var

from nat import Nat
from bool import Bool


class Z(Sort):
    def __init__(self, *args, **kwargs):
        if (len(args) == 1) and isinstance(args[0], int):
            number = args[0]

            Sort.__init__(self)
            if number == 0:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat.zero(), 'neg': Nat.zero()}
            elif number > 0:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat(number), 'neg': Nat.zero()}
            else:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat.zero(), 'neg': Nat(-number)}

        else:
            Sort.__init__(self, **kwargs)

    @generator
    def zero() -> Z: pass

    @generator
    def cons(pos: Nat, neg: Nat) -> Z: pass

    @operation
    def __add__(self: Z, other: Z) -> Z:
        self._generator_args['pos'] += other._generator_args['pos']
        self._generator_args['neg'] += other._generator_args['neg']
        self.normalize()
        return self

    @operation
    def __eq__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] == y['pos'] and x['neg'] == y['neg']:
            return Bool.true()
        return Bool.false()

    @operation
    def __gt__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] > y['pos']:
            return Bool.true()
        elif x['neg'] < y['neg']:
            return Bool.true()
        else:
            return Bool.false()

    @operation
    def __lt__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] < y['pos']:
            return Bool.true()
        elif x['neg'] > y['neg']:
            return Bool.true()
        else:
            return Bool.false()

    @operation
    def normalize(self: Z) -> Z:

        if self._generator_args['pos'] == self._generator_args['neg']:
            self = Z.zero()

        elif self._generator_args['pos'] > self._generator_args['neg']:
            x = self._generator_args['pos']
            y = self._generator_args['neg']
            self._generator_args['pos'] = x - y
            self._generator_args['neg'] = Nat.zero()

        elif self._generator_args['neg'] > self._generator_args['pos']:
            x = self._generator_args['pos']
            y = self._generator_args['neg']
            self._generator_args['pos'] = Nat.zero()
            self._generator_args['neg'] = y - x

        return self

    def __str__(self):
        x = self._generator_args['pos']
        y = self._generator_args['neg']
        if x >= y:
            return '%s(%s)' % (self.__class__.__name__, x)
        else:
            return '%s(-%s)' % (self.__class__.__name__, y)<commit_msg>correction of __add__ and normalize()<commit_after>from stew.core import Sort, generator, operation
from stew.matching import var

from nat import Nat
from bool import Bool


class Z(Sort):
    def __init__(self, *args, **kwargs):
        if (len(args) == 1) and isinstance(args[0], int):
            number = args[0]

            Sort.__init__(self)
            if number == 0:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat.zero(), 'neg': Nat.zero()}
            elif number > 0:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat(number), 'neg': Nat.zero()}
            else:
                self._generator = Z.cons
                self._generator_args = {'pos': Nat.zero(), 'neg': Nat(-number)}

        else:
            Sort.__init__(self, **kwargs)

    @generator
    def zero() -> Z: pass

    @generator
    def cons(pos: Nat, neg: Nat) -> Z: pass

    @operation
    def __add__(self: Z, other: Z) -> Z:
        x = self._generator_args['pos'] + other._generator_args['pos']
        y = self._generator_args['neg'] + other._generator_args['neg']
        z = Z.cons(pos=x, neg=y)
        z.normalize()
        return z

    @operation
    def __eq__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] == y['pos'] and x['neg'] == y['neg']:
            return Bool.true()
        return Bool.false()

    @operation
    def __gt__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] > y['pos']:
            return Bool.true()
        elif x['neg'] < y['neg']:
            return Bool.true()
        else:
            return Bool.false()

    @operation
    def __lt__(self: Z, other: Z) -> Z:
        x = self._generator_args
        y = other._generator_args
        if x['pos'] < y['pos']:
            return Bool.true()
        elif x['neg'] > y['neg']:
            return Bool.true()
        else:
            return Bool.false()

    @operation
    def normalize(self: Z) -> Z:

        x = self._generator_args['pos']
        y = self._generator_args['neg']

        # if self.x == 0 or self.y == 0
        if x == Nat.zero() or y == Nat.zero():
            return self

        # else we reduce
        elif x == Nat.suc(var.xx) and y == Nat.suc(var.yy):
            self._generator_args['pos'] = var.xx
            self._generator_args['neg'] = var.yy
            return self.normalize()

    def __str__(self):
        x = self._generator_args['pos']
        y = self._generator_args['neg']
        if x >= y:
            return '%s(%s)' % (self.__class__.__name__, x)
        else:
            return '%s(-%s)' % (self.__class__.__name__, y)
{'fraction_non_alphanumeric': 0.14696093886845332, 'fraction_numerical': 0.0021019442984760903, 'mean_word_length': 1.8309370352007932, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 27, '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': '1015290', 'n_tokens_mistral': 1767, 'n_tokens_neox': 1691, 'n_words': 438}