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. * If 'alpha' is already bound to the same kind of type, new unification constraints may be added by overwriting '**cont' * and putting more elements into the '*cont' stack and 'true' is
| 66 | * NULL != bindings_used |
| 67 | */ |
| 68 | static bool applyBinding_cont(unification_var* alpha, binding* bound, unification_cont** cont, size_t* bindings_used) { |
| 69 | if (!alpha->isBound) { |
| 70 | /* alpha is currently a free variable. Copy the provided binding. */ |
| 71 | alpha->isBound = true; |
| 72 | alpha->bound = *bound; |
| 73 | *cont = (*cont)->next; |
| 74 | return true; |
| 75 | } |
| 76 | |
| 77 | if (&alpha->bound == bound) { |
| 78 | simplicity_assert(false); /* The algorithm should never try to bind an already bound variable to it's own binding. */ |
| 79 | |
| 80 | /* However, if it does happen then just return successfully without pushing any new unification constraints. */ |
| 81 | *cont = (*cont)->next; |
| 82 | return true; |
| 83 | } |
| 84 | |
| 85 | if (alpha->bound.kind != bound->kind) return false; /* Unification failure */ |
| 86 | /* Otherwise 'bound' is bound to the same kind of type as 'alpha's. */ |
| 87 | |
| 88 | if (ONE == bound->kind) { |
| 89 | /* 'bound' is a trivial binding. */ |
| 90 | *cont = (*cont)->next; |
| 91 | return true; |
| 92 | } else { |
| 93 | /* 'bound' is a non-trivial binding. |
| 94 | * Push two new pairs of the 'alpha->bound' and 'bound' type's unification variables to the stack of variables to be unified |
| 95 | * by overwriting the top of the stack and slipping a new stack item underneath it. |
| 96 | */ |
| 97 | |
| 98 | (*cont)->alpha = alpha->bound.arg[0]; |
| 99 | (*cont)->beta = bound->arg[0]; |
| 100 | /* 'bound' will not be used further, so it is safe to activate 'bound->cont'. */ |
| 101 | bound->cont = (unification_cont){ .alpha = alpha->bound.arg[1] |
| 102 | , .beta = bound->arg[1] |
| 103 | , .next = (*cont)->next |
| 104 | }; |
| 105 | (*cont)->next = &(bound->cont); |
| 106 | simplicity_assert(0 < *bindings_used); |
| 107 | (*bindings_used)--; |
| 108 | } |
| 109 | return true; |
| 110 | } |
| 111 | |
| 112 | /* Unify a stack of pairs of unification variables. |
| 113 | * If any unification fails, then NULL is returned. |
no outgoing calls
no test coverage detected