public List getVarIds()

in meta/src/main/java/org/arend/lib/meta/closure/CongruenceClosure.java [412:471]


    public List<VarId> getVarIds(CoreExpression value) {
      int prefixSize = 0;
      List<VarId> result = new ArrayList<>();
      int index = getIndex(value);

      if (index == -1) {
        return result;
      }

      if (!(value instanceof CoreDefCallExpression)) {
        return result;
      }

      List<Integer> argInds = new ArrayList<>();

      for (CoreExpression arg : ((CoreDefCallExpression) value).getDefCallArguments()) {
        int argInd = getIndex(arg);
        argInds.add(argInd);
      }

      int numArgs = argInds.size();

      for (int i = 0; i < values.size(); i++) {
        if (i == index) continue;
        CoreExpression element = values.get(i);
        if (element instanceof CoreDefCallExpression && ((CoreDefCallExpression) value).getDefinition().equals(((CoreDefCallExpression) element).getDefinition())) {
          if (((CoreDefCallExpression) element).getDefCallArguments().size() != numArgs) return Collections.emptyList();
          if (prefixSize == 0) {
            result.add(new VarId(i, numArgs - prefixSize - 1));
            ++prefixSize;
          }
          for (int j = 0; j < numArgs; ++j) {
            if (argInds.get(j) == -1) {
              break;
            }
            int elementArg = getIndex(((CoreDefCallExpression) element).getDefCallArguments().get(j));
            if (argInds.get(j) == elementArg) {
              if (prefixSize <= j + 1) {
                result.add(new VarId(i, numArgs - prefixSize - 1));
                ++prefixSize;
              }
            } else {
              break;
            }
          }
          if (prefixSize > argInds.size() || prefixSize > 0 && argInds.get(prefixSize - 1) == -1) {
            break;
          }
        }
      }

      for (int i = 0; i < numArgs - prefixSize; ++i) {
        result.add(null);
      }

      result.add(new VarId(index, -1));
      Collections.reverse(result);

      return result;
    }