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;
}