in meta/src/main/java/org/arend/lib/meta/RewriteMeta.java [244:441]
public TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
List<? extends ConcreteArgument> args = contextData.getArguments();
int currentArg = 0;
ConcreteExpression occurrencesArg = args.get(0).isExplicit() ? null : args.get(currentArg++).getExpression();
List<? extends ConcreteExpression> args0 = new ArrayList<>(Utils.getArgumentList(args.get(currentArg++).getExpression()));
if (args0.isEmpty()) {
return typechecker.typecheck(args.get(currentArg).getExpression(), contextData.getExpectedType());
}
CoreExpression expectedType = contextData.getExpectedType() == null ? null : contextData.getExpectedType().getUnderlyingExpression();
boolean reverse = expectedType == null || args.size() > currentArg + 2;
boolean isForward = reverse || this.isForward;
ErrorReporter errorReporter = typechecker.getErrorReporter();
ConcreteReferenceExpression refExpr = contextData.getReferenceExpression();
ConcreteFactory factory = ext.factory.withData(refExpr.getData());
if (args0.size() > 1) {
if (isForward) {
Collections.reverse(args0);
}
ConcreteExpression result = args.get(currentArg++).getExpression();
for (int i = args0.size() - 1; i >= 0; i--) {
ConcreteAppBuilder builder = factory.appBuilder(refExpr);
if (occurrencesArg != null) builder.app(occurrencesArg, false);
result = builder.app(args0.get(i)).app(result).build();
}
return typechecker.typecheck(factory.app(result, args.subList(currentArg, args.size())), contextData.getExpectedType());
}
ConcreteExpression arg0 = args0.get(0);
// Collect occurrences
List<Integer> occurrences;
if (occurrencesArg != null) {
occurrences = new ArrayList<>();
for (ConcreteExpression expr : Utils.getArgumentList(occurrencesArg)) {
getNumber(expr, occurrences, errorReporter);
}
} else {
occurrences = null;
}
//noinspection SimplifiableConditionalExpression
boolean isInverse = reverse && !this.isForward ? !this.isInverse : this.isInverse;
// Add inference holes to functions and type-check the path argument
TypedExpression path = Utils.typecheckWithAdditionalArguments(arg0, typechecker, ext, 0, false);
if (path == null) {
return null;
}
// Check that the first argument is a path
CoreFunCallExpression eq = Utils.toEquality(path.getType(), errorReporter, arg0);
if (eq == null) {
return null;
}
ConcreteExpression transport = factory.ref((isInverse ? ext.transportInv : ext.transport).getRef(), refExpr.getPLevels(), refExpr.getHLevels());
CoreExpression value = eq.getDefCallArguments().get(isInverse == isForward ? 2 : 1);
// This case won't happen often, but sill possible
if (!isForward && expectedType instanceof CoreInferenceReferenceExpression) {
CoreExpression var = value.getUnderlyingExpression();
if (var instanceof CoreInferenceReferenceExpression && ((CoreInferenceReferenceExpression) var).getVariable() == ((CoreInferenceReferenceExpression) expectedType).getVariable()) {
if (!(occurrences == null || occurrences.isEmpty() || occurrences.size() == 1 && occurrences.contains(1))) {
occurrences.remove(1);
errorReporter.report(new SubexprError(typechecker.getExpressionPrettifier(), occurrences, var, null, expectedType, refExpr));
return null;
}
ArendRef ref = factory.local("T");
return typechecker.typecheck(factory.app(transport, true, Arrays.asList(
factory.lam(Collections.singletonList(factory.param(ref)), factory.ref(ref)),
factory.core("transport (\\lam T => T) {!} _", path),
args.get(currentArg).getExpression())), null);
}
isForward = true;
}
TypedExpression lastArg;
CoreExpression type;
if (isForward) {
lastArg = typechecker.typecheck(args.get(currentArg++).getExpression(), null);
if (lastArg == null) {
return null;
}
type = lastArg.getType();
} else {
lastArg = null;
type = expectedType;
}
if (useEqSolver) {
solver = new EqualitySolver(ext.equationMeta, typechecker, factory, refExpr);
solver.setValuesType(value.computeType());
solver.setUseHypotheses(false);
solver.initializeSolver();
}
ConcreteExpression concretePath = factory.core(path);
CoreExpression normType = type.normalize(NormalizationMode.RNF);
ConcreteExpression term = lastArg == null ? args.get(currentArg++).getExpression() : factory.core("transport _ _ {!}", lastArg);
var occurVars = new ArrayList<ArendRef>();
var eqProofs = new ArrayList<EqProofConcrete>();
var processor = new RewriteExpressionProcessor(value, eq.getDefCallArguments().get(0), occurrences, typechecker, refExpr);
typechecker.withCurrentState(tc -> normType.processSubexpression(processor));
var foundOccurs = processor.getFoundOccurrences();
int firstExactMatch = processor.getExactMatches().isEmpty() ? -1 : processor.getExactMatches().get(0);
if (foundOccurs.isEmpty() || !processor.allOccurrencesFound()) {
errorReporter.report(new SubexprError(typechecker.getExpressionPrettifier(), occurrences, value, null, normType, refExpr));
return null;
}
Map<Integer, Integer> occurIndToVarInd = new HashMap<>();
for (int i = 0; i < foundOccurs.size(); ++i) {
boolean isExactMatch = processor.getExactMatches().contains(i);
if (i <= firstExactMatch || !isExactMatch) {
var var = factory.local("y" + i);
occurIndToVarInd.put(i, occurVars.size());
occurVars.add(var);
var left = factory.core(isInverse == isForward ? eq.getDefCallArguments().get(1).computeTyped() : foundOccurs.get(i).proj2.computeTyped());
var right = factory.core(isInverse == isForward ? foundOccurs.get(i).proj2.computeTyped() : eq.getDefCallArguments().get(2).computeTyped());
if (isExactMatch) {
eqProofs.add(new EqProofConcrete(concretePath, left, right));
} else {
var subExprOccur = foundOccurs.get(i).proj1;
var fixedLeft = factory.appBuilder(subExprOccur.exprWithOccurrences).app(left).build();
var fixedRight = factory.appBuilder(subExprOccur.exprWithOccurrences).app(right).build();
var occurPathTransport = factory.appBuilder(factory.ref(ext.pmap.getRef())).app(subExprOccur.exprWithOccurrences).app(concretePath).build();
var eqProof = factory.appBuilder(factory.ref(ext.concat.getRef())).app(subExprOccur.equalityProof).app(occurPathTransport).build();
eqProofs.add(new EqProofConcrete(eqProof, fixedLeft, fixedRight)); // (factory.core(solver.finalize(eqProof)));
}
} else {
occurIndToVarInd.put(i, occurVars.size() - 1);
}
}
var lamParams = new ArrayList<ConcreteParameter>();
for (int i = 0; i < occurVars.size(); ++i) {
var var = occurVars.get(i);
var typeParam = useEqSolver ? factory.core(foundOccurs.get(i).proj2.computeType().computeTyped()) : factory.core(eq.getDefCallArguments().get(0).computeTyped());
lamParams.add(factory.param(true, Collections.singletonList(var), typeParam));
}
ConcreteExpression lam = factory.lam(lamParams, factory.meta("\\lam y_v => {!}", new MetaDefinition() {
@Override
public TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
List<TypedExpression> checkedVars = new ArrayList<>();
for (var var : occurVars) {
var checkedVar = typechecker.typecheck(factory.ref(var), null);
assert checkedVar != null;
checkedVars.add(checkedVar);
}
Map<CoreExpression, Integer> indexOfSubExpr = new HashMap<>();
for (int i = 0; i < foundOccurs.size(); ++i) {
indexOfSubExpr.put(foundOccurs.get(i).proj2, i);
}
// TypedExpression exactMatchVar = finalExactMatchParam != null ? typechecker.typecheck(factory.ref(finalExactMatchParam.getBinding()), null) : var;
var typeWithOccur = normType.replaceSubexpressions(expression -> {
Integer occurInd = indexOfSubExpr.get(expression);
if (occurInd == null) return null;
Integer varInd = occurIndToVarInd.get(occurInd);
if (varInd == null) return null;
return checkedVars.get(varInd).getExpression();
}, false);
TypedExpression result = typeWithOccur != null ? Utils.tryTypecheck(typechecker, tc -> tc.check(typeWithOccur, refExpr)) : null;
if (result == null) {
errorReporter.report(typeWithOccur == null ? new SubexprError(typechecker.getExpressionPrettifier(), occurrences, value, null, normType, refExpr) : new TypeError(typechecker.getExpressionPrettifier(), "Cannot substitute a variable. The resulting type is invalid", typeWithOccur, refExpr));
}
return result;
}
}));
var checkedLam = typechecker.typecheck(lam, null);
if (checkedLam == null || checkedLam instanceof CoreErrorExpression) {
return null;
}
term = chainOfTransports(transport, checkedLam.getExpression(), eqProofs, term, factory, ext);
if (term == null) return null;
term = factory.appBuilder(term)
.app(args.subList(currentArg, args.size()))
.build();
if (useEqSolver) return solver.finalize(term);
return typechecker.typecheck(term, expectedType);
}