private List getSimplificationRulesForType()

in meta/src/main/java/org/arend/lib/meta/simplify/Simplifier.java [150:205]


    private List<SimplificationRule> getSimplificationRulesForType(CoreExpression type) {
        var rules = new ArrayList<SimplificationRule>();
        type = type == null ? null : type.normalize(NormalizationMode.WHNF);
        var possibleClasses = new HashSet<>(Arrays.asList(ext.equationMeta.Monoid, ext.equationMeta.AddMonoid, ext.equationMeta.Semiring, ext.equationMeta.Ring, ext.equationMeta.AddGroup, ext.equationMeta.Group, ext.equationMeta.CGroup, ext.equationMeta.AbGroup));
        var instanceClassCallPair = Utils.findInstanceWithClassCall(new InstanceSearchParameters() {
            @Override
            public boolean testClass(@NotNull CoreClassDefinition classDefinition) {
                for (var clazz : possibleClasses) {
                    if (classDefinition.isSubClassOf(clazz)) {
                        return true;
                    }
                }
                return false;
            }
        }, ext.carrier, type, typechecker, refExpr, null);
        if (instanceClassCallPair != null) {
            TypedExpression instance = instanceClassCallPair.proj1;
            CoreClassCallExpression classCall = instanceClassCallPair.proj2;
            if (classCall != null) {
                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.Monoid)) {
                    rules.add(new MonoidIdentityRule(instance, classCall, ext, refExpr, typechecker, false));
                }
                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.AddMonoid)) {
                    rules.add(new MonoidIdentityRule(instance, classCall, ext, refExpr, typechecker, true));
                }
                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.Semiring)) {
                    rules.add(new MultiplicationByZeroRule(instance, classCall, ext, refExpr, typechecker));
                }
                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.Ring)) {
                    rules.add(new MulOfNegativesRule(instance, classCall, ext, refExpr, typechecker));
                }

                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.AddGroup)) {
                    rules.add(new DoubleNegationRule(instance, classCall, ext, refExpr, typechecker, true));
                    rules.add(new IdentityInverseRule(instance, classCall, ext, refExpr, typechecker, true));
                    rules.add(new NegationPropagationRule(instance, classCall, ext, refExpr, typechecker, true));
                } else if (classCall.getDefinition().isSubClassOf(ext.equationMeta.Group)) {
                    rules.add(new DoubleNegationRule(instance, classCall, ext, refExpr, typechecker, false));
                    rules.add(new IdentityInverseRule(instance, classCall, ext, refExpr, typechecker, false));
                    rules.add(new NegationPropagationRule(instance, classCall, ext, refExpr, typechecker, false));
                }/**/

                if (classCall.getDefinition().isSubClassOf(ext.equationMeta.CGroup)) {
                    rules.add(new AbGroupInverseRule(instance, classCall, ext, refExpr, typechecker, false));
                } else if (classCall.getDefinition().isSubClassOf(ext.equationMeta.AbGroup)) {
                    rules.add(new AbGroupInverseRule(instance, classCall, ext, refExpr, typechecker, true));
                } else if (classCall.getDefinition().isSubClassOf(ext.equationMeta.Group)) {
                    rules.add(new GroupInverseRule(instance, classCall, ext, refExpr, typechecker, false));
                } else if (classCall.getDefinition().isSubClassOf(ext.equationMeta.AddGroup)) {
                    rules.add(new GroupInverseRule(instance, classCall, ext, refExpr, typechecker, true));
                }/**/
            }
        }

        return rules;
    }