in meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java [356:570]
private ConcreteExpression checkInternal(Context context, ConcreteExpression argument, CoreExpression expectedType, boolean withExpectedType, ConcreteSourceNode marker, ExpressionTypechecker typechecker) {
ContextHelper contextHelper = new ContextHelper(context, argument);
ConcreteFactory factory = ext.factory.withData(marker.getData());
CoreExpression type = null;
ConcreteExpression contr = null;
Values<UncheckedExpression> values = new Values<>(typechecker, marker);
Map<CoreClassField, Map<Integer, List<Edge<Integer>>>> transGraphs = new HashMap<>();
List<Negation> negations = new ArrayList<>();
List<ConcreteClause> clauses = new ArrayList<>();
if (argument != null && contextHelper.meta == null) {
TypedExpression contradiction = typechecker.typecheck(argument, null);
if (contradiction == null) {
return null;
}
type = Utils.unfoldType(contradiction.getType().normalize(NormalizationMode.WHNF));
if (isEmpty(type)) {
contr = factory.core(contradiction);
} else {
if (!makeNegation(type, factory.core(contradiction), factory, negations, values, transGraphs)) {
typechecker.getErrorReporter().report(new TypeError(typechecker.getExpressionPrettifier(), "The expression does not prove a contradiction", type, argument));
return null;
}
}
}
if (contr == null) {
BunchedEquivalenceClosure<Integer> equivalenceClosure = new BunchedEquivalenceClosure<>(factory.ref(ext.prelude.getIdp().getRef()), factory.ref(ext.inv.getRef()), factory.ref(ext.concat.getRef()), factory);
ValuesRelationClosure closure = new ValuesRelationClosure(values, equivalenceClosure);
List<Edge<Integer>> equalities = new ArrayList<>();
Values<CoreExpression> typeValues = new Values<>(typechecker, marker);
Map<Integer, RType> assumptions = new HashMap<>();
boolean searchForContradiction = negations.isEmpty() && transGraphs.isEmpty();
List<Integer> conIndices = new ArrayList<>();
for (CoreBinding binding : contextHelper.getAllBindings(typechecker)) {
type = Utils.unfoldType(binding.getTypeExpr().normalize(NormalizationMode.WHNF));
List<CoreDataCallExpression.ConstructorWithDataArguments> constructors = isAppropriateDataCall(type) ? type.computeMatchedConstructorsWithDataArguments() : null;
if (constructors != null && constructors.isEmpty()) {
contr = factory.ref(binding);
break;
}
if (constructors != null) {
contr = factory.ref(binding);
for (CoreDataCallExpression.ConstructorWithDataArguments con : constructors) {
List<ConcretePattern> subPatterns = new ArrayList<>();
for (CoreParameter param = con.getParameters(); param.hasNext(); param = param.getNext()) {
subPatterns.add(factory.refPattern(factory.local(ext.renamerFactory.getNameFromBinding(param.getBinding(), null) + "1"), null));
}
clauses.add(factory.clause(Collections.singletonList(factory.conPattern(con.getConstructor().getRef(), subPatterns)), factory.meta("case_" + con.getConstructor().getName(), new MetaDefinition() {
@Override
public @Nullable TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
ConcreteExpression result = check(HidingContext.make(context, Collections.singleton(binding)), null, null, true, marker, typechecker);
return result == null ? null : typechecker.typecheck(result, contextData.getExpectedType());
}
})));
}
break;
}
RType rType = makeRType(binding, type);
RType prev = null;
if (rType instanceof EqType) {
CoreExpression expr1 = ((EqType) rType).leftExpr.normalize(NormalizationMode.WHNF);
CoreExpression expr2 = ((EqType) rType).rightExpr.normalize(NormalizationMode.WHNF);
int value1 = values.addValue(expr1);
int value2 = values.addValue(expr2);
if (expr1 instanceof CoreConCallExpression || expr1 instanceof CoreIntegerExpression) {
conIndices.add(value1);
}
if (expr2 instanceof CoreConCallExpression || expr2 instanceof CoreIntegerExpression) {
conIndices.add(value2);
}
ConcreteExpression proof = factory.ref(binding);
closure.addRelation(value1, value2, proof);
equalities.add(new Edge<>(value1, value2, proof, EdgeKind.EQ, null));
} else {
prev = assumptions.putIfAbsent(typeValues.addValue(type), rType);
}
if (searchForContradiction && prev == null) {
makeNegation(type, factory.ref(binding), factory, negations, values, transGraphs);
}
}
if (contr == null) {
loop:
for (Integer conIndex1 : conIndices) {
for (Integer conIndex2 : conIndices) {
if (equivalenceClosure.areRelated(conIndex1, conIndex2) && values.getValue(conIndex1).areDisjointConstructors(values.getValue(conIndex2))) {
contr = equivalenceClosure.checkRelation(conIndex1, conIndex2);
type = null;
break loop;
}
}
}
if (contr == null) {
loop:
for (Negation negation : negations) {
Deque<ConcreteExpression> arguments = new ArrayDeque<>();
Map<CoreBinding, CoreExpression> subst = new HashMap<>();
for (int i = 0; i < negation.assumptions.size(); i++) {
RType assumption = negation.assumptions.get(i);
boolean isFree = false;
for (int j = i + 1; j < negation.assumptions.size(); j++) {
if (negation.assumptions.get(j).type.findFreeBinding(assumption.binding)) {
isFree = true;
break;
}
}
ConcreteExpression argExpr;
if (isFree) {
UncheckedExpression paramType = assumption.type.findFreeBindings(subst.keySet()) != null ? assumption.type.substitute(subst) : assumption.type;
CoreExpression checkedType;
if (paramType instanceof CoreExpression) {
checkedType = (CoreExpression) paramType;
} else {
TypedExpression typedExpr = typechecker.check(paramType, marker);
if (typedExpr == null) {
continue loop;
}
checkedType = typedExpr.getExpression();
}
argExpr = factory.hole();
subst.put(assumption.binding, Objects.requireNonNull(typechecker.typecheck(argExpr, checkedType)).getExpression());
} else {
if (assumption instanceof EqType) {
argExpr = closure.checkRelation(((EqType) assumption).leftExpr.substitute(subst), ((EqType) assumption).rightExpr.substitute(subst));
if (argExpr == null) {
continue loop;
}
} else {
int index = typeValues.getIndex(assumption.type.substitute(subst));
if (index == -1) {
continue loop;
}
argExpr = factory.ref(assumptions.get(index).binding);
}
}
arguments.add(argExpr);
}
contr = negation.proof.apply(arguments);
type = negation.type;
break;
}
if (contr == null) {
loop:
for (Map.Entry<CoreClassField, Map<Integer, List<Edge<Integer>>>> entry : transGraphs.entrySet()) {
for (Edge<Integer> edge : equalities) {
entry.getValue().computeIfAbsent(edge.source, k -> new ArrayList<>()).add(edge);
entry.getValue().computeIfAbsent(edge.target, k -> new ArrayList<>()).add(new Edge<>(edge.target, edge.source, edge.proof, EdgeKind.EQ_INV, null));
}
for (Negation negation : negations) {
List<Triple> triples = new ArrayList<>(negation.assumptions.size());
for (RType assumption : negation.assumptions) {
Triple triple = Triple.make(assumption.type);
if (triple == null || triple.fun.getDefinition() != entry.getKey()) break;
if (negation.assumptions.size() == 1) {
CoreExpression instanceType = triple.fun.getArgument().computeType().normalize(NormalizationMode.WHNF);
if (instanceType instanceof CoreClassCallExpression && ((CoreClassCallExpression) instanceType).getDefinition().isSubClassOf(ext.equationMeta.LinearOrder)) break;
}
triples.add(triple);
}
if (triples.size() != negation.assumptions.size()) continue;
Deque<ConcreteExpression> negationArgs = new ArrayDeque<>(triples.size());
for (Triple triple : triples) {
List<Edge<Integer>> path = bfs(entry.getValue(), values.addValue(triple.arg1), values.addValue(triple.arg2));
if (path == null) break;
negationArgs.add(makeTransitivityProof(entry.getKey(), path, factory));
}
if (negationArgs.size() == triples.size()) {
contr = negation.proof.apply(negationArgs);
type = negation.type;
break loop;
}
}
FieldKey.Data irreflexivityData = entry.getKey().getUserData(ext.irreflexivityKey);
if (irreflexivityData == null) continue;
for (Integer vertex : entry.getValue().keySet()) {
List<Edge<Integer>> path = bfs(entry.getValue(), vertex, vertex);
if (path != null) {
ConcreteExpression transProof = makeTransitivityProof(entry.getKey(), path, factory);
List<CoreParameter> irrParams = new ArrayList<>(2);
type = irreflexivityData.field.getResultType().getPiParameters(irrParams);
List<ConcreteArgument> irrArgs = new ArrayList<>(2);
if (irrParams.get(0).isExplicit()) {
irrArgs.add(factory.arg(factory.hole(), true));
}
irrArgs.add(factory.arg(transProof, irrParams.get(1).isExplicit()));
contr = factory.app(factory.ref(irreflexivityData.field.getRef()), irrArgs);
break loop;
}
}
}
}
if (contr == null) {
typechecker.getErrorReporter().report(new TypecheckingError("Cannot infer contradiction", marker));
return null;
}
}
}
}
return expectedType != null && type != null && expectedType.compare(type, CMP.EQ) ? contr : factory.caseExpr(false, Collections.singletonList(factory.caseArg(contr, null, null)), withExpectedType ? null : factory.ref(ext.Empty.getRef()), null, clauses);
}