in base/src/main/java/org/arend/core/pattern/ConstructorExpressionPattern.java [275:373]
public List<? extends Expression> getMatchingExpressionArguments(Expression expression, boolean normalize) {
Expression dataExpr = getDataExpression();
if (dataExpr instanceof SigmaExpression) {
TupleExpression tuple = expression.cast(TupleExpression.class);
return tuple == null ? null : tuple.getFields();
}
if (dataExpr instanceof FunCallExpression) {
FunctionDefinition function = ((FunCallExpression) dataExpr).getDefinition();
expression = expression.getUnderlyingExpression();
if (function == Prelude.EMPTY_ARRAY) {
if (expression instanceof ArrayExpression array && array.getElements().isEmpty() && array.getTail() == null) {
return array.getConstructorArguments(getArrayElementsType() == null, getArrayLength() == null, normalize);
}
ClassCallExpression classCall = expression.getType().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
if (classCall != null && classCall.getDefinition() == Prelude.DEP_ARRAY) {
Expression length = classCall.getImplementationHere(Prelude.ARRAY_LENGTH, expression);
if (length != null) {
length = length.normalize(NormalizationMode.WHNF);
if (length instanceof IntegerExpression && ((IntegerExpression) length).isZero()) {
return getArrayElementsType() == null ? Collections.singletonList(FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expression)) : Collections.emptyList();
}
}
}
return null;
}
if (function == Prelude.ARRAY_CONS) {
if (expression instanceof ArrayExpression array && !array.getElements().isEmpty()) {
return array.getConstructorArguments(getArrayElementsType() == null, getArrayLength() == null, normalize);
}
ClassCallExpression classCall = expression.getType().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
if (classCall != null && classCall.getDefinition() == Prelude.DEP_ARRAY) {
Expression length = classCall.getImplementationHere(Prelude.ARRAY_LENGTH, expression);
if (length != null) {
if (length instanceof IntegerExpression && !((IntegerExpression) length).isZero() || length instanceof ConCallExpression && ((ConCallExpression) length).getDefinition() == Prelude.SUC) {
List<Expression> result = new ArrayList<>(4);
if (getArrayLength() == null) result.add(length instanceof IntegerExpression intExpr ? intExpr.pred() : ((ConCallExpression) length).getDefCallArguments().get(0));
Expression elementsType = FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expression);
if (getArrayElementsType() == null) result.add(elementsType);
result.add(AppExpression.make(FieldCallExpression.make(Prelude.ARRAY_AT, expression), new SmallIntegerExpression(0), true));
result.add(ArrayExpression.makeTail(length, elementsType, classCall, expression));
return result;
}
}
}
return null;
}
if (function != Prelude.IDP) {
return null;
}
if (expression instanceof FunCallExpression && ((FunCallExpression) expression).getDefinition() == Prelude.IDP) {
return Collections.emptyList();
}
if (!(expression instanceof PathExpression)) {
return null;
}
Expression arg = ((PathExpression) expression).getArgument();
if (normalize) {
arg = arg.normalize(NormalizationMode.WHNF);
}
LamExpression lamExpr = arg.cast(LamExpression.class);
if (lamExpr == null) {
return null;
}
Expression body = lamExpr.getParameters().getNext().hasNext() ? new LamExpression(lamExpr.getResultSort(), lamExpr.getParameters().getNext(), lamExpr.getBody()) : lamExpr.getBody();
return NormalizingFindBindingVisitor.findBinding(body, lamExpr.getParameters()) ? null : Collections.emptyList();
}
if (dataExpr instanceof ConCallExpression || dataExpr instanceof SmallIntegerExpression) {
ConCallExpression conCall = expression.cast(ConCallExpression.class);
Definition myConstructor = getDefinition();
if (conCall == null && (myConstructor == Prelude.ZERO || myConstructor == Prelude.SUC)) {
IntegerExpression intExpr = expression.cast(IntegerExpression.class);
if (intExpr != null) {
return myConstructor == Prelude.ZERO && intExpr.isZero()
? Collections.emptyList()
: myConstructor == Prelude.SUC && !intExpr.isZero()
? Collections.singletonList(intExpr.pred())
: null;
}
}
if (conCall == null || conCall.getDefinition() != myConstructor) {
return null;
}
return conCall.getDefCallArguments();
}
NewExpression newExpr = expression.cast(NewExpression.class);
if (newExpr == null) {
return null;
}
List<Expression> arguments = new ArrayList<>();
for (ClassField field : ((ClassCallExpression) dataExpr).getDefinition().getNotImplementedFields()) {
if (!((ClassCallExpression) dataExpr).isImplementedHere(field)) {
arguments.add(newExpr.getImplementation(field));
}
}
return arguments;
}