unification.h

// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
// -*- mode: C++ -*-
//
// Copyright 2022-2024 Google LLC
//
// Licensed under the Apache License v2.0 with LLVM Exceptions (the
// "License"); you may not use this file except in compliance with the
// License.  You may obtain a copy of the License at
//
//     https://llvm.org/LICENSE.txt
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//
// Author: Giuliano Procida

#ifndef STG_UNIFICATION_H_
#define STG_UNIFICATION_H_

#include "graph.h"
#include "runtime.h"

namespace stg {

// Keep track of which nodes are pending substitution and rewrite the graph on
// destruction.
class Unification {
 public:
  Unification(Runtime& runtime, Graph& graph, Id start, Id limit);

  ~Unification() noexcept(false);

  // id2 will always be preferred as a parent node; interpreted as a
  // substitution, id1 will be replaced by id2
  void Union(Id id1, Id id2);

  Id Find(Id id);

  // attempt to unify, recursively, allowing types declarations to be replaced
  // by definitions
  bool Unify(Id id1, Id id2);

 private:
  Graph& graph_;
  Id start_;
  DenseIdMapping mapping_;
  Runtime& runtime_;
  Counter find_query_;
  Counter find_halved_;
  Counter union_known_;
  Counter union_unknown_;
};

}  // namespace stg

#endif  // STG_UNIFICATION_H_