<commit_before>// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at  9:18:39 PST by lamport
//      modified on Tue Jan  2 11:40:25 PST 2001 by yuanyu

package tlc2.module;

import tlc2.output.EC;
import tlc2.tool.EvalControl;
import tlc2.tool.EvalException;
import tlc2.tool.TLARegistry;
import tlc2.util.Vect;
import tlc2.value.Applicable;
import tlc2.value.BoolValue;
import tlc2.value.FcnRcdValue;
import tlc2.value.IntValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
import tlc2.value.ValueConstants;
import tlc2.value.ValueVec;

public class Bags implements ValueConstants
{

    static
    {
        TLARegistry.put("BagCup", "\\oplus");
        TLARegistry.put("BagDiff", "\\ominus");
        TLARegistry.put("SqSubseteq", "\\sqsubseteq");
    }

    public static Value EmptyBag()
    {
        return EmptyFcn;
    }

    public static BoolValue IsABag(Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        if (fcn == null)
        {
            throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "IsBag",
                    "a function with a finite domain", Value.ppr(b.toString()) });
        }
        Value[] vals = fcn.values;
        for (int i = 0; i < vals.length; i++)
        {
            if (!(vals[i] instanceof IntValue) || ((IntValue) vals[i]).val < 0)
            {
                return ValFalse;
            }
        }
        return ValTrue;
    }

    public static IntValue BagCardinality(Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        if (fcn == null)
        {
            throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality",
                    "a function with a finite domain", Value.ppr(b.toString()) });
        }
        int num = 0;
        Value[] vals = fcn.values;
        for (int i = 0; i < vals.length; i++)
        {
            if (vals[i] instanceof IntValue)
            {
                int cnt = ((IntValue) vals[i]).val;
                if (cnt > 0)
                {
                    num += ((IntValue) vals[i]).val;
                } else
                {
                    new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality", "a bag",
                            Value.ppr(b.toString()) });
                }
            } else
            {
                new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality", "a bag",
                        Value.ppr(b.toString()) });
            }
        }
        return IntValue.gen(num);
    }

    public static BoolValue BagIn(Value e, Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        Value[] domain = fcn.domain;<commit_msg>Actually throw the exception if the bag cardinality is incorrect.<commit_after>// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at  9:18:39 PST by lamport
//      modified on Tue Jan  2 11:40:25 PST 2001 by yuanyu

package tlc2.module;

import tlc2.output.EC;
import tlc2.tool.EvalControl;
import tlc2.tool.EvalException;
import tlc2.tool.TLARegistry;
import tlc2.util.Vect;
import tlc2.value.Applicable;
import tlc2.value.BoolValue;
import tlc2.value.FcnRcdValue;
import tlc2.value.IntValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
import tlc2.value.ValueConstants;
import tlc2.value.ValueVec;

public class Bags implements ValueConstants
{

    static
    {
        TLARegistry.put("BagCup", "\\oplus");
        TLARegistry.put("BagDiff", "\\ominus");
        TLARegistry.put("SqSubseteq", "\\sqsubseteq");
    }

    public static Value EmptyBag()
    {
        return EmptyFcn;
    }

    public static BoolValue IsABag(Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        if (fcn == null)
        {
            throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "IsBag",
                    "a function with a finite domain", Value.ppr(b.toString()) });
        }
        Value[] vals = fcn.values;
        for (int i = 0; i < vals.length; i++)
        {
            if (!(vals[i] instanceof IntValue) || ((IntValue) vals[i]).val < 0)
            {
                return ValFalse;
            }
        }
        return ValTrue;
    }

    public static IntValue BagCardinality(Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        if (fcn == null)
        {
            throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality",
                    "a function with a finite domain", Value.ppr(b.toString()) });
        }
        int num = 0;
        Value[] vals = fcn.values;
        for (int i = 0; i < vals.length; i++)
        {
            if (vals[i] instanceof IntValue)
            {
                int cnt = ((IntValue) vals[i]).val;
                if (cnt > 0)
                {
                    num += ((IntValue) vals[i]).val;
                } else
                {
                    throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality", "a bag",
                            Value.ppr(b.toString()) });
                }
            } else
            {
            	throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagCardinality", "a bag",
                        Value.ppr(b.toString()) });
            }
        }
        return IntValue.gen(num);
    }

    public static BoolValue BagIn(Value e, Value b)
    {
        FcnRcdValue fcn = FcnRcdValue.convert(b);
        Value[] domain = fcn.domain;
{'fraction_non_alphanumeric': 0.11179592535524739, 'fraction_numerical': 0.016777948981338813, 'mean_word_length': 1.9180819180819182, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 5, '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': '3379549', 'n_tokens_mistral': 1949, 'n_tokens_neox': 1829, 'n_words': 440}