Solve the constraints of source and target types of each subexpression in a Simplicity DAG. * * If the Simplicity DAG, 'dag', has a principal type (including constraints due to sharing of subexprssions), * then 'arrow[i]'s and 'source' and 'target' fields are set to unification variables * that are bound to the principal source and target types of subexpression denoted by the slice '(dag_nodes
| 265 | * and 'arrow' is a graph of bindings that satisfies the typing constraints of imposed by 'dag'. |
| 266 | */ |
| 267 | static simplicity_err typeInference( unification_arrow* arrow, const dag_node* dag, const uint_fast32_t len, |
| 268 | unification_var* extra_var, unification_var* bound_var, size_t word256_ix, size_t* bindings_used |
| 269 | ) { |
| 270 | for (uint_fast32_t i = 0; i < len; ++i) { |
| 271 | switch (dag[i].tag) { |
| 272 | #define UNIFY(a, b) { if (!unify((a), (b), bindings_used)) return SIMPLICITY_ERR_TYPE_INFERENCE_UNIFICATION; } |
| 273 | #define APPLY_BINDING(a, b) { if (!applyBinding((a), (b), bindings_used)) return SIMPLICITY_ERR_TYPE_INFERENCE_UNIFICATION; } |
| 274 | case COMP: |
| 275 | arrow[i] = (unification_arrow){0}; |
| 276 | UNIFY(&(arrow[dag[i].child[0]].source), &(arrow[i].source)); |
| 277 | UNIFY(&(arrow[dag[i].child[1]].target), &(arrow[i].target)); |
| 278 | UNIFY(&(arrow[dag[i].child[0]].target), &(arrow[dag[i].child[1]].source)); |
| 279 | break; |
| 280 | case ASSERTL: |
| 281 | case ASSERTR: |
| 282 | case CASE: |
| 283 | *bindings_used += 2; |
| 284 | extra_var[0] = extra_var[1] = extra_var[2] = (unification_var){0}; |
| 285 | extra_var[3] = (unification_var) |
| 286 | { .isBound = true |
| 287 | , .bound = { .kind = SUM |
| 288 | , .arg = { &extra_var[0], &extra_var[1] } |
| 289 | } }; |
| 290 | arrow[i] = (unification_arrow){ .source = |
| 291 | { .isBound = true |
| 292 | , .bound = { .kind = PRODUCT |
| 293 | , .arg = { &extra_var[3], &extra_var[2] } |
| 294 | } } }; |
| 295 | if (ASSERTR != dag[i].tag) { |
| 296 | *bindings_used += 1; |
| 297 | APPLY_BINDING(&(arrow[dag[i].child[0]].source), &((binding) |
| 298 | { .kind = PRODUCT |
| 299 | , .arg = { &extra_var[0], &extra_var[2] } |
| 300 | })); |
| 301 | UNIFY(&(arrow[dag[i].child[0]].target), &(arrow[i].target)); |
| 302 | } |
| 303 | if (ASSERTL != dag[i].tag) { |
| 304 | *bindings_used += 1; |
| 305 | APPLY_BINDING(&(arrow[dag[i].child[1]].source), &((binding) |
| 306 | { .kind = PRODUCT |
| 307 | , .arg = { &extra_var[1], &extra_var[2] } |
| 308 | })); |
| 309 | UNIFY(&(arrow[dag[i].child[1]].target), &(arrow[i].target)); |
| 310 | } |
| 311 | extra_var += 4; |
| 312 | break; |
| 313 | case PAIR: |
| 314 | *bindings_used += 1; |
| 315 | arrow[i] = (unification_arrow){ .target = |
| 316 | { .isBound = true |
| 317 | , .bound = { .kind = PRODUCT |
| 318 | , .arg = { &(arrow[dag[i].child[0]].target), &(arrow[dag[i].child[1]].target) } |
| 319 | } } }; |
| 320 | UNIFY(unify(&(arrow[dag[i].child[0]].source), &(arrow[dag[i].child[1]].source), bindings_used), &(arrow[i].source)); |
| 321 | break; |
| 322 | case DISCONNECT: |
| 323 | *bindings_used += 3; |
| 324 | *extra_var = (unification_var){0}; |
no test coverage detected