Function findRoot

src/simplicity/typeInference.c:25–44

Returns the representative of this variable's equivalence class. * Note: the 'parent' pointers of some variables within this equivalence class may be adjusted (to point more directly to the * representative). * * Precondition: NULL != alpha * * Postcondition: NULL == result_value->parent */

 * Postcondition: NULL == result_value->parent
 */
static unification_var* findRoot(unification_var* alpha) {
  /* During unification, when '.rank' fields are active, the value of 'alpha->rank' strictly increases during this loop.
   * If 'alpha->rank' = 'i', then there must be at least 2^'i' unification variables referencing (indirectly) 'alpha'.
   * Therefore, this loop terminates in at most log_2('n')/2 steps where 'n' is the number of unification variables in 'alpha's
   * equivalence class.
   * This bound holds even during freezing when 'alpha->rank' may not be activated.
   *
   * Note: the total number of unification variables created for type inference is linearly bounded by the number of nodes
   * in the Simplicity expression being inferred's DAG.
   *
   * According to ``Worst-Case Analysis of Set Union Algorithms'' by Robert E. Tarjan and Jan van Leeuwen (1984)
   * the "path halving" method used in this implementation is adequate to ensure that the amortized time complexity is
   * O(InvAck('n')) and ``for all practical purposes InvAck('n') a constant no larger than four''.
   */
  while (alpha->parent != NULL) {
    if (alpha->parent->parent != NULL) alpha->parent = alpha->parent->parent;
    alpha = alpha->parent;
  }
  return alpha;
}

/* Begin attempt to add a new binding, 'bound', to a unification variable 'alpha' representing its equivalence class.
 * If 'alpha' is a free variable, it becomes a bound to a copy of 'bound' and 'true' is returned.