<commit_before>/* Copyright 2009-2016 EPFL, Lausanne */

package stainless.utils

import scala.collection.mutable.{ ListBuffer, Map => MutableMap, Set => MutableSet, Queue => MutableQueue }

/**
 * Describes a Graph of Computation that is incrementally refined/updated. [[Node]]s can be inserted
 * (and updated), sequentially to build a full graph. After each [[update]], [[compute]] is called at
 * most once with the set of all nodes not yet computed -- which (indirect, possibly cyclic) dependencies
 * are all known -- with the dependencies themselves, hence a node might be passed to [[compute]]
 * several times. When any dependency of a node is updated, the node is recomputed.
 */
trait IncrementalComputationalGraph[Id, Input, Result] {

  /******************* Public Interface ***********************************************************/

  /**
   * Insert (or override) a given node into the graph, then perform computation
   * based on the graph state. Return the computed values.
   */
  def update(id: Id, in: Input, deps: Set[Id]): Option[Result] = {
    update(Node(id, in, deps))
  }

  /******************* Customisation Points *******************************************************/

  /**
   * Produce some result for the set of nodes that are all ready.
   *
   * If is guarantee that [[ready]] contains all the dependencies for all element of [[ready]].
   *
   * The result itself is not used by [[IncrementalComputationalGraph]].
   */
  protected def compute(ready: Set[(Id, Input)]): Result

  /**
   * Determine whether the new value for a node is equivalent to the old value, given that
   * they have the same id (enforced by the graph model) and the same set of dependencies.
   *
   * The default implementation make the conservative assumption that two inputs are equivalent
   * if and only if they are equal. This function can be redefined in subclasses if needed.
   */
  protected final def equivalent(id: Id, deps: Set[Id], oldInput: Input, newInput: Input): Boolean = {
    false // FIXME: oldInput == newInput is not correct; remove `final` qualifier.
  }

  /******************* Implementation *************************************************************/

  /**
   * Representation of a [[Node]]:
   *  - It's [[id]] fully identifies a node (i.e. two nodes are equal <=> their ids are equal).
   *    This allows overriding a node simply by inserting a new node with the same identifier.
   *  - [[in]] denotes the input value for the node which is used for the computation.
   *  - [[deps]] holds the set of **direct** dependencies.
   * Indirect dependencies is computed by [[IncrementalComputationalGraph]] itself.
   */
  private case class Node(id: Id, in: Input, deps: Set[Id]) {
    override def equals(any: Any): Boolean = any match {
      case Node(other, _, _) => id == other
      case _ => false
    }

    override def hashCode = id.hashCode
  }

  /**
   * Implementation for the public [[update]] function.
   *
   * If the new node is equivalent to an old one, do nothing. Otherwise, process normally.
   */
  private def update(n: Node): Option[Result] = {
    def run(delete: Boolean) = {
      if (delete) remove(n)
      insert(n)
      process()
    }

    nodes get n.id match {
      case Some(m) if (m.deps == n.deps) && equivalent(n.id, n.deps, m.in, n.in) => None // nothing new
      case mOpt => run(mOpt.isDefined)
    }
  }

  /**
   * Some nodes might not yet be fully known, yet we have some evidence (through other nodes'
   * dependencies) that they exists. We therefore keep track of dependencies using their
   * identifiers, and we keep track of the mapping between identifiers and nodes in [[nodes]].
   */
  private val nodes = MutableMap[Id, Node]()

  /* The set of nodes not yet computed, but seen. */
  private val toCompute = MutableSet[Node]()

  /*
   * A reverse graph of dependencies. Because we might not fully know the node yet.
   * we use the known identifiers for the mapping.
   */
  private val reverse = MutableMap[Id, MutableSet[Node]]()


  /** Insert a new node & update the graph. */
  private def insert(n: Node): Unit = {
    nodes += n.id -> n
    toCompute += n
    n.deps foreach { depId =>
      reverse.getOrElseUpdate(depId, MutableSet()) += n
    }
  }

  /** Remove an existing node from the graph. */
  private def remove(n: Node): Unit = {
    nodes -= n.id
    reverse.values foreach { _ -= n }

    mark(n)
  }

  /** Recursively put the nodes that depends on [[n]] into [[toCompute]]. */
  private def mark(n: Node): Unit = {
    val seen = MutableSet[Node]()
    val queue = MutableQueue[Node]()<commit_msg>Update IncrementalComputationalGraph<commit_after>/* Copyright 2009-2016 EPFL, Lausanne */

package stainless.utils

import scala.collection.mutable.{ ListBuffer, Map => MutableMap, Set => MutableSet, Queue => MutableQueue }

/**
 * Describes a Graph of Computation that is incrementally refined/updated. [[Node]]s can be inserted
 * (and updated) sequentially to build a full graph. After each [[update]], [[compute]] is called at
 * most once with the set of all nodes not yet computed -- which (indirect, possibly cyclic) dependencies
 * are all known -- with the dependencies themselves, hence a node might be passed to [[compute]]
 * several times. When any dependency of a node is updated, the node is recomputed.
 */
trait IncrementalComputationalGraph[Id, Input, Result] {

  /******************* Public Interface ***********************************************************/

  /**
   * Insert (or override) a given node into the graph, then perform computation
   * based on the graph state. Return the computed values.
   */
  def update(id: Id, in: Input, deps: Set[Id]): Option[Result] = {
    update(Node(id, in, deps))
  }

  /******************* Customisation Points *******************************************************/

  /**
   * Produce some result for the set of nodes that are all ready.
   *
   * It is guarantee that [[ready]] contains all the dependencies for all element of [[ready]].
   *
   * The result itself is not used by [[IncrementalComputationalGraph]].
   */
  protected def compute(ready: Set[(Id, Input)]): Result

  /**
   * Determine whether the new value for a node is equivalent to the old value, given that
   * they have the same id (enforced by the graph model) and the same set of dependencies.
   */
  protected def equivalent(id: Id, deps: Set[Id], oldInput: Input, newInput: Input): Boolean

  /******************* Implementation *************************************************************/

  /**
   * Representation of a [[Node]]:
   *  - It's [[id]] fully identifies a node (i.e. two nodes are equal <=> their ids are equal).
   *    This allows overriding a node simply by inserting a new node with the same identifier.
   *  - [[in]] denotes the input value for the node which is used for the computation.
   *  - [[deps]] holds the set of **direct** dependencies.
   * Indirect dependencies is computed by [[IncrementalComputationalGraph]] itself.
   */
  private case class Node(id: Id, in: Input, deps: Set[Id]) {
    override def equals(any: Any): Boolean = any match {
      case Node(other, _, _) => id == other
      case _ => false
    }

    override def hashCode = id.hashCode
  }

  /**
   * Implementation for the public [[update]] function.
   *
   * If the new node is equivalent to an old one, do nothing. Otherwise, process normally.
   * Note that, when any of its dependencies is updated the (new) node is put in the
   * [[toCompute]] set.
   */
  private def update(n: Node): Option[Result] = nodes get n.id match {
    case Some(m) if (m.deps == n.deps) && equivalent(n.id, n.deps, m.in, n.in) =>
      // Nothing new, but update the node anyway -- equivalence != equality.
      nodes += n.id -> n
      None

    case mOpt =>
      val replace = mOpt.isDefined
      if (replace) remove(n)
      insert(n)
      process()
  }

  /**
   * Some nodes might not yet be fully known, yet we have some evidence (through other nodes'
   * dependencies) that they exists. We therefore keep track of dependencies using their
   * identifiers, and we keep track of the mapping between identifiers and nodes in [[nodes]].
   */
  private val nodes = MutableMap[Id, Node]()

  /* The set of nodes not yet computed, but seen. */
  private val toCompute = MutableSet[Node]()

  /*
   * A reverse graph of dependencies. Because we might not fully know the node yet.
   * we use the known identifiers for the mapping.
   */
  private val reverse = MutableMap[Id, MutableSet[Node]]()


  /** Insert a new node & update the graph. */
  private def insert(n: Node): Unit = {
    nodes += n.id -> n
    toCompute += n
    n.deps foreach { depId =>
      reverse.getOrElseUpdate(depId, MutableSet()) += n
    }
  }

  /**
   * Remove an existing node from the graph,
   * placing any node that depends on [[n]] into [[toCompute]]
   */
  private def remove(n: Node): Unit = {
    nodes -= n.id
    reverse.values foreach { _ -= n }

    mark(n)
  }

  /** Recursively put the nodes that depends on [[n]] into [[toCompute]]. */
  private def mark(n: Node): Unit = {
    val seen = MutableSet[Node]()
    val queue = MutableQueue[Node]()
{'fraction_non_alphanumeric': 0.15459670424978317, 'fraction_numerical': 0.0017346053772766695, 'mean_word_length': 3.2531120331950207, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 24, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '534570', 'n_tokens_mistral': 2618, 'n_tokens_neox': 2527, 'n_words': 1081}