Function freeze

src/simplicity/typeInference.c:436–492

Set '*result' to the index within 'type_dag' that contains an instance type bound by 'var' where free variables are instantiated * at the ONE type, recursively adding new nodes to 'type_dag' as necessary. * '*type_dag_used' will be incremented by the number of new 'type_dag' nodes created. * * If it is impossible to create a required instance (due to a cycle in the bindings reachable by 'var')

 * Postcondition: If 'true' is returned, then type type_dag[*type_dag_used] is well-formed
 */
static bool freeze(size_t* result, type* type_dag, size_t* type_dag_used, unification_var* var) {
  var = findRoot(var);

  if (isFrozen(var)) {
    *result = getFrozenIx(var);
    return true;
  }

  /* 'var' is not frozen, and therefore it must have a non-trivial binding.
   * Create a one item stack of unification variables 'var' to be frozen.
   */
  var->next = NULL;
  simplicity_assert(!var->bound.occursCheck);
  var->bound.occursCheck = true;

  /* Attempt to freeze all variables on the stack, pushing new variables onto the stack to recursively freeze them if needed.
   *
   * All variables in the stack are representatives of their equivalence class and have just had their 'occursCheck' flag changed
   * from 'false' to 'true'.
   * Variables never change their 'occursCheck' flag back from 'true' to 'false'.
   * Variables are only removed from the stack after being frozen.
   * Each time we go through this loop, the stack size either increases by 1 or decreases by 1.
   * Therefore the total number of times this loop iterates summed over all calls to 'freeze' is bounded by
   * twice the number of unification variable (representatives) with non-trivial bindings.
   * ("twice" because once to add the variable to the stack and once to remove the variable from the stack).
   *
   * Note that number of unification_variables is bound linearly in the number of nodes in the Simplicity DAG.
   */
  while (var) {
    unification_var* typeArg[2] = { findRoot(var->bound.arg[0]), findRoot(var->bound.arg[1]) };
    if (!isFrozen(typeArg[0])) {
      /* The first type argument's representative isn't frozen.  Add it to the stack and immediately attempt to freeze it. */
      if (typeArg[0]->bound.occursCheck) return false; /* Occurs check failure. */
      typeArg[0]->bound.occursCheck = true;
      typeArg[0]->next = var;
      var = typeArg[0];
    } else if (!isFrozen(typeArg[1])) {
      /* The second type argument's representative isn't frozen.  Add it to the stack and immediately attempt to freeze it. */
      if (typeArg[1]->bound.occursCheck) return false; /* Occurs check failure. */
      typeArg[1]->bound.occursCheck = true;
      typeArg[1]->next = var;
      var = typeArg[1];
    } else {
      /* Both the type argument's representatives are frozen.
       * Create a new entry in the 'type_dag' for 'var's binding and freeze 'var'.
       */
      *result = var->bound.frozen_ix = (*type_dag_used)++;
      type_dag[var->bound.frozen_ix] = (type)
        { .kind = var->bound.kind
        , .typeArg = { getFrozenIx(typeArg[0]), getFrozenIx(typeArg[1]) }
        };
      var = var->next;
    }
  }

  return true;
}